A Formal Semantics for Evaluating Cryptographic Protocols

Secure communication is largely dependent on effective application of cryptography. While cryptographic methods have been investigated to ensure confidence in the security of the encryption algorithm, many cryptographic schemes are vulnerable to attack because the protocols used to implement communication in a cryptographic environment do not meet their intended goals. Cryptographic protocols, like software, are very difficult to verify. Recent research is aimed at finding methods of verifying cryptographic protocols. Though no method has achieved widespread acceptance and use, the most prevalent class of cryptographic protocol evaluation techniques is based on application of epistemic logical systems to reason about the protocols. In this dissertation we present a methodology for verifying cryptographic protocols based on the classical program verification technique of Weakest Precondition reasoning [DIJK76] and a set of tools to automate application of the method. The methodology solves many problems of existing methods by formalizing the meaning of the messages in a protocol session and by including message sequencing in the protocol definition. The proposed method can also be combined with logical methods to construct a more thorough cryptographic protocol evaluation technique.