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.
|Title of host publication||Proceedings of the 16th Computer Security Foundations Workshop (CSFW 03).|
|Publisher||IEEE Computer Society Press|
|Publication status||Published - 2003|