Gribanova I.A.   Zaikin O.S.   Kochemazov S.E.   Otpuschennikov I.V.   Semenov A.A.  

The study of inversion problems of cryptographic hash functions from MD family using algorithms for solving Boolean satisfiability problem

Reporter: Zaikin O.S.

In this report we present the result of application of state-of-the-art SAT solvers to problems of inversion of cryptographic hash functions from the MD family. In particular we consider the problems of finding preimages and collisions for MD4 and MD5 hash functions. Hash function is a total computable discrete function of the kind  \chi:{0,1}^*\rightarrow {0,1}^C, where C is some constant called the hash length. If n>C then in {0,1}^* there are such x_1,x_2∈{0,1}^n, x_1 \neq x_2, that \chi(x_1 )=\chi(x_2). In this case messages x_1,x_2 form a collision. Usually, cryptographic hash functions have to satisfy a number of additional conditions, such as that all problems related to function inversion must be computationally hard. In other words, both finding preimage (i.e. inversion) and finding collisions should be hard.

We consider finding preimages and collisions of the widely known MD4 and MD5 hash functions. To solve the problems we apply the approach based on reducing them to Boolean satisfiability problem (SAT), and applying state-of-the-art SAT solvers to corresponding encodings. The SAT encodings of the algorithms specifying the considered functions are constructed using the Transalg system. This system makes it possible to modify the propositional encodings of MD4 and MD5 algorithms by adding to them additional constraints in the form of differential paths by X. Wang for finding collisions, or the constraints by H. Dobbertin for finding preimages. The effectiveness of proposed algorithms is greater than that of similar algorithms from papers of different authors. In addition to that, using the constructed algorithms we managed to find new families of two-block collisions for MD5 and new differential paths for finding single-block collisions for MD4.