Accession Number:

ADA250128

Title:

The Application of Higher Order Logic to Security Models

Descriptive Note:

Research rept.,

Corporate Author:

ELECTRONICS RESEARCH LAB ADELAIDE (AUSTRALIA)

Personal Author(s):

Report Date:

1991-11-01

Pagination or Media Count:

39.0

Abstract:

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.

Subject Categories:

  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE