Title: Authenticity by typing for security protocols
Abstract: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 propert...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.Read More
Publication Year: 2005
Publication Date: 2005-08-29
Language: en
Type: article
Indexed In: ['crossref']
Access and Citation
Cited By Count: 106
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot