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

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.