Inverting 29-step MD5 compression function via SAT
Prikladnaya Diskretnaya Matematika. Supplement, no. 16 (2023), pp. 36-40.

Voir la notice de l'article provenant de la source Math-Net.Ru

The cryptographic hash function MD5 was proposed in 1992. Its key component is a 64-step compression function. The compression function is still preimage resistant, that is why its step-reduced versions are usually investigated in this context. In 2007, the 26-step version of the MD5 compression function was inverted via SAT. In 2012, 27- and 28-step versions were inverted via SAT as well. In the paper, an approach to forming 32 intermediate inversion problems between two subsequent steps of the MD5 compression function is proposed. SAT encodings of such problems were constructed between 28 and 29 steps. Several simplest problems were leveraged for tuning a modern SAT solver. As a result, the 29-step version of the MD5 compression function was inverted for the first time.
Keywords: cryptographic hash function, logical cryptanalysis, SAT.
Mots-clés : MD5, algebraic cryptanalysis
@article{PDMA_2023_16_a9,
     author = {O. S. Zaikin},
     title = {Inverting 29-step {MD5} compression function via {SAT}},
     journal = {Prikladnaya Diskretnaya Matematika. Supplement},
     pages = {36--40},
     publisher = {mathdoc},
     number = {16},
     year = {2023},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/PDMA_2023_16_a9/}
}
TY  - JOUR
AU  - O. S. Zaikin
TI  - Inverting 29-step MD5 compression function via SAT
JO  - Prikladnaya Diskretnaya Matematika. Supplement
PY  - 2023
SP  - 36
EP  - 40
IS  - 16
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/PDMA_2023_16_a9/
LA  - ru
ID  - PDMA_2023_16_a9
ER  - 
%0 Journal Article
%A O. S. Zaikin
%T Inverting 29-step MD5 compression function via SAT
%J Prikladnaya Diskretnaya Matematika. Supplement
%D 2023
%P 36-40
%N 16
%I mathdoc
%U http://geodesic.mathdoc.fr/item/PDMA_2023_16_a9/
%G ru
%F PDMA_2023_16_a9
O. S. Zaikin. Inverting 29-step MD5 compression function via SAT. Prikladnaya Diskretnaya Matematika. Supplement, no. 16 (2023), pp. 36-40. http://geodesic.mathdoc.fr/item/PDMA_2023_16_a9/

[1] Alferov A. P., Zubov A. Yu., Kuzmin A. S., Cheremushkin A. V., Osnovy kriptografii, 2-e izd., Gelios ARV, M., 2002

[2] Rivest R., The MD5 message-digest algorithm, RFC 1321, , 1992 https://www.ietf.org/rfc/rfc1321.txt

[3] Wang X. and Yu H., “How to break MD5 and other hash functions”, LNCS, 3494, 2005, 19–35 | MR | Zbl

[4] Massacci F. and Marraro L., “Logical cryptanalysis as a SAT problem”, J. Automated Reasoning, 1 (2000), 165–203 | DOI | MR | Zbl

[5] Bard G., Algebraic Cryptanalysis, Springer, N.Y., 2009 | MR | Zbl

[6] De D., Kumarasubramanian A., and Venkatesan R, “Inversion attacks on secure hash functions using SAT solvers”, LNCS, 4501, 2007, 377–382 | Zbl

[7] Marques-Silva J. P. and Sakallah K. A., “GRASP: a search algorithm for propositional satisfiability”, IEEE Trans. Computers, 48:5 (1999), 506–521 | DOI | MR | Zbl

[8] Legendre F., Dequen G., and Krajecki M., “Encoding hash functions as a SAT problem”, Proc. ICTAI (Athens, Greece, 2012), 916–921

[9] Zaikin O., “Inverting 43-step MD4 via cube-and-conquer”, Proc. IJCAI-ECAI 2022, 1894–1900

[10] Heule M. J. H., Kullmann O., Wieringa S., and Biere A., “Cube and Conquer: guiding CDCL SAT solvers by lookaheads”, LNCS, 7261, 2012, 50–65

[11] Dobbertin H., “The first two rounds of MD4 are not one-way”, LNCS, 1372, 1998, 284–292 | Zbl

[12] Gribanova I. A., “Novyi algoritm porozhdeniya oslablyayuschikh ogranichenii v zadache obrascheniya khesh-funktsii MD4-39”, Prikladnaya diskretnaya matematika. Prilozhenie, 2018, no. 11, 139–141

[13] Semenov A. A., Otpuschennikov I. V., Gribanova I. A., et al., “Translation of algorithmic descriptions of discrete functions to SAT with application to cryptanalysis problems”, Logical Methods in Computer Science, 16:1 (2020), 29:1–29:42 pp. | MR

[14] Clarke E., Kroening D., and Lerda F., “A tool for checking ANSI-C programs”, LNCS, 2988, 2004, 168–176 | Zbl

[15] Biere A. and Fleury M., “Gimsatul, IsaSAT and Kissat entering the SAT Competition 2022”, Proc. SAT Competition 2022 Solver and Benchmark Descriptions, 10–11

[16] Irkutskii superkompyuternyi tsentr SO RAN, http://hpc.icc.ru