Understanding the correctness of cryptographic authenticity protocols is a difficult problem. We propose a new method for verifying authenticity properties of protocols based on symmetric-key cryptography. First, we code the protocol in the spi calculus of Abadi and Gordon. Second, we specify authenticity properties expected of the protocol by annotating the code with correspondence assertions in the style of Woo and Lam. Third, we figure out types for the keys, nonces, and messages of the protocol. Fourth, we mechanically check that the spi calculus code is well-typed. We have a type safety result that ensures that any well-typed program is robustly safe. 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 led us to the identification of problems in an authentication protocol due to Woo and Lam, previously discovered by Abadi, Anderson and Needham.
Gates 4B, 12/12/00, 4:15 PM