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

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. 2 128 ✓ 2 256 ✗ SHA2-512 2001 TLS, SSL, SSH, S/MIME, IPSec, DNSSEC, Linux/Unix password hashing ✓ 2 256 ✓ 2 512 ✗ SHA3-256 2012 Ethereum ✓ 2 128 ✓ 2 256 ✓ ✓= currently still secure ⊗=weak, but no full attack yet ✗= known attack * = Theoretical attacks on (second) preimage resistance were found [54] [44], but they are still not feasible. ** = The small bit size allows to find collisions in practice, but doing so is not necessarily feasible. Table 1 : Examples of widely used hash functions that are currently deployed in security protocols and do not offer perfect (randomoracle like) guarantees. The numbers indicate the complexity of the currently best known attack on the property [32, 44, 45, 53, 54] . For the hash functions currently deemed secure the best known attacks would be a brute-force approach; e.g., the complexity to break collision resistance on SHA2-256 is 2 128 . Crucially, this situation is not constant, but expected to get worse: history suggests that the numbers for the best attacks are likely to decrease over time for all hashes, see e.g., [2, 48] . This raises the natural question: how can we check if a protocol using a hash function with a particular weakness meets its security guarantees? History has shown such attacks are rare but can be very subtle, e.g., [9, 48, 49] , and thus difficult to detect manually. From a cryptographic perspective, the answer would be: provide a computational proof of the security of the entire protocol, and if this proof relies on assumptions not met by the hash function, this may indicate an attack. However, for most protocols, this task ranges from daunting to infeasible; and most existing protocol proofs simply assume that the hash function is perfect, by using the ROM. In contrast, automated protocol analysis tools have shown to be effective for analyzing real-world protocols [5, 6, 8, 16, 18, 28] . However, they model hash functions as being perfect (traditionally as an operator in a free term algebra). Thus, like computational proofs that use the ROM, such analyses miss any attacks that exploit the use of a non-perfect hash function. In this work, we revisit cryptographic hash function definitions, common weaknesses, and the potential attacker capabilities that arise from them. Based on this, we develop a methodology to systematically discover attacks on protocols that exploit their use of "less-than-perfect" hash functions, and show how this can be implemented in the two leading protocol-analysis tools. To realize this, we both exploit advanced features of these tools (such as equational theories, event-based modeling, and restrictions) but we in fact also extend them (partial support for associative operators, recursive computation functions). Our methodology can be used in the design phase to avoid the use of hash functions that are too weak, or to find and fix problems in deployed protocols. Contributions. 1. We develop the first systematic, automated methodology to find protocol attacks that exploit weaknesses of real-world hash functions. At a technical level, we achieve this by symbolically modeling cryptographic weaknesses (i.e., the lack of desirable cryptographic properties) as well as real-world attack classes that are not captured by classical security definitions for cryptographic hash functions. 2. We automate our methodology in the two leading automated protocol analysis tools, TAMARIN and PROVERIF. To achieve this, we (a) propose dedicated modeling techniques, and (b) extend both tools with new required features that are of independent interest beyond this work. 3. We apply our methodology to over 20 protocols, automatically rediscovering all previously reported attacks on those protocols that exploit weak hash functions, as well a