# Inverting Cryptographic Hash Functions via Cube-and-Conquer

arXiv: https://arxiv.org/abs/2212.02405 · HTML: https://mlsanity.com/paper/2212.02405/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 12 of its 108 references that are in the map.
- First posted on arXiv 5 Dec 2022.

## Builds on (most cited first, 12 of 12)

- [Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer](https://mlsanity.com/paper/1605.00723/) (2016)
- [The Resolution of Keller's Conjecture](https://mlsanity.com/paper/1910.03740/) (2019)
- [On Cryptographic Attacks Using Backdoors for SAT](https://mlsanity.com/paper/1803.04646/) (2018)
- [Using Automatic Generation of Relaxation Constraints to Improve the Preimage Attack on 39-step MD4](https://mlsanity.com/paper/1802.06940/) (2018)
- [Translation of Algorithmic Descriptions of Discrete Functions to SAT with Applications to Cryptanalysis Problems](https://mlsanity.com/paper/1805.07239/) (2018)
- [A SAT-based Resolution of Lam's Problem](https://mlsanity.com/paper/2012.04715/) (2020)
- [Using Monte Carlo method for searching partitionings of hard variants of Boolean satisfiability problem](https://mlsanity.com/paper/1507.00862/) (2015)
- [Encoding Cryptographic Functions to SAT Using Transalg System](https://mlsanity.com/paper/1607.00888/) (2016)
- [Adaptive Restart and CEGAR-based Solver for Inverting Cryptographic Hash Functions](https://mlsanity.com/paper/1608.04720/) (2016)
- [CDCL(Crypto) SAT Solvers for Cryptanalysis](https://mlsanity.com/paper/2005.13415/) (2020)
- [Computer-Aided Proof of Erdos Discrepancy Properties](https://mlsanity.com/paper/1405.3097/) (2014)
- [Constructing Minimal Perfect Hash Functions Using SAT Technology](https://mlsanity.com/paper/1911.10099/) (2019)

## Built on by (most cited first, 1 of 1)

- [Efficient Parallel Algorithm for Decomposing Hard CircuitSAT Instances](https://mlsanity.com/paper/2602.17130/) (2026)

## Abstract (arXiv)

MD4 and MD5 are fundamental cryptographic hash functions proposed in the 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 by 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 extra 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 inverse 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 the minimum runtime estimate 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 is therefore 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. Also, 28-step MD5 is inverted for four hashes via the incomplete SAT solving mode of the second algorithm. For three hashes out of them, it is done for the first time.