Title :
Automated analysis of cryptographic protocols using Murφ
Author :
Mitchell, John C. ; Mitchell, Mark ; Stern, Ulrich
Author_Institution :
Dept. of Comput. Sci., Stanford Univ., CA, USA
Abstract :
A methodology is presented for using a general-purpose state enumeration tool, Murφ, to analyze cryptographic and security-related protocols. We illustrate the feasibility of the approach by analyzing the Needham-Schroeder (1978) protocol, finding a known bug in a few seconds of computation time, and analyzing variants of Kerberos and the faulty TMN protocol used in another comparative study. The efficiency of Murφ also allows us to examine multiple terms of relatively short protocols, giving us the ability to detect replay attacks, or errors resulting from confusion between independent execution of a protocol by independent parties
Keywords :
client-server systems; cryptography; network operating systems; protocols; Kerberos; Murφ; client server system; computation time; cryptographic protocol analysis; errors; faulty TMN protocol; general-purpose state enumeration tool; methodology; network operating system; replay attack detection; security-related protocols; Authentication; Computer science; Contracts; Cryptographic protocols; Cryptography; Documentation; Failure analysis; NASA; Public key; US Government;
Conference_Titel :
Security and Privacy, 1997. Proceedings., 1997 IEEE Symposium on
Conference_Location :
Oakland, CA
Print_ISBN :
0-8186-7828-3
DOI :
10.1109/SECPRI.1997.601329
