Hash Gone Bad: Automated discovery of protocol attacks that exploit hash function weaknesses
Vincent Cheval, Cas Cremers, Alexander Dax, Lucca Hirschi, Charlie Jacomme, and Steve Kremer. Hash Gone Bad: Automated discovery of protocol attacks that exploit hash function weaknesses. In 32nd USENIX Security Symposium (USENIX Security'23), USENIX Association, Anaheim, CA, USA, August 2023. Distinguished paper award.
Download
Abstract
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.
BibTeX
@inproceedings{CCDHJK-usenix23,
abstract = {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.
\par
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.
\par
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.
},
address = {Anaheim, CA, USA},
author = {Cheval, Vincent and Cremers, Cas and Dax, Alexander and Hirschi, Lucca and Jacomme, Charlie and Kremer, Steve},
booktitle = {32nd USENIX Security Symposium ({USENIX}
Security'23)},
month = aug,
publisher = {{USENIX} Association},
title = {Hash Gone Bad: Automated discovery of protocol attacks that exploit hash function weaknesses},
year = 2023,
acronym = {{USENIX} Security'23},
nmonth = 8,
note = {\textbf{\href{https://www.usenix.org/conferences/best-papers?taxonomy_vocabulary_1_tid=2023&title_1=Sec}{Distinguished paper award}}},
}