Affiliations: [a] Microsoft Research, 7 J.J. Thomson Ave., Cambridge CB3/0FB, UK | [b] CTI, DePaul University, 243 S. Wabash Ave., Chicago, IL 60604, USA
Note: [1] A portion of this work appeared in the proceedings of the 14th IEEE Computer Security Foundations Workshop (CSFW14), Cape Breton, USA, 11–13 June, 2001. The two authors completed part of this work at Microsoft Research in Cambridge and part at DePaul University in Chicago.
Abstract: We propose a new method to check authenticity properties of cryptographic protocols. First, code up the protocol in the spi-calculus of Abadi and Gordon. Second, specify authenticity properties by annotating the code with correspondence assertions in the style of Woo and Lam. Third, figure out types for the keys, nonces, and messages of the protocol. Fourth, check that the spi-calculus code is well-typed according to a novel type and effect system presented in this paper. Our main theorem guarantees that any well-typed protocol is robustly safe, that is, its correspondence assertions are true in the presence of any opponent expressible in spi. It is feasible to apply this method by hand to several well-known cryptographic protocols. It requires little human effort per protocol, puts no bound on the size of the opponent, and requires no state space enumeration. Moreover, the types for protocol data provide some intuitive explanation of how the protocol works. This paper describes our method and gives some simple examples. Our method has led us to the independent rediscovery of flaws in existing protocols and to the design of improved protocols.
