The Application of Higher Order Logic to Security Models
ELECTRONICS RESEARCH LAB ADELAIDE (AUSTRALIA)
Pagination or Media Count:
This paper describes the application of the proof assistant HOL Higher Order Logic to reasoning about security models. Using Rushbys 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.
- Computer Programming and Software