×

An attack-finding algorithm for security protocols. (English) Zbl 1057.68006

Summary: This paper proposes an automatic attack construction algorithm in order to find potential attacks on security protocols. It is based on a dynamic strand space model, which enhances the original strand space model by introducing active nodes on strands so as to characterize the dynamic procedure of protocol execution. With exact causal dependency relations between messages considered in the model, this algorithm can avoid state space explosion caused by asynchronous composition. In order to get a finite state space, a new method called strand-added on demand is exploited, which extends a bundle in an incremental manner without requiring explicit configuration of protocol execution parameters. A finer granularity model of term structure is also introduced, in which subterms are divided into check subterms and data subterms. Moreover, data subterms can be further classified based on the compatible data subterm relation to obtain automatically the finite set of valid acceptable terms for an honest principal. In this algorithm, terms core is designed to represent the intruder’s knowledge compactly, and forward search technology is used to simulate attack patterns easily. Using this algorithm, a new attack on the Dolve-Yao protocol can be found, which is even more harmful because the secret is revealed before the session terminates.

MSC:

68M10 Network design and communication in computer systems
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Lowe G. An attack on the Needham-Schroeder public key authentication protocol.Information Processing Letters, 1995, 56(3): 131–136. · Zbl 0875.94114
[2] Gritzalis S, Spinellis D, Georgiadis P. Security protocols over open networks and distributed systems: Formal methods for their analysis, design, and verification.Computer Communications 1999, 22(8): 695–707. · Zbl 05396456
[3] Burrows M, Abadi M, Needham R. A logic of authentication.ACM Transactions on Computer Systems, 1990, 8(1): 18–36. · Zbl 0687.68007
[4] Gong L, Needham R, Yahalom R. Reasoning about belief in cryptographic protocols. InProceedings of the IEEE 1990 Symp. on Security and Privacy, Oakland, California, May, 1990, pp.234–248.
[5] Kindred D. Theory generation for security protocols [Dissertation]. Carnegie Mellon University, 1999.
[6] Brackin S. Automatically detecting most vulnerabilities in cryptographic protocols. In the DARPA Information. Survivability Conference and Exposition, 2000, 1: 222–236.
[7] Mitchell J C, Mitchell M, Stern U. Automated analysis of cryptographic protocols, using Murø InProceedings of the 1997 IEEE Symposium on Security and Privacy, IEEE Computer Society Press, 1997, pp.141–151.
[8] Clarke E M, Jha S, Marrero W. Using state space exploration and a natural deduction style message derivation engine to verify security protocols. InProceedings of the IFIP Working, Conference on Programming Concepts and Methods, New York, 1998.
[9] Lowe G. Breaking and fixing the Needham-Schroeder public-key protocol using FDR. InTools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science 1055, Springer-Verlag, 1996, pp.147–166.
[10] Song D. Athena: A new efficient automated checker for security protocol analysis. InProceedings of 12th IEEE Computer Security Foundations Workshop, IEEE Computer Society Press, June, 1999, pp.192–202.
[11] Paulson L. Proving properties of security protocols by induction. InProceedings of the 1997 IEEE Symposium on Research in Security and Privacy, 1997, pp.70–83.
[12] Thayer J F, Herzog J C, Guttman J D. Strand spaces: Proving security protocols correct.Journal of Computer Security, 1999.
[13] Thayer J F, Herzog J C, Guttman J D. Strand space: Why is a security protocol correct? InProceedings of 1998 IEEE Symposium on Security and Privacy, 1998, pp.160–171.
[14] Woo T, Lam S. A semantic model for authentication protocols. InProc. 14th IEEE Symposium on Research in Security and Privacy, Oakland: IEEE Computer Society Press, 1993, pp.178–194.
[15] Clark J, Jacob, J. A survey of authentication protocol literature. Available at: http://www.cs.york.ac.uk/-jac/papers/drareviewps.ps, 1997.
[16] Thayer J F, Herzog J C, Guttman J D. Strand space pictures InWorkshop on Formal Methods and Security Protocols, Indianapolis, Indiana, 1998.
[17] Ding Y. A Lazy Approach to Model Checking Authentication Protocols with ”Black Boxes”. Available at: http://www.comp.nus.edu.sg/\(\sim\)dingyq.
[18] Mitchell J C, Shmatikov V, Stern U. Finite-state analysis of SSL 3.0. InSeventh USENIX Security Symposium, San Antonio, 1998, pp.201–216.
[19] Abadi M, Needham R. Prudent engineering practice for cryptographic protocols.IEEE Transactions on Software Engineering, 1996 22(1): 5–15. · Zbl 05113217
[20] Hopper N J, Seshia S A, Wing J M. Combining theory generation and model checking for security protocol analysis. Technical Report CMU-CS-00-107, Carnegie Mellon University, 2000.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.