Automated analysis of cryptographic protocols using Murφ
- 22 November 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
A methodology is presented for using a general-purpose state enumeration tool, Mur/spl phi/, 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/spl phi/ 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
This publication has 12 references indexed in Scilit:
- Modelling and verifying key-exchange protocols using CSP and FDRPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Security properties and CSPPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1996
- State reduction using reversible rulesPublished by Association for Computing Machinery (ACM) ,1996
- Verifying systems with replicated components in murϕPublished by Springer Nature ,1996
- System Design Methodology of UltraSPARC™ -IProceedings of the 39th conference on Design automation - DAC '02, 1995
- Automatic verification of the SCI cache coherence protocolPublished by Springer Nature ,1995
- The Kerberos Network Authentication Service (V5)Published by RFC Editor ,1993
- Non-malleable cryptographyPublished by Association for Computing Machinery (ACM) ,1991
- Key Distribution Protocol for Digital Mobile Communication SystemsPublished by Springer Nature ,1990
- Using encryption for authentication in large networks of computersCommunications of the ACM, 1978