Title :
Automatic validation of protocol narration
Author :
Bodei, C. ; Buchholtz, M. ; Degano, P. ; Nielson, H. Riis ; Riis Nielson, H.
Author_Institution :
Dipt. di Informatica, Universita di Pisa, Italy
Abstract :
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.
Keywords :
access protocols; data flow analysis; message authentication; process algebra; public key cryptography; Andrew Secure RPC key protocol; Needham-Schroeder key protocol; Otway-Rees key protocol; Yahalom key protocol; authentication flaw; automatic validation; process algebra; protocol narration; static analysis; symmetric key protocol; systematic expansion; Algebra; Artificial intelligence; Authentication; Cryptography; Informatics; Internet; Mathematical model; Protocols; Security; Testing;
Conference_Titel :
Computer Security Foundations Workshop, 2003. Proceedings. 16th IEEE
Print_ISBN :
0-7695-1927-X
DOI :
10.1109/CSFW.2003.1212709
