Formal Techniques for an ITSEC-E4 Secure Gateway

In this paper we describe the method used to develop a gateway capable of meeting the ITSEC E4 requirements. The security policy was formally modelled and proven consistent with the functional specifications by means of an interactive theorem prover. The formalisms were used to assist in the design of the security architecture. Keywords : ITSEC, formal methods, security policy

• Type: Conference
• Year: 1996
• Where: ACSAC
• Authors: Pierre Bieber
• Keywords: ACSAC 1996, Interactive Theorem Prover, ITSEC E4 Requirements, Security Policy, Security Privacy