Automatic detection of attacks on cryptographic protocols: A case study

Abstract

Recently, a new verification tool for cryptographic protocols called S 3 A (Spi Calculus Specifications Symbolic Analyzer) has been developed, which is based on exhaustive state space exploration and symbolic data representation, and overcomes most of the limitations of previously available tools. In this paper we present some insights on the ability of S 3 A to detect complex type flaw attacks, using a weakened version of the well-known Yahalom authentication protocol as a case study. The nature of the attack found by S 3 A makes it very difficult to spot by hand, thus showing the usefulness of analyis tools of this kind in real-world protocol analysis. © Springer-Verlag Berlin Heidelberg 2005.