Automatic Detection of Attacks on Cryptographic Protocols: a Case Study

Recently, a new verification tool for cryptographic protocols called S3A (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 S3A 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 S3A makes it very difficult to spot by hand, thus showing the usefulness of analyis tools of this kind in real-world protocol analysis.