The Application of Higher Order Logic to Security Models

Abstract

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Nov 01, 1991
Accession Number
ADA250128

Entities

People

  • A. Cant
  • K. Eastaughffe

Tags

Communities of Interest

  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Abstracts
  • Command And Control
  • Computer Program Verification
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Cybersecurity
  • Information Processing
  • Information Systems
  • Language
  • Mathematical Models
  • Security
  • Software Development
  • Specifications
  • Verification
  • Warfare

Fields of Study

  • Computer science

Readers

  • Artificial Intelligence
  • Critical Infrastructure Protection in CBRN and WMD Threats.
  • East Asian Political and Security Studies within the Soviet Union