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.