Copyright Notice:
The publication copies distributed in this site are
provided to ensure timely dissemination of scholarly and technical
work. Copyright and all rights therein are retained by authors or by
other copyright holders (as explicitly indicated). All persons copying
this information are expected to adhere
to the terms and constraints invoked by each copyright. In
most cases, these works may not be reposted without the explicit
permission of the copyright holder
Ivan Cibrario Bertolotti, Luca Durante, Riccardo Sisto, Adriano Valenzano,
Automatic Detection of Attacks on Cryptographic Protocols: a Case Study,
in DIMVA 2005: 2nd Int. Conf. on Detection of Intrusions and Malware and Vulnerability Assessment, Vienna, Austria, July 2005, Springer, pp. 69-84.
©2005 Springer
doi: 10.1007/11506881_5
Abstract
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.
Back to Riccardo Sisto's publications