Abstract: Cryptographic protocols are the thread that knits together the security of the Internet. Thus it is important that they be correct. This is especially true for the design of the protocol. Although implementation errors are more common, design errors are harder to fix, especially for protocols, which must be both interoperable and widely deployed, making them difficult to redesign and redistribute on the fly. Indeed, even protocols with known flaws may remain deployed for a long time in order to support communication with legacy systems. For this reason, it is important to get a protocol right the first time. But since cryptographic protocols must be designed to operate in the face of an active attacker working to subvert their goals, this is not an easy problem.
One way of assuring correctness that has seen great success is the use of formal verification based on automated search techniques. One reason for this success has been the simple but powerful paradigm developed by Dolev and Yao in the late 70's and early 80's. In this paradigm messages are represented by symbolic terms constructed out of constants, function symbols, and variables. Furthermore, the network is controlled by an intruder who can intercept, destroy, and redirect traffic, and create and send messages of its own. Thus, we can think of the protocol as a distributed program for generating elements of a term algebra, defined by a set of rules that define actions executed by the intruder, and a set of rules describing actions executed by the honest principals.
Although the basic Dolev-Yao model is well-understood, it becomes more complex when we take into account the equational properties underlying the cryptoalgorithms used in the protocol, e.g. the axioms governing Abelian groups. However, it is necessary to do this, not only to faithfully represent the protocol, but in order to reason about the possible actions of an attacker. Thus, representation and reasoning about equational properties has been an active area of research. In this talk we will give an overview of research in this area, and present the approach used by a particular tool, the Maude-NRL Protocol Analyzer (Maude-NPA).