Hash Functions Vulnerabilities
Hash functions are extensively used as key components in cryptographic protocols. However, most existing symbolic analyses assume the Random Oracle Model (ROM), abstracting hash functions as ideal black boxes. In our work [1], we move beyond this abstraction by analyzing two representative protocols under more realistic models that incorporate algebraic properties of hash functions to represent known vulnerabilities.
The protocols analyzed are:
- A variant of the Sign-and-MAC (SIGMA) protocol [2], whose structure closely resembles widely deployed protocols such as TLS and SSH.
- The Meadows Distance Bounding protocol [3], instantiated with the function \( F(N_V, P, N_P) = N_V \oplus H(P \parallel N_P) \).
Hash function vulnerabilities considered:
Given a hash function \( H: \{0,1\}^* \rightarrow \{0,1\}^{\ell(n)} \), we modeled the following vulnerabilities:
- Second Preimage (2ndPreImg): Given \( x \in \{0,1\}^* \), the intruder can find \( \pi_2(x) \) such that \( H(x) = H(\pi_2(x)) \).
- First Preimage (1stPreImg): Given \( t = H(x) \), the intruder can find \( \pi_1(x) \) such that \( H(\pi_1(x)) = t \).
- Chosen Prefix Collision (CPC): Given two prefixes \( P, P' \in \{0,1\}^* \), the intruder can find suffixes \( cp1(P,P') \) and \( cp2(P,P') \) such that \( H(P \parallel cp1(P,P')) = H(P' \parallel cp2(P,P')) \).
- Collision Extension (ColExt): If \( H(x) = H(y) \), then for any suffix \( s \in \{0,1\}^* \), we have \( H(x \parallel s) = H(y \parallel s) \).
- Input Leak (InLeak): Given \( H(x) \), the intruder can guess or reconstruct the original \( x \).
These vulnerabilities were modeled using an equational theory with order-sorted restrictions for operators such as \( H \), \( \pi_1 \), \( \pi_2 \), \( cp1 \), and \( cp2 \), while preserving associativity of the concatenation operator \( \parallel \). CPC and ColExt vulnerabilities were also modeled for the SIGMA protocol with the following intruder strand instead of equations, which alligns with the event-based approach propossed in [4]:
:: nil :: [ nil
| -(sign(sk(A), H(X1 ; X2 ; X3 ; cp1(X1 ; X2 ; X3, Y1) ; S1 ; S2))),
+(sign(sk(A), H(Y1 ; cp2(X1 ; X2 ; X3, Y1) ; S1 ; S2))),
nil ]
Using this modeling, we were able to automatically discover the known attacks on SIGMA previously found using Tamarin [4], as well as a new attack on the Meadows protocol using the combination of 1stPreImg and 2ndPreImg+InLeak.
A summary of our analysis is shown below, including execution time, number of states, and search depth:
| Protocol | Hash Vulnerability | Approach | Algebraic Theory | Depth | States | Time |
|---|---|---|---|---|---|---|
| SIGMA | CPC & ColExt | Eq. Theory | conc (assoc) exp (assoc, comm) cp1, cp2 |
11 | 6180 | 16.32 days |
| Event-Based | conc (assoc) exp (assoc, comm) |
13 | 618 | 1.14 hours | ||
| CPC | Eq. Theory | conc (assoc) exp (assoc, comm) cp1, cp2 |
11 | 258 | 18 min | |
| Meadows | 1stPreImg | Eq. Theory | conc (assoc*) XOR (assoc*, comm) pi1 |
8 | 313 | 20.88 min |
| 2ndPreImg & InLeak | Eq. Theory | conc (assoc*) XOR (assoc*, comm) pi2, inLeak |
8 | 698 | 2.37 hours |
* Associativity was not needed to find the attacks considering these vulnerabilities.
To download the complete Maude-NPA specification and outputs, click HERE.
References
- Hernández-Sánchez, A., & Escobar, S. (2025). A Symbolic Analysis of Hash Functions Vulnerabilities in Maude-NPA. European Symposium on Research in Computer Security (ESORICS).
- Bhargavan, K., & Leurent, G. (2016). Transcript collision attacks: Breaking authentication in TLS, IKE, and SSH. NDSS Symposium.
- Meadows, C., et al. (2007). Distance bounding protocols: Authentication logic analysis and collusion attacks. In Secure Localization and Time Synchronization. Springer.
- Cheval, V., et al. (2023). Hash Gone Bad: Automated Discovery of Protocol Attacks That Exploit Hash Function Weaknesses. USENIX Security.