Document Open Access Logo

Inverting Step-Reduced SHA-1 and MD5 by Parameterized SAT Solvers

Author Oleg Zaikin

PDF
Thumbnail PDF

File

LIPIcs.CP.2024.31.pdf
  • Filesize: 0.77 MB
  • 19 pages

Document Identifiers

Author Details

Oleg Zaikin
  • ISDCT SB RAS, Irkutsk, Russia

Funding

This study was funded by the Ministry of Education of the Russian Federation, project No. 121041300065-9.

Cite AsGet BibTex

Oleg Zaikin. Inverting Step-Reduced SHA-1 and MD5 by Parameterized SAT Solvers. In 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 307, pp. 31:1-31:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.CP.2024.31

Abstract

MD5 and SHA-1 are fundamental cryptographic hash functions proposed in 1990s. Given a message of arbitrary finite size, MD5 produces a 128-bit hash in 64 steps, while SHA-1 produces a 160-bit hash in 80 steps. It is computationally infeasible to invert MD5 and SHA-1, i.e. to find a message given a hash. In 2012, 28-step MD5 and 23-step SHA-1 were inverted by CDCL solvers, yet no progress has been made since then. The present paper proposes to construct 31 intermediate inverse problems for any pair of MD5 or SHA-1 steps (i,i+1), such that the first problem is very close to inverting i steps, while the 31st one is almost inverting i+1 steps. We constructed SAT encodings of intermediate problems for MD5 and SHA-1, and tuned a CDCL solver on the simplest of them. Then the tuned solver was used to design a parallel Cube-and-Conquer solver which for the first time inverted 29-step MD5 and 24-step SHA-1.

Subject Classification

ACM Subject Classification
  • Theory of computation → Constraint and logic programming
Keywords
  • cryptographic hash function
  • MD5
  • SHA-1
  • preimage attack
  • SAT
  • Cube-and-Conquer

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Carlos Ansótegui, Josep Pon, Meinolf Sellmann, and Kevin Tierney. Pydgga: Distributed GGA for automatic configuration. In Chu-Min Li and Felip Manyà, editors, Theory and Applications of Satisfiability Testing - SAT 2021 - 24th International Conference, Barcelona, Spain, July 5-9, 2021, Proceedings, volume 12831 of Lecture Notes in Computer Science, pages 11-20. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-80223-3_2.
  2. Carlos Ansótegui, Meinolf Sellmann, and Kevin Tierney. A gender-based genetic algorithm for the automatic configuration of algorithms. In Ian P. Gent, editor, Principles and Practice of Constraint Programming - CP 2009, 15th International Conference, CP 2009, Lisbon, Portugal, September 20-24, 2009, Proceedings, volume 5732 of Lecture Notes in Computer Science, pages 142-157. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-04244-7_14.
  3. João Araújo, Choiwah Chow, and Mikolás Janota. Symmetries for cube-and-conquer in finite model finding. In Roland H. C. Yap, editor, 29th International Conference on Principles and Practice of Constraint Programming, CP 2023, August 27-31, 2023, Toronto, Canada, volume 280 of LIPIcs, pages 8:1-8:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.CP.2023.8.
  4. Emanuele Bellini, Alessandro De Piccoli, Rusydi H. Makarim, Sergio Polese, Lorenzo Riva, and Andrea Visconti. New records of pre-image search of reduced SHA-1 using SAT solvers. In Debasis Giri, Kim-Kwang Raymond Choo, Saminathan Ponnusamy, Weizhi Meng, Sedat Akleylek, and Santi Prasad Maity, editors, Proceedings of the Seventh International Conference on Mathematics and Computing - ICMC 2021, Shibpur, India, volume 1412 of Advances in Intelligent Systems and Computing, pages 141-151. Springer, 2021. URL: https://doi.org/10.1007/978-981-16-6890-6_11.
  5. Armin Biere and Mathias Fleury. Gimsatul, IsaSAT and Kissat entering the SAT Competition 2022. In Tomas Balyo, Marijn Heule, Markus Iser, Matti Järvisalo, and Martin Suda, editors, SAT Competition 2022 - Solver and Benchmark Descriptions, volume B-2022-1 of Department of Computer Science Series of Publications B, pages 10-11. University of Helsinki, 2022. Google Scholar
  6. Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA336.
  7. Curtis Bright, Kevin K. H. Cheung, Brett Stevens, Ilias S. Kotsireas, and Vijay Ganesh. A sat-based resolution of lam’s problem. In Thirty-Fifth AAAI Conference on Artificial Intelligence, AAAI 2021, Virtual Event, February 2-9, 2021, pages 3669-3676. AAAI Press, 2021. URL: https://doi.org/10.1609/AAAI.V35I5.16483.
  8. Davin Choo, Mate Soos, Kian Ming Adam Chai, and Kuldeep S. Meel. Bosphorus: Bridging ANF and CNF solvers. In Jürgen Teich and Franco Fummi, editors, Design, Automation & Test in Europe Conference & Exhibition, DATE 2019, Florence, Italy, March 25-29, 2019, pages 468-473. IEEE, 2019. URL: https://doi.org/10.23919/DATE.2019.8715061.
  9. Ivan Damgård. A design principle for hash functions. In Gilles Brassard, editor, Advances in Cryptology - CRYPTO '89, 9th Annual International Cryptology Conference, Santa Barbara, California, USA, August 20-24, 1989, Proceedings, volume 435 of Lecture Notes in Computer Science, pages 416-427. Springer, 1989. URL: https://doi.org/10.1007/0-387-34805-0_39.
  10. Debapratim De, Abishek Kumarasubramanian, and Ramarathnam Venkatesan. Inversion attacks on secure hash functions using satsolvers. In João Marques-Silva and Karem A. Sakallah, editors, Theory and Applications of Satisfiability Testing - SAT 2007, 10th International Conference, Lisbon, Portugal, May 28-31, 2007, Proceedings, volume 4501 of Lecture Notes in Computer Science, pages 377-382. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-72788-0_36.
  11. Donald E. Eastlake and Paul E. Jones. US secure hash algorithm 1 (SHA1). RFC, 3174:1-22, 2001. URL: https://doi.org/10.17487/RFC3174.
  12. Thomas Espitau, Pierre-Alain Fouque, and Pierre Karpman. Higher-order differential meet-in-the-middle preimage attacks on SHA-1 and BLAKE. In Rosario Gennaro and Matthew Robshaw, editors, Advances in Cryptology - CRYPTO 2015 - 35th Annual Cryptology Conference, Santa Barbara, CA, USA, August 16-20, 2015, Proceedings, Part I, volume 9215 of Lecture Notes in Computer Science, pages 683-701. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-47989-6_33.
  13. Marijn Heule, Oliver Kullmann, Siert Wieringa, and Armin Biere. Cube and conquer: Guiding CDCL SAT solvers by lookaheads. In Kerstin Eder, João Lourenço, and Onn Shehory, editors, Hardware and Software: Verification and Testing - 7th International Haifa Verification Conference, HVC 2011, Haifa, Israel, December 6-8, 2011, Revised Selected Papers, volume 7261 of Lecture Notes in Computer Science, pages 50-65. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-34188-5_8.
  14. Marijn Heule and Hans van Maaren. March_dl: Adding adaptive heuristics and a new branching strategy. J. Satisf. Boolean Model. Comput., 2(1-4):47-59, 2006. URL: https://doi.org/10.3233/SAT190016.
  15. Marijn J. H. Heule. Schur number five. In Sheila A. McIlraith and Kilian Q. Weinberger, editors, Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, (AAAI-18), New Orleans, Louisiana, USA, February 2-7, 2018, pages 6598-6606. AAAI Press, 2018. URL: https://doi.org/10.1609/AAAI.V32I1.12209.
  16. Marijn J. H. Heule, Oliver Kullmann, and Victor W. Marek. Solving and verifying the Boolean Pythagorean triples problem via Cube-and-Conquer. In Nadia Creignou and Daniel Le Berre, editors, Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings, volume 9710 of Lecture Notes in Computer Science, pages 228-245. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-40970-2_15.
  17. Ekawat Homsirikamol, Pawel Morawiecki, Marcin Rogawski, and Marian Srebrny. Security margin evaluation of SHA-3 contest finalists through sat-based attacks. In Agostino Cortesi, Nabendu Chaki, Khalid Saeed, and Slawomir T. Wierzchon, editors, Computer Information Systems and Industrial Management - 11th IFIP TC 8 International Conference, CISIM 2012, Venice, Italy, September 26-28, 2012. Proceedings, volume 7564 of Lecture Notes in Computer Science, pages 56-67. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-33260-9_4.
  18. Holger H. Hoos, Frank Hutter, and Kevin Leyton-Brown. Automated configuration and selection of SAT solvers. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 481-507. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA200995.
  19. Frank Hutter, Holger H. Hoos, and Kevin Leyton-Brown. Sequential model-based optimization for general algorithm configuration. In Carlos A. Coello Coello, editor, Learning and Intelligent Optimization - 5th International Conference, LION 5, Rome, Italy, January 17-21, 2011. Selected Papers, volume 6683 of Lecture Notes in Computer Science, pages 507-523. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-25566-3_40.
  20. Frank Hutter, Holger H. Hoos, and Thomas Stützle. Automatic algorithm configuration based on local search. In Proceedings of the Twenty-Second AAAI Conference on Artificial Intelligence, July 22-26, 2007, Vancouver, British Columbia, Canada, pages 1152-1157. AAAI Press, 2007. URL: http://www.aaai.org/Library/AAAI/2007/aaai07-183.php.
  21. Stepan Kochemazov. Exploring the limits of problem-specific adaptations of SAT solvers in SAT-based cryptanalysis. In Leonid Sokolinsky and Mikhail Zymbler, editors, Parallel Computational Technologies, pages 149-163. Springer International Publishing, 2021. URL: https://doi.org/10.1007/978-3-030-81691-9_11.
  22. Florian Legendre, Gilles Dequen, and Michaël Krajecki. Encoding hash functions as a SAT problem. In IEEE 24th International Conference on Tools with Artificial Intelligence, ICTAI 2012, Athens, Greece, November 7-9, 2012, pages 916-921. IEEE Computer Society, 2012. URL: https://doi.org/10.1109/ICTAI.2012.128.
  23. Marius Lindauer, Katharina Eggensperger, Matthias Feurer, André Biedenkapp, Difan Deng, Carolin Benjamins, Tim Ruhkopf, René Sass, and Frank Hutter. SMAC3: A versatile bayesian optimization package for hyperparameter optimization. J. Mach. Learn. Res., 23:54:1-54:9, 2022. URL: http://jmlr.org/papers/v23/21-0888.html.
  24. João Marques-Silva and Karem Sakallah. GRASP: A search algorithm for propositional satisfiability. IEEE Trans. Computers, 48(5):506-521, 1999. URL: https://doi.org/10.1109/12.769433.
  25. Alfred Menezes, Paul C. van Oorschot, and Scott A. Vanstone. Handbook of Applied Cryptography. CRC Press, 1996. URL: https://doi.org/10.1201/9781439821916.
  26. Ralph C. Merkle. A certified digital signature. In Gilles Brassard, editor, Advances in Cryptology - CRYPTO '89, 9th Annual International Cryptology Conference, Santa Barbara, California, USA, August 20-24, 1989, Proceedings, volume 435 of Lecture Notes in Computer Science, pages 218-238. Springer, 1989. URL: https://doi.org/10.1007/0-387-34805-0_21.
  27. Ilya Mironov and Lintao Zhang. Applications of SAT solvers to cryptanalysis of hash functions. In Armin Biere and Carla P. Gomes, editors, Theory and Applications of Satisfiability Testing - SAT 2006, 9th International Conference, Seattle, WA, USA, August 12-15, 2006, Proceedings, volume 4121 of Lecture Notes in Computer Science, pages 102-115. Springer, 2006. URL: https://doi.org/10.1007/11814948_13.
  28. Pawel Morawiecki and Marian Srebrny. A SAT-based preimage analysis of reduced Keccak hash functions. Inf. Process. Lett., 113(10-11):392-397, 2013. URL: https://doi.org/10.1016/J.IPL.2013.03.004.
  29. Rajeev Motwani and Prabhakar Raghavan. Randomized Algorithms. Cambridge University Press, 1995. URL: https://doi.org/10.1017/CBO9780511814075.
  30. Heinz Mühlenbein. How genetic algorithms really work: Mutation and hillclimbing. In Reinhard Männer and Bernard Manderick, editors, Parallel Problem Solving from Nature 2, PPSN-II, Brussels, Belgium, September 28-30, 1992, pages 15-26. Elsevier, 1992. Google Scholar
  31. Kevin P. Murphy. Machine learning - a probabilistic perspective. Adaptive computation and machine learning series. MIT Press, 2012. Google Scholar
  32. Saeed Nejati and Vijay Ganesh. CDCL(Crypto) SAT solvers for cryptanalysis. In Tima Pakfetrat, Guy-Vincent Jourdan, Kostas Kontogiannis, and Robert F. Enenkel, editors, Proceedings of the 29th Annual International Conference on Computer Science and Software Engineering, CASCON 2019, Markham, Ontario, Canada, November 4-6, 2019, pages 311-316. ACM, 2019. URL: https://doi.org/10.5555/3370272.3370307.
  33. Saeed Nejati, Jan Horácek, Catherine H. Gebotys, and Vijay Ganesh. Algebraic fault attack on SHA hash functions using programmatic SAT solvers. In John N. Hooker, editor, Principles and Practice of Constraint Programming - 24th International Conference, CP 2018, Lille, France, August 27-31, 2018, Proceedings, volume 11008 of Lecture Notes in Computer Science, pages 737-754. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-98334-9_47.
  34. Saeed Nejati, Jia Hui Liang, Catherine H. Gebotys, Krzysztof Czarnecki, and Vijay Ganesh. Adaptive restart and CEGAR-based solver for inverting cryptographic hash functions. In Andrei Paskevich and Thomas Wies, editors, Verified Software. Theories, Tools, and Experiments - 9th International Conference, VSTTE 2017, Heidelberg, Germany, July 22-23, 2017, Revised Selected Papers, volume 10712 of Lecture Notes in Computer Science, pages 120-131. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-72308-2_8.
  35. Vegard Nossum. SAT-based preimage attacks on SHA-1. Master’s thesis, University of Oslo, Department of Informatics, 2012. Google Scholar
  36. Ronald L. Rivest. The MD4 message digest algorithm. In Alfred Menezes and Scott A. Vanstone, editors, Advances in Cryptology - CRYPTO '90, 10th Annual International Cryptology Conference, Santa Barbara, California, USA, August 11-15, 1990, Proceedings, volume 537 of Lecture Notes in Computer Science, pages 303-311. Springer, 1990. URL: https://doi.org/10.1007/3-540-38424-3_22.
  37. Ronald L. Rivest. The MD5 message-digest algorithm. RFC, 1321:1-21, 1992. URL: https://doi.org/10.17487/RFC1321.
  38. Yu Sasaki, Wataru Komatsubara, Yasuhide Sakai, Lei Wang, Mitsugu Iwamoto, Kazuo Sakiyama, and Kazuo Ohta. Meet-in-the-middle preimage attacks revisited - new results on MD5 and HAVAL. In Pierangela Samarati, editor, SECRYPT 2013 - Proceedings of the 10th International Conference on Security and Cryptography, Reykjavík, Iceland, 29-31 July, 2013, pages 111-122. SciTePress, 2013. URL: https://ieeexplore.ieee.org/document/7223160/.
  39. Alexander A. Semenov, Daniil Chivilikhin, Artem Pavlenko, Ilya V. Otpuschennikov, Vladimir Ulyantsev, and Alexey Ignatiev. Evaluating the hardness of SAT instances using evolutionary optimization algorithms. In Laurent D. Michel, editor, 27th International Conference on Principles and Practice of Constraint Programming, CP 2021, Montpellier, France (Virtual Conference), October 25-29, 2021, volume 210 of LIPIcs, pages 47:1-47:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPICS.CP.2021.47.
  40. Alexander A. Semenov, Ilya V. Otpuschennikov, Irina Gribanova, Oleg Zaikin, and Stepan Kochemazov. Translation of algorithmic descriptions of discrete functions to SAT with applications to cryptanalysis problems. Log. Methods Comput. Sci., 16(1), 2020. URL: https://doi.org/10.23638/LMCS-16(1:29)2020.
  41. Mate Soos, Karsten Nohl, and Claude Castelluccia. Extending SAT solvers to cryptographic problems. In Oliver Kullmann, editor, Theory and Applications of Satisfiability Testing - SAT 2009, 12th International Conference, SAT 2009, Swansea, UK, June 30 - July 3, 2009. Proceedings, volume 5584 of Lecture Notes in Computer Science, pages 244-257. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02777-2_24.
  42. Marian Srebrny, Mateusz Srebrny, and Lidia Stepien. SAT as a programming environment for linear algebra and cryptanalysis. In International Symposium on Artificial Intelligence and Mathematics, ISAIM 2008, Fort Lauderdale, Florida, USA, January 2-4, 2008, 2008. URL: http://isaim2008.unl.edu/PAPERS/SS1-AI+Logic/MSrebrny-ss1.pdf.
  43. Marc Stevens, Elie Bursztein, Pierre Karpman, Ange Albertini, and Yarik Markov. The first collision for full SHA-1. In Jonathan Katz and Hovav Shacham, editors, Advances in Cryptology - CRYPTO 2017 - 37th Annual International Cryptology Conference, Santa Barbara, CA, USA, August 20-24, 2017, Proceedings, Part I, volume 10401 of Lecture Notes in Computer Science, pages 570-596. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-63688-7_19.
  44. Xiaoyun Wang and Hongbo Yu. How to break MD5 and other hash functions. In Ronald Cramer, editor, Advances in Cryptology - EUROCRYPT 2005, 24th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Aarhus, Denmark, May 22-26, 2005, Proceedings, volume 3494 of Lecture Notes in Computer Science, pages 19-35. Springer, 2005. URL: https://doi.org/10.1007/11426639_2.
  45. Oleg Zaikin. Inverting 43-step MD4 via Cube-and-Conquer. In Luc De Raedt, editor, Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, IJCAI 2022, Vienna, Austria, 23-29 July 2022, pages 1894-1900. ijcai.org, 2022. URL: https://doi.org/10.24963/IJCAI.2022/263.
  46. Oleg Zaikin. Inverting cryptographic hash functions via Cube-and-Conquer. J. Artif. Intell. Res., in press. Google Scholar
  47. Oleg Zaikin and Stepan Kochemazov. On black-box optimization in divide-and-conquer SAT solving. Optim. Methods Softw., 36(4):672-696, 2021. URL: https://doi.org/10.1080/10556788.2019.1685993.
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact