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 theorems must be proved guarantee cryptographic facility satisfies invariants automatically generated by system. A specification of an example system presented, several weaknesses were revealed attempting verify test formally discussed. >