Using Formal Verification Techniques to Analyze Encryption Protocols

This paper presents an approach to analyzing Encryption protocols using machine aided formal verification techniques. The desirable properties that a protocol is to preserve are expressed as state invariants and the theorems that need to be proved to guarantee that the cryptographic facility satisfies the invariants are automatically generated by the verification system. A formal specification of an example system is presented, and a weakness that was revealed by testing the formal specification is discussed.