Application of Higher Order Logic to Security Models.

摘要

This paper describes the application of the proof assistant HOL (Higher Order Logic) to reasoning about security models. Using Rushby's general framework for security models, we show how the HOL system can prove an unwinding theorem for non-interference of processes at different security levels. The method of unwinding is then applied to the Low Water Mark Model of security. From this analysis, we draw conclusions about the strengths and weaknesses of HOL as a reasoning tool.