Verifying Privacy Enhanced Mail Functions with Higher Order Logic


Dan Zhou and Shiu-Kai Chin
Dept. of Electrical Engineering & Computer Science
Syracuse University, Syracuse, NY 13244
{danzhou | chin}@cat.syr.edu http://www.cat.syr.edu/~chin

Security properties such as privacy, authentication, and integrity are of increasing importance to networked systems. We show how the message structure of Privacy Enhanced Mail (PEM) and the functions on PEM structures have the desired security properties. Higher-order logic and the HOL theorem-prover are used to precisely relate security properties to implementation specifications. Once the specifications are proved to have the desired security properties, they are passed on to software engineers for implementation.