Formal Verification of Security Properties of Privacy Enhanced Mail
Shiu‐Kai Chin, Dan Zhou · 1998
this document is to describe in detail how security properties are related to secure electronic mail message formats and operations. We show how system-level security properties are satisfied by functional specifications of operations on specific message formats. Our formal analysis is based on the Internet Privacy Enhanced Mail (PEM) described in four Request for Comment (RFC) papers: RFC 1421, RFC 1422, RFC 1423, and RFC 1424, [9, 8, 1, 7]. PEM is similar to military systems such as the National Security Agency's Multilevel Information Systems Security Initiative (MISSI). MISSI is based in part on PEM. While the message field names and structure may differ somewhat between MISSI and PEM, the analytical techniques used here are applicable to both. We use several means of description. Informal descriptions are used to give an intuitive notion of behavior, properties, or requirements. These are derived from the above-cited documents. Formal descriptions are derived from the informal descriptions. These are intended to be precise descriptions of behavior which are subject to rigorous analysis. The types of analysis done includes correctness -- e.g. ensuring requirements are met, and behavioral properties -- e.g. security properties. Our formal descriptions focus on: ffl Structure of well-formed messages.