We constructed a formal specification for sending secure Internet e-mail using Multilevel Information System Security Initiative (MISSI). We used formal language PROMELA, based on Hoare's CSP. We verified the model using AT&T's automated model checker SPIN. We propose a software engineering approach where we translate from English to pseudocode to a process algebra specification, verify the specification, and discover ambiguities, omissions, and errors in the English description. This work shows that formal methods can be used to speed up and clarify the software engineering process. It took eight weeks to choose SPIN among several tools, learn SPIN and MISSI, and produce and verify a sender model. We later added a local cache specification. The complexity of the process is intensified by starting from the purely English- and figure-based original specification, which relies on many separate documents and standards that operate together.

The paper compares and contrasts various methods presently available for specification, validation and verification, with emphasis on verification. We describe an application of formal methods to protocol specification, validation, and verification, using an actual protocol as an example. We use a process algebra to build models of an OSI protocol and test these models using a model checker. Model checking allows us to verify large and complex models and use formal methods as practical solutions. We also show an example with an automated theorem prover.