Authenticity by Typing for Security Protocols
Andy Gordon, Microsoft Research
Based on joint work with Alan Jeffrey, DePaul University

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 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. Our method has led us to the independent 
rediscovery of flaws in existing protocols and to the design of 
improved protocols.

The talk describes our method and gives some simple examples. 
A paper describing the method appears in the proceedings of the 
14th IEEE Computer Security Foundations Workshop, June 11--13, 2001.