Application of algorithms solving SAT problem to cryptanalysis of hash functions of MD family

I. A. Bogachkova ; O. S. Zaikin ; S. E. Kochemazov ; I. V. Otpuschennikov ; A. A. Semenov

Prikladnaya Diskretnaya Matematika. Supplement, no. 8 (2015), pp. 139-142.

Résumé

In this research, we consider the problems of searching for collisions in cryptographic hash functions from the MD family as variants of the Boolean Satisfiability problem (SAT). To construct the SAT encodings for MD4 and MD5 algorithms, we employ the Transalg system designed to automatically transform algorithmic descriptions of discrete functions to Boolean equations. For hash functions under consideration, the SAT encodings are much more compact than known analogues, because the several additional constraints based on the known differential attacks on these functions are used in these encodings. The solving time for the SAT instances, encoding the search for single block collisions for MD4, is on average less than 1 sec on an usual PC. To solve the SAT instances, encoding the search for two-block collisions for MD5, we employed parallel SAT solvers working on the computing cluster. As a result, we found a class of two-block collisions for MD5 with the first 10 zero bytes. We constructed several dozens of collisions of the proposed kind. Also, we considered the inversion problem for the MD4 hash function (the search for the preimage for a given hash value). To solve this problem, we developed a technique relying on the so called “switch variables”. Each switch variable is responsible for an additional constraint on several Boolean variables included in the SAT encoding. If a switch variable takes the value of Truth then the corresponding constraint becomes enabled and should be taken into account by the SAT solving algorithm. Otherwise this constraint remains inactive. The use of switch variables made it possible to find new additional constraints (similar to “Dobbertin's constraints”) and to improve the effectiveness of solving the inversion problem for $39$-step MD4 by a hundredfold.

Détail

Keywords: cryptographic hash functions, collisions of hash functions, Boolean satisfiability problem, SAT.
Mots-clés : MD4, MD5

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] Rivest R. L., “The MD4 Message Digest Algorithm”, LNCS, 537, 1991, 303–311 | Zbl

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

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

[6] Biham E., Shamir A., “Differential cryptanalysis of DES-like cryptosystems”, J. Cryptology, 4:1 (1991), 3–72 | DOI | MR | Zbl

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

[8] Biere A., Heule V., van Maaren H, Walsh T., Handbook of Satisfiability, IOS Press, Amsterdam, 2009 | Zbl

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

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

[11] De D., Kumarasubramanian A., Venkatesan R., “Inversion attacks on secure hash functions using SAT solvers”, LNCS, 4501, 2007, 377–382 | Zbl

[12] Dobbertin H., “The first two rounds of MD4 are not One-Way”, Proc. 5th Intern. Workshop Fast Software Encryption, Springer Verlag, London, UK, 1998, 284–292 | DOI

[13] Nadel A., Ryvchin V., “Efficient SAT solving under assumptions”, LNCS, 7317, 2012, 242–255 | Zbl