Geodesic
Application of algorithms solving SAT problem to cryptanalysis of hash functions of MD family
Prikladnaya Diskretnaya Matematika. Supplement, no. 8 (2015), pp. 139-142

Voir la notice de l'article provenant de la source Math-Net.Ru

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.
Keywords: cryptographic hash functions, collisions of hash functions, Boolean satisfiability problem, SAT.
Mots-clés : MD4, MD5 
@article{PDMA_2015_8_a53,
     author = {I. A. Bogachkova and O. S. Zaikin and S. E. Kochemazov and I. V. Otpuschennikov and A. A. Semenov},
     title = {Application of algorithms solving {SAT} problem to cryptanalysis of hash functions of {MD} family},
     journal = {Prikladnaya Diskretnaya Matematika. Supplement},
     pages = {139--142},
     publisher = {mathdoc},
     number = {8},
     year = {2015},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/PDMA_2015_8_a53/}
}
TY  - JOUR
AU  - I. A. Bogachkova
AU  - O. S. Zaikin
AU  - S. E. Kochemazov
AU  - I. V. Otpuschennikov
AU  - A. A. Semenov
TI  - Application of algorithms solving SAT problem to cryptanalysis of hash functions of MD family
JO  - Prikladnaya Diskretnaya Matematika. Supplement
PY  - 2015
SP  - 139
EP  - 142
IS  - 8
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/PDMA_2015_8_a53/
LA  - ru
ID  - PDMA_2015_8_a53
ER  - 
%0 Journal Article
%A I. A. Bogachkova
%A O. S. Zaikin
%A S. E. Kochemazov
%A I. V. Otpuschennikov
%A A. A. Semenov
%T Application of algorithms solving SAT problem to cryptanalysis of hash functions of MD family
%J Prikladnaya Diskretnaya Matematika. Supplement
%D 2015
%P 139-142
%N 8
%I mathdoc
%U http://geodesic.mathdoc.fr/item/PDMA_2015_8_a53/
%G ru
%F PDMA_2015_8_a53
I. A. Bogachkova; O. S. Zaikin; S. E. Kochemazov; I. V. Otpuschennikov; A. A. Semenov. Application of algorithms solving SAT problem to cryptanalysis of hash functions of MD family. Prikladnaya Diskretnaya Matematika. Supplement, no. 8 (2015), pp. 139-142. http://geodesic.mathdoc.fr/item/PDMA_2015_8_a53/