Automated analysis of cryptographic protocols using Murφ Export

@inproceedings{citeulike:3855639, 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}, author = {Mitchell, J. C. and Mitchell, M. and Stern, U.}, booktitle = {Security and Privacy, 1997. Proceedings., 1997 IEEE Symposium on}, citeulike-article-id = {3855639}, citeulike-linkout-0 = {http://dx.doi.org/10.1109/SECPRI.1997.601329}, citeulike-linkout-1 = {http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=601329}, doi = {10.1109/SECPRI.1997.601329}, journal = {Security and Privacy, 1997. Proceedings., 1997 IEEE Symposium on}, keywords = {copy, cryptography, model-checking, security}, pages = {141--151}, posted-at = {2009-01-07 02:50:57}, priority = {2}, title = {Automated analysis of cryptographic protocols using Mur\φ}, url = {http://dx.doi.org/10.1109/SECPRI.1997.601329}, year = {1997} }

TY - CONF ID - citeulike:3855639 L3 - citeulike-article-id:3855639 N2 - 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 JF - Security and Privacy, 1997. Proceedings., 1997 IEEE Symposium on EP - 151 TI - Automated analysis of cryptographic protocols using Murφ T2 - Security and Privacy, 1997. Proceedings., 1997 IEEE Symposium on SP - 141 KW - copy KW - cryptography KW - model-checking KW - security AU - Mitchell, JC AU - Mitchell, M AU - Stern, U PY - 1997/// UR - http://dx.doi.org/10.1109/SECPRI.1997.601329 ER -