DocumentCode
1649886
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
fYear
2003
Firstpage
126
Lastpage
140
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Computer Security Foundations Workshop, 2003. Proceedings. 16th IEEE
ISSN
1063-6900
Print_ISBN
0-7695-1927-X
Type
conf
DOI
10.1109/CSFW.2003.1212709
Filename
1212709
Link To Document