Automatic validation of protocol narration
Chiara Bodei, Mikael Buchholtz, Pierpaolo Degano, Flemming Nielson, Hanne Riis Nielson · 2004
We perform a systematic expansion of protocol narrations into terms of 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.