Romulus, A Computer Security Properties Modeling Environment: Romulus Theories. Volume 1.
Abstract
The Romulus security properties modeling environment contains tools, theories, and models that support the high-level design and analysis of secure systems. The Romulus nondisclosure tool supports development and analysis of distributed composite security models and their properties. The Romulus modeling approach establishes the models on a solid theoretical basis and uses formal mathematical tools to aid in the analysis. Romulus allows a user to express a model of a secure system using a formal specification notation that combines graphics and text. Verification of the model proves that it satisfies its critical properties. The user verifies the model by using a combination of automatic decision procedures and interactive theorem proving. The primary emphasis in the current system is the analysis of multilevel trusted system models to see if they satisfy nondisclosure properties. Romulus also includes a tool for formally specifying and verifying authentication protocols. This tool can be used to reason about the beliefs of the parties engaged in a protocol in order to analyze whether the protocol achieves the desired behavior. The Romulus theories include formal theories of nondisclosure, integrity, and availability security. The Romulus library of models demonstrates the application of these theories.
Document Details
- Document Type
- Technical Report
- Publication Date
- Apr 01, 1996
- Accession Number
- ADA310945
Entities
People
- A. Heff
- B. Hartman
- L. Gong
- S. Brackin
- S. Foley