Automatic Validation of Protocol Narration

We perform a systematic expansion of protocol narrations into terms of a process algebra in order to make precise some of the detailed checks that need to be made in a protocol. We then apply static analysis technology to develop an automatic validation procedure for protocols. Finally, we demonstrate that these techniques suffice for identifying a number of authentication flaws in symmetric key protocols such as Needham-Schroeder, Otway-Rees, Yahalom and Andrew Secure RPC.

• Type: Conference
• Year: 2003
• Where: CSFW
• Authors: Chiara Bodei, Mikael Buchholtz, Pierpaolo Degano, Flemming Nielson, Hanne Riis Nielson
• Keywords: Automatic Validation Procedure, CSFW 2003, Protocol Narrations, Security Privacy, Symmetric Key Protocols