Analyzing encryption protocols using formal verification techniques

An approach to analyzing encryption protocols using machine-aided formal verification techniques is presented. The properties that the protocol should preserve are expressed as state invariants, and the theorems that must 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 several weaknesses that were revealed by attempting to verify and test the specification formally are discussed.