Synthesising attacks on cryptographic protocols

Abstract

This paper presents a new algorithm for synthesising attacks on cryptographic protocols. The algorithm constructs attacks where the attacker interacts with the agents in the system in order to discover some set of restricted information or send a specific message to another participant in the protocol. This attacker is akin to the Dolev-Yao model of attacker but behaves in a manner that does not betray its presence in the system. The state space reduction heuristics used in the algorithm manage the growth of the state space through the use of strict typing and by only allowing protocol specifications that do not deadlock. The cryptographic protocols are specified in the spi calculus. The variant of the spi calculus used is a syntactically restricted variant which is semantically equivalent to the full spi calculus. A model checker based on this algorithm has been implemented, and the results of this model checker on common cryptographic protocols are presented. This technique can be used to quickly search for an attack on a protocol. The knowledge of the structure of such an attack will enable the protocol designers to repair the protocol. Keywords: cryptographic protocols, security, model checking © Springer-Verlag 2004.