Journal Home
Login
Register
Open Access Journal
Submit a Paper
Propose a Special lssue
Open Access
ARTICLE
LEVERAGING CUBE-AND-CONQUER FOR CRYPTOGRAPHIC HASH FUNCTION PREIMAGE DISCOVERY: A SAT-BASED CRYPTANALYSIS PERSPECTIVE
Issue Vol. 1 No. 01 (2024): Volume 01 Issue 01 --- Section Articles
pdf
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
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.
