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

fYear

1997

fDate

4-7 May 1997

Firstpage

141

Lastpage

151

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Security and Privacy, 1997. Proceedings., 1997 IEEE Symposium on

Conference_Location

Oakland, CA

ISSN

1081-6011

Print_ISBN

0-8186-7828-3

Type

conf

DOI

10.1109/SECPRI.1997.601329

Filename

601329