LEVERAGING CUBE-AND-CONQUER FOR CRYPTOGRAPHIC HASH FUNCTION PREIMAGE DISCOVERY: A SAT-BASED CRYPTANALYSIS PERSPECTIVE

Dr. Sophia Chen; Dr. Marcus J. Rivera

Open Access icon Open Access

ARTICLE

LEVERAGING CUBE-AND-CONQUER FOR CRYPTOGRAPHIC HASH FUNCTION PREIMAGE DISCOVERY: A SAT-BASED CRYPTANALYSIS PERSPECTIVE

Dr. Sophia Chen ¹ , Dr. Marcus J. Rivera ²

¹ School of Computing, National University of Singapore, Singapore

² Department of Engineering, Imperial College London, United Kingdom

Issue Vol. 1 No. 01 (2024): Volume 01 Issue 01 --- Section Articles --- Published Date: 2024-12-18

Citations: Loading…

ABSTRACT VIEWS: 24 | FILE VIEWS: 5 | PDF: 5 HTML: 0 OTHER: 0 | TOTAL: 29

Views + Downloads (Last 90 days)

Cumulative % included

Abstract

Cryptographic hash functions are cornerstones of digital security, inherently designed to resist preimage attacks—the computational challenge of finding an input that generates a specific output hash. Despite this design principle, certain hash functions, particularly their reduced-round versions or older standards, can exhibit vulnerabilities that allow for practical preimage discovery. This comprehensive article delves into advanced methodologies for conducting preimage attacks on cryptographic hash functions, with a particular emphasis on the sophisticated integration of Satisfiability (SAT) solvers and the "Cube-and-Conquer" (CnC) paradigm. We meticulously explore the intricate process of encoding hash function inversion problems into Boolean formulas, elucidating the advantages conferred by parallel and distributed SAT solving environments. A core focus is placed on how the divide-and-conquer strategy, synergistically enhanced by look-ahead heuristics and strategic backdoor detection, can dramatically augment the efficiency and feasibility of such cryptanalytic endeavors. Empirical results pertaining to the inversion of various step-reduced MD4 and MD5 versions are critically examined, highlighting the practical implications of these findings for assessing the real-world security margins of cryptographic primitives.

Keywords

Cryptographic hash functions, Preimage attacks, Cube-and-Conquer, SAT solvers

References

1. Almagro-Blanco, P., & Gir´aldez-Cru, J. (2022). Characterizing the temperature of SAT formulas. Int. J. Comput. Intell. Syst., 15(1), 69.

2. Ans´otegui, C., Bonet, M. L., Levy, J., & Many`a, F. (2008). Measuring the hardness of SAT instances. In AAAI, pp. 222–228.

3. Aoki, K., & Sasaki, Y. (2008). Preimage attacks on one-block MD4, 63-step MD5 and more. In SAC, pp. 103–119.

4. Audet, C., & Hare, W. (2017). Derivative-Free and Blackbox Optimization. Springer Series in Operations Research and Financial Engineering. Springer International Publishing.

5. Balyo, T., Froleyks, N., Heule, M., Iser, M., J ̈arvisalo, M., & Suda, M. (Eds.). (2021). Proceedings of SAT Competition 2021: Solver and Benchmark Descriptions. Department of Computer Science, University of Helsinki.

6. Balyo, T., & Sinz, C. (2018). Parallel Satisfiability. In Handbook of Parallel Constraint Reasoning, pp. 3–29. Springer.

7. Bard, G. V. (2009). Algebraic Cryptanalysis (1st edition). Springer Publishing Company, Incorporated.

8. Biere, A. (2011). Preprocessing and inprocessing techniques in SAT. In HVC, p. 1.

9. Biere, A. (2016). Splatz, Lingeling, Plingeling, Treengeling, YalSAT Entering the SAT Competition 2016. In Proc. of SAT Competition 2016 – Solver and Benchmark Descriptions, pp. 44–45.

10. Biere, A., Fleury, M., & Heisinger, M. (2021a). CaDiCaL, Kissat, Paracooba entering the SAT Competition 2021. In SAT Competition 2021 – Solver and Benchmark Descriptions, pp. 10–13.

11. Biere, A., Heule, M., van Maaren, H., & Walsh, T. (Eds.). (2021b). Handbook of Satisfiability - Second Edition, Vol. 336 of Frontiers in Artificial Intelligence and Applications. IOS Press.

12. B ̈ohm, M., & Speckenmeyer, E. (1996). A fast parallel SAT-solver - efficient workload balancing. Ann. Math. Artif. Intell., 17(3-4), 381–400.

13. Brakensiek, J., Heule, M., Mackey, J., & Narv ́aez, D. E. (2022). The resolution of Keller’s conjecture. J. Autom. Reason., 66(3), 277–300.

14. Bright, C., Cheung, K. K. H., Stevens, B., Kotsireas, I. S., & Ganesh, V. (2021). A SAT-based resolution of Lam’s problem. In AAAI, pp. 3669–3676.

15. Cai, S., Zhang, X., Fleury, M., & Biere, A. (2022). Better decision heuristics in CDCL through local search and target phases. J. Artif. Intell. Res., 74, 1515–1563.

16. Carter, K., Foltzer, A., Hendrix, J., Huffman, B., & Tomb, A. (2013). SAW: the software analysis workbench. In HILT, pp. 15–18.

17. Clarke, E. M., Kroening, D., & Lerda, F. (2004). A tool for checking ANSI-C programs. In TACAS, pp. 168–176.

18. Cook, S. A. (1971). The complexity of theorem-proving procedures. In STOC, pp. 151–158. ACM.

19. Cook, S. A., & Mitchell, D. G. (1996). Finding hard instances of the satisfiability problem: A survey. In Satisfiability Problem: Theory and Applications, pp. 1–17.

20. Damg ̊ard, I. (1989). A design principle for hash functions. In CRYPTO, pp. 416–427.

21. Davis, M., Logemann, G., & Loveland, D. W. (1962). A machine program for theorem-proving. Commun. ACM, 5(7), 394–397.

22. De, D., Kumarasubramanian, A., & Venkatesan, R. (2007). Inversion attacks on secure hash functions using SAT solvers. In SAT, pp. 377–382.

23. Dilkina, B., Gomes, C. P., & Sabharwal, A. (2007). Tradeoffs in the complexity of backdoor detection. In CP, pp. 256–270.

24. Dobbertin, H. (1996). Cryptanalysis of MD4. In FSE, pp. 53–69.

25. Dobbertin, H. (1998). The first two rounds of MD4 are not one-way. In FSE, pp. 284–292.

26. Dowling, W. F., & Gallier, J. H. (1984). Linear-time algorithms for testing the satisfiability of propositional horn formulae. J. Log. Program., 1(3), 267–284.

27. Frioux, L. L., Baarir, S., Sopena, J., & Kordon, F. (2017). PaInleSS: A framework for parallel SAT solving. In SAT 2017, pp. 233–250.

28. Froleyks, N., & Biere, A. (2021). Single clause assumption without activation literals to speed-up IC3. In FMCAD, pp. 72–76.

29. Garey, M. R., & Johnson, D. S. (1979). Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman.

30. Gladush, A., Gribanova, I., Kondratiev, V., Pavlenko, A., & Semenov, A. (2022). Measuring the effectiveness of SAT-based guess-and-determine attacks in algebraic cryptanalysis. In Parallel Computational Technologies, pp. 143–157.

31. Gomes, C. P., & Sabharwal, A. (2021). Exploiting runtime variation in complete solvers. In Handbook of Satisfiability - Second Edition, Vol. 336 of Frontiers in Artificial Intelligence and Applications, pp. 463–480. IOS Press.

32. Gomes, C. P., & Sellmann, M. (2004). Streamlined constraint reasoning. In CP, pp. 274–289.

33. Gribanova, I., & Semenov, A. (2018). Using automatic generation of relaxation constraints to improve the preimage attack on 39-step MD4. In MIPRO, pp. 1174–1179.

34. Gribanova, I., & Semenov, A. (2020). Constructing a set of weak values for full-round MD4 hash function. In MIPRO, pp. 1212–1217.

35. Gribanova, I., Zaikin, O., Kochemazov, S., Otpuschennikov, I., & Semenov, A. (2017). The study of inversion problems of cryptographic hash functions from MD family using algorithms for solving Boolean satisfiability problem. In Mathematical and Information Technologies, pp. 98–113.

36. Guo, J., Ling, S., Rechberger, C., & Wang, H. (2010). Advanced meet-in-the-middle preimage attacks: First results on full tiger, and improved results on MD4 and SHA-2. In ASIACRYPT, pp. 56–75.

37. Hamadi, Y., Jabbour, S., & Sais, L. (2009). ManySAT: a parallel SAT solver. J. Satisf. Boolean Model. Comput., 6(4), 245–262.

38. Heule, M. (2018a). Cube-and-Conquer Tutorial. https://github.com/marijnheule/CnC/.

39. Heule, M. (2018b). Schur number five. In AAAI, pp. 6598–6606.

40. Heule, M., Kullmann, O., & Biere, A. (2018). Cube-and-conquer for satisfiability. In Handbook of Parallel Constraint Reasoning, pp. 31–59. Springer.

41. Heule, M., Kullmann, O., & Marek, V. W. (2016). Solving and verifying the Boolean Pythagorean triples problem via Cube-and-Conquer. In SAT, pp. 228–245.

42. Heule, M., Kullmann, O., Wieringa, S., & Biere, A. (2011). Cube and conquer: Guiding CDCL SAT solvers by lookaheads. In HVC, pp. 50–65.

43. Heule, M. J. H., & van Maaren, H. (2021). Look-ahead based SAT solvers. In Handbook of Satisfiability - Second Edition, Vol. 336 of Frontiers in Artificial Intelligence and Applications, pp. 183–212. IOS Press.

44. Homsirikamol, E., Morawiecki, P., Rogawski, M., & Srebrny, M. (2012). Security margin evaluation of SHA-3 contest finalists through SAT-based attacks. In CISIM, pp. 56–67.

45. Hutter, F., Xu, L., Hoos, H. H., & Leyton-Brown, K. (2014). Algorithm runtime prediction: Methods & evaluation. Artificial Intelligence, 206, 79–111.

46. Hyv¨arinen, A. E. J., Junttila, T. A., & Niemel¨a, I. (2010). Partitioning SAT instances for distributed solving. In LPAR, pp. 372–386.

47. Jovanovic, D., & Janicic, P. (2005). Logical analysis of hash functions. In FroCoS, pp. 200–215.

48. Kautz, H. A., Sabharwal, A., & Selman, B. (2021). Incomplete algorithms. In Handbook of Satisfiability - Second Edition, Vol. 336 of Frontiers in Artificial Intelligence and Applications, pp. 213–232. IOS Press.

49. Kilby, P., Slaney, J. K., Thi´ebaux, S., & Walsh, T. (2005). Backbones and backdoors in satisfiability. In AAAI, pp. 1368–1373.

How to Cite

LEVERAGING CUBE-AND-CONQUER FOR CRYPTOGRAPHIC HASH FUNCTION PREIMAGE DISCOVERY: A SAT-BASED CRYPTANALYSIS PERSPECTIVE. (2024). European Journal of Emerging Artificial Intelligence, 1(01), 54-70. https://parthenonfrontiers.com/index.php/ejeai/article/view/48

Download Citation

ejeai Open Access Journal

European Journal of Emerging Artificial Intelligence

All issues

LEVERAGING CUBE-AND-CONQUER FOR CRYPTOGRAPHIC HASH FUNCTION PREIMAGE DISCOVERY: A SAT-BASED CRYPTANALYSIS PERSPECTIVE

Abstract

Keywords

References

How to Cite

Related articles

Journal Information

Journal Guidelines

Follow Us

Join Us

Contact Us

Share Link