Abstract
Security properties such as privacy, authentication, and integrity are of increasing importance to networked systems. Systems with security requirements typically must operate with a high degree of confidence, i.e. they must be highly assured. We show how the message structure of Privacy Enhanced Mail (PEM) and the operations on PEM structures have the desired implementation-independent security properties. The verification of an integrity checking function is shown in detail. Higher-order logic and the HOL theorem-prover are used to precisely relate security properties to implementation specifications.
Original language | English (US) |
---|---|
Title of host publication | Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS |
Publisher | IEEE Computer Society |
Pages | 344-351 |
Number of pages | 8 |
State | Published - 1996 |
Event | Proceedings of the 1996 2nd IEEE International Conference on Engineering of Complex Computer Systems - Montreal, Can Duration: Oct 21 1996 → Oct 25 1996 |
Other
Other | Proceedings of the 1996 2nd IEEE International Conference on Engineering of Complex Computer Systems |
---|---|
City | Montreal, Can |
Period | 10/21/96 → 10/25/96 |
ASJC Scopus subject areas
- General Computer Science
- General Engineering