loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
1997 IEEE Symposium on Security and Privacy
Automated analysis of cryptographic protocols using Mur/spl phi/
Oakland, CA
May 04-May 07
ISBN: 0-8186-7828-3
ASCII Text
x 
 
J.C. Mitchell, M. Mitchell, U. Stern, "Automated analysis of cryptographic protocols using Mur/spl phi/," Security and Privacy, IEEE Symposium on, pp. 0141, 1997 IEEE Symposium on Security and Privacy, 1997.
 
 
BibTex
x
 
@article{ 10.1109/SECPRI.1997.601329,
author = {J.C. Mitchell and M. Mitchell and U. Stern},
title = {Automated analysis of cryptographic protocols using Mur/spl phi/},
journal ={Security and Privacy, IEEE Symposium on},
volume = {0},
year = {1997},
issn = {1540-7993},
pages = {0141},
doi = {http://doi.ieeecomputersociety.org/10.1109/SECPRI.1997.601329},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Security and Privacy, IEEE Symposium on
TI - Automated analysis of cryptographic protocols using Mur/spl phi/
SN - 1540-7993
SP
EP
A1 - J.C. Mitchell,
A1 - M. Mitchell,
A1 - U. Stern,
PY - 1997
KW - cryptography; cryptographic protocol analysis; Mur/spl phi/; methodology; general-purpose state enumeration tool; security-related protocols; computation time; Kerberos; faulty TMN protocol; replay attack detection; errors; client server system; network operating system
VL - 0
JA - Security and Privacy, IEEE Symposium on
ER -
 
J.C. Mitchell, Dept. of Comput. Sci., Stanford Univ., CA, USA
M. Mitchell, Dept. of Comput. Sci., Stanford Univ., CA, USA
U. Stern, Dept. of Comput. Sci., Stanford Univ., CA, USA
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.
Index Terms:
cryptography; cryptographic protocol analysis; Mur/spl phi/; methodology; general-purpose state enumeration tool; security-related protocols; computation time; Kerberos; faulty TMN protocol; replay attack detection; errors; client server system; network operating system
Citation:
J.C. Mitchell, M. Mitchell, U. Stern, "Automated analysis of cryptographic protocols using Mur/spl phi/," sp, pp.0141, 1997 IEEE Symposium on Security and Privacy, 1997
Usage of this product signifies your acceptance of the Terms of Use.