Paper 2022/1314

Hash Gone Bad: Automated discovery of protocol attacks that exploit hash function weaknesses

Vincent Cheval, Inria Paris
Cas Cremers, CISPA Helmholtz Center for Information Security
Alexander Dax, CISPA Helmholtz Center for Information Security
Lucca Hirschi, Inria & LORIA
Charlie Jacomme, Inria Paris
Steve Kremer, Inria & LORIA

Most cryptographic protocols use cryptographic hash functions as a building block. The security analyses of these protocols typically assume that the hash functions are perfect (such as in the random oracle model). However, in practice, most widely deployed hash functions are far from perfect -- and as a result, the analysis may miss attacks that exploit the gap between the model and the actual hash function used. We develop the first methodology to systematically discover attacks on security protocols that exploit weaknesses in widely deployed hash functions. We achieve this by revisiting the gap between theoretical properties of hash functions and the weaknesses of real-world hash functions, from which we develop a lattice of threat models. For all of these threat models, we develop fine-grained symbolic models. Our methodology's fine-grained models cannot be directly encoded in existing state-of-the-art analysis tools by just using their equational reasoning. We therefore develop extensions for the two leading tools, Tamarin and Proverif. In extensive case studies using our methodology, the extended tools rediscover all attacks that were previously reported for these protocols and discover several new variants.

Available format(s)
Publication info
Published elsewhere. USENIX 2023
Hash collisions Symbolic models Proverif Tamarin automation formal analysis
Contact author(s)
vincent cheval @ inria fr
cremers @ cispa de
alexander dax @ cispa de
lucca hirschi @ inria fr
charlie jacomme @ inria fr
steve kremer @ inria fr
2022-10-05: approved
2022-10-04: received
See all versions
Short URL
Creative Commons Attribution


      author = {Vincent Cheval and Cas Cremers and Alexander Dax and Lucca Hirschi and Charlie Jacomme and Steve Kremer},
      title = {Hash Gone Bad: Automated discovery of protocol attacks that exploit hash function weaknesses},
      howpublished = {Cryptology ePrint Archive, Paper 2022/1314},
      year = {2022},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.