Automatic Validation of Protocol Narration

Chiara Bodei, Mikael Buchholtz, Pierpablo Degano, Flemming Nielson, Hanne Riis Nielson

AbstractWe 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.
TypeConference paper [With referee]
ConferenceProceedings of the 16th Computer Security Foundations Workshop (CSFW 03).
Year2003    pp. 126-140
PublisherIEEE Computer Society Press
BibTeX data [bibtex]
IMM Group(s)Computer Science & Engineering