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

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.