Formal Verification of Security Properties of Privacy Enhanced Mail
Abstract
The increased use of networked and distributed computing makes security a major concern. The capability to verify that a system meets its security requirements will continue to grow in importance. In particular, the capability to assign security properties to engineering structures is crucial. This work focuses on verifying the security properties of Privacy Enhanced Mail (PEM). Security properties such as non-repudiation, privacy, authentication, and integrity are defined independently of any implementation structure. PEM message structures and operations on those structures are shown to have the desired security properties. All formal definitions and proofs of security properties are done using the Higher Order Logic theorem prover. This work on PEM shows the feasibility of using formal logic and computer assisted reasoning tools to describe and verify relatively complex systems.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jun 01, 1998
- Accession Number
- ADA349807
Entities
People
- Dan Zhou
- Shiu-kai Chin
Organizations
- Syracuse University