16th IEEE Computer Security Foundations Workshop (CSFW'03)
Automatic Validation of Protocol Narration
Pacific Grove, California
June 30-July 02
ISBN: 0-7695-1927-X
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.
Citation:
C. Bodei, M. Buchholtz, P. Degano, F. Nielson, H. Riis Nielson, "Automatic Validation of Protocol Narration," csfw, pp.126, 16th IEEE Computer Security Foundations Workshop (CSFW'03), 2003