Authenticity by Typing in Security Protocols

Andrew D. Gordon, Microsoft Research
Joint work with Alan Jeffrey, DePaul University

Understanding the correctness of cryptographic authentication protocols is a
difficult problem.  We propose a new method for verifying authenticity
properties of protocols based on symmetric-key cryptography.  First, code up
the protocol in the spi calculus of Abadi and Gordon.  Second, specify
authenticity properties expected of the protocol 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.  It is feasible to apply this
method by hand to several well-known cryptographic protocols.  Hence the
method is considerably more efficient than previous analyses of authenticity
for the spi calculus.  Moreover, the types for protocol data serve as
informative documentation of how the protocol works.  Our method has led us
to the independent rediscovery of flaws in existing protocols and has helped
the design of new protocols.