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.