An Attack-Finding Algorithm for Security Protocols

This paper proposes an automatic attack construction algorithm in order to find potential attacks on ecurity 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 explo-sion 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 beeause the secret is revealed before the session terminates.

An attack-finding algorithm for security protocols

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. Supported by the National S219 Engineering under Grant No.2000-A32-09. LIU Dongxi was born in 1973. He received his B.S. and M.S. degrees in computer science from Taiyuan University of Technology in 1996 and 1999 respectively. Now he is a Ph.D. candidate in the Department of Computer Science and Technology, Shanghai Jiaotong University. His research interests concentrate on security protocols, model checking and software architecture in router. LI Xiaoyong was born in 1972. He received his B.S. and M.S. degrees in computer science from University of Electronic Science and Technology of China in 1993 and 1999. Now he is a Ph.D. candidate in the Department of Computer Science and Technology, Shanghai Jiaotong University. His research interests include intrusion detection, router architecture and Linux. BAI Yingcai received his B.S. degree from Tsinghua University in 1961. Now he is a professor as well as a Ph.D. Supervisor in the Department of Computer Science and Technology, Shanghai Jiaotong University. He has published more than 96 papers and 43 books on computer network, and has received 16 awards for his research. His research interests include network management, router architecture, network security and network storage technology.