Authenticity by typing for security protocols
Andrew D. Gordon, Alan Jeffrey · 2005
We propose a new method to check authenticity proper-ties 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 corre-spondence 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 express-ible in spi. 1 Verifying Correspondences by Typing Spi We propose a new method for analysing authenticity