Application of solving SAT algorithms to constructing differential paths for finding collisions of cryptographic hash functions in the MD family

I. A. Gribanova

Prikladnaya Diskretnaya Matematika. Supplement, no. 9 (2016), pp. 129-132.

Résumé

In this paper, we present a new method for constructing differential paths to find collisions of cryptographic hash functions in the MD family. The method is based on using the algorithms for solving Boolean satisfiability problem (SAT). The proposed method can be applied to hash functions based on the Merkle–Damgard construction, which, on its internal stages, use inner variables of relatively small size. We consider two copies of the algorithm for computing hash function value, that process some messages $M$ and $M'$, respectively. On the initial stage of the method, we construct two “template” CNFs $C$ and $C'$, which encode the process of computing hash-images for $M$ and $M'$. The sets of Boolean variables used in these two CNFs are disjoint. We combine CNFs $C$ and $C'$ via conjunction and add to the result the constraint specifying that hash values for $M$ and $M'$ are equal. Thus, we obtain the CNF $\tilde C$ that encodes the problem of finding collisions for the considered hash function. Then we add to $\tilde C$ additional constraints (in the form of clauses), that encode the corresponding differential path. In the context of the proposed method, we then explore the satisfiability of CNF of the form $\tilde C\wedge C_\Delta\wedge C_{\delta_k=c}$, where by $C_\Delta$ we denote the CNF, that takes the value $1$ iff the difference between integer values specified by $512$-bit vectors $M$ and $M'$ is equal to some constant $\Delta$. By $C_{\delta_k=c}$ we denote the CNF, that takes value $1$ iff a variable $\delta_k$ takes the value $c$. Here, $\delta_k$ is a $32$-bit variable, that encodes the difference of integer values of hash registers at the step number $k$. The algorithms in the MD family use $32$-bit inner variables. In this case, $c$ is a $32$-bit constant. Therefore, it is possible to check all of its possible values and consider SAT for CNFs of the kind $\tilde C\wedge C_\Delta\wedge C_{\delta_k=c}$. The SAT instances of this kind, for which we cannot obtain the answer in relatively small time (several seconds), are interrupted. Let $c'$ be the value of $\delta_k$, for which the solving of such SAT instance is interrupted, and assume that $c'$ is not equal to the corresponding value in the known differential path. Then we can consider $c'$ as a possible candidate for the value of $\delta_k$ in the new differential path. The described algorithm is implemented in the form of parallel MPI program and tested on the computing cluster. As a result we managed to construct new differential path for finding collisions of MD4 hash function. This path differs from the path proposed by X. Wang in differential constraints for steps number $k\in\{13,17,20,21\}$. We incorporated it into the propositional encoding of MD4, constructed the corresponding CNF, and applied to it the SAT solver {\texttt cryptominisat}, that has an option of enumerating multiple solutions. For the constructed CNF, the solver managed to find 1000 solutions in 416 seconds. In the application to the similar CNF produced for the Wang differential path, {\texttt cryptominisat} finds 1000 solutions in 520 seconds.

Détail

Keywords: cryptographic hash function, collision, Boolean satisfiability problem, SAT, MD family hash functions.

Bibliographie

[1] Merkle R. A., “Certified digital signature”, LNCS, 435, 1990, 218–238 | MR

[2] Damgard I. A., “A design principle for hash functions”, LNCS, 435, 1990, 416–427 | MR | Zbl

[3] Wang X., Lai X., Feng D., et al., “Cryptanalysis of the hash functions MD4 and RIPEMD”, LNCS, 3494, 2005, 1–18 | MR | Zbl

[4] Wang X., Yu H., “How to break MD5 and other hash functions”, LNCS, 3494, 2005, 19–35 | MR | Zbl

[5] Mironov I., Zhang L., “Applications of SAT solvers to cryptanalysis of hash functions”, LNCS, 4121, 2006, 102–115 | MR | Zbl

[6] Bogachkova I. A., Zaikin O. S., Kochemazov S. E. i dr., “Zadachi poiska kollizii dlya kriptograficheskikh khesh-funktsii semeistva MD kak varianty zadachi o bulevoi vypolnimosti”, Vychislitelnye metody i programmirovanie, 16:1 (2015), 61–77

[7] Otpuschennikov I. V., Semënov A. A., “Tekhnologiya translyatsii kombinatornykh problem v bulevy uravneniya”, Prikladnaya diskretnaya matematika, 2011, no. 1, 96–115

[8] Otpuschennikov I., Semenov A., Kochemazov S., “Transalg: a tool for translating procedural descriptions of discrete functions to SAT”, WCSE 2015-IPCE, Proc. 5th Intern. Workshop on Computer Science and Engineering: Information Processing and Control Engineering, 2015, 289–294

[9] Hawkes P., Paddon M., Rose G., Musings on the Wang et al. MD5 Collision, Cryptology ePrint Archive, Report 2004/264, , 2004 http://eprint.iacr.org/2004/264

[10] Hirshman G., Further Musings on the Wang et al. MD5 Collision: Improvements and Corrections on the Work of Hawkes, Paddon, and Rose, Cryptology ePrint Archive, Report 2007/375, , 2007 http://eprint.iacr.org/2007/375

[11] Stevens M., Attacks on Hash Functions and Applications, PhD Thesis, Ipskamp Drukkers, Amsterdam, 2012, 258 pp.