A Method For Examining Cryptographic Protocols

In this dissertation we present a powerful, general, extensible, and formal methodology that automatically examines cryptographic protocols. Our approach is to specify a protocol, its assumptions, and a statement of failure in a notation that allows us to give a formal semantic definition of the protocol and its failure conditions. We then use deductive program synthesis to try to automatically modify the protocol so that the failure condition is achieved. If this last step succeeds, we have found a weakness in the protocol and we can then give a step-by-step description of an attack to the user. Given an adequate set of axioms and enough time, our method will find any attack that exists for a given protocol and failure condition. Even if our methodology does not discover a flaw in the amount of time it is given to run, we can make a concrete statement about the minimum length of a constructive proof for any attack that might exist on the protocol (for the given failure condition and axiom set) as a result of its analysis. A preliminary implementation of our methodology has had great success in finding both known and previously unknown flaws in a significant number of published protocols. This system also helped us to discover and demonstrate an important new class of attacks based on the interaction of two or more cryptographic protocols.