An Attack-Finding Algorithm for Security Protocols

This paper proposes an automatic attack constructionalgorithm in order to find potential attacks on security protocols. Itis based on a dynamic strand space model, which enhances the originalstrand space model by introducing active nodes on strands so as tocharacterize the dynamic procedure of protocol execution. With exactcausal dependency relations between messages considered in the model,this algorithm can avoid state space explosion caused by asynchronouscomposition. In order to get a finite state space, a new method calledstrand-added on demand is exploited, which extends a bundle in anincremental manner without requiring explicit configuration of protocolexecution parameters. A finer granularity model of term structure isalso introduced, in which subterms are divided into check subterms anddata subterms. Moreover, data subterms can be further classifiedbased on the compatible data subterm relation to obtain automaticallythe finite set of valid acceptable terms for an honest principal. Inthis algorithm, terms core is designed to represent the intruder'sknowledge compactly, and forward search technology is used to simulateattack patterns easily. Using this algorithm, a new attack on the Dolve-Yaoprotocol can be found, which is even more harmful because the secret isrevealed before the session terminates.