  MD4 and MD5 are seminal cryptographic hash functions proposed in early 1990s.
MD4 consists of 48 steps and produces a 128-bit hash given a message of
arbitrary finite size. MD5 is a more secure 64-step extension of MD4. Both MD4
and MD5 are vulnerable to practical collision attacks, yet it is still not
realistic to invert them, i.e. to find a message given a hash. In 2007, the
39-step version of MD4 was inverted via reducing to SAT and applying a CDCL
solver along with the so-called Dobbertin's constraints. As for MD5, in 2012
its 28-step version was inverted via a CDCL solver for one specified hash
without adding any additional constraints. In this study, Cube-and-Conquer (a
combination of CDCL and lookahead) is applied to invert step-reduced versions
of MD4 and MD5. For this purpose, two algorithms are proposed. The first one
generates inversion problems for MD4 by gradually modifying the Dobbertin's
constraints. The second algorithm tries the cubing phase of Cube-and-Conquer
with different cutoff thresholds to find the one with minimal runtime
estimation of the conquer phase. This algorithm operates in two modes: (i)
estimating the hardness of a given propositional Boolean formula; (ii)
incomplete SAT-solving of a given satisfiable propositional Boolean formula.
While the first algorithm is focused on inverting step-reduced MD4, the second
one is not area-specific and so is applicable to a variety of classes of hard
SAT instances. In this study, 40-, 41-, 42-, and 43-step MD4 are inverted for
the first time via the first algorithm and the estimating mode of the second
algorithm. 28-step MD5 is inverted for four hashes via the incomplete
SAT-solving mode of the second algorithm. For three hashes out of them this is
done for the first time.
