Towards Better SAT Encodings for Hash Function Inversion Problems

Inversion of reduced-round hash functions is one of the areas of cryptography, in which Boolean satisfiability (SAT) solvers show good performance. Recent results on the inversion of 43 -step MD4 using SAT make it possible to believe that more progress can be achieved by careful solver engineering and SAT encodings manipulation. In the present paper we consider possible ways to improve the SAT encodings for inversion of hash functions from the MD and SHA families, in particular, MD4, and SHA-1. We study the available encodings, including the ones proposed by Vegard Nossum, and made by automatic encoding tools. We then show that it is possible to make the encodings better by constructing the integer sums in a different way or eliminating some of the auxiliary variables via Boolean minimization. In the computational experiments we consider a variety of benchmarks, which encode reduced-round variants of the considered hash functions.