Analysis of the cryptographic strength of the SHA-256 hash function using the SAT approach

Cryptographic hash functions play a significant role in modern information security systems by ensuring data integrity and enabling efficient data compression. One of the most important and widely used cryptographic hash functions is SHA-256 that belongs to the SHA-2 family. In this regard, the study of SHA-256 cryptographic resistance using modern cryptanalysis approaches to preimage and collision attacks with an emphasis on the practical feasibility of such attacks is an urgent scientific task. To search for preimages of round-reduced versions of the SHA-256 compression function, the logical cryptanalysis was applied, i.e., cryptanalysis problems were reduced to the Boolean satisfiability problem (SAT). For collision attacks, a combination of logical and differential cryptanalysis was utilized. The work presents a comparison between various methods for reducing the SHA-256 compression function to SAT and evaluates their efficiency. As a result of the work, preimages for 17- and 18-round SHA-256 compression functions were found for the first time as well as preimages for a weakened 19-round compression function. Basic differential paths were constructed, which facilitated faster finding of collisions for the 18-round compression function. Known differential paths were reduced in SAT leading to finding collisions for the 19-round compression function. The work demonstrates the possibility of combining two cryptanalysis methods to enhance the efficiency of analyzing cryptographic algorithms. The results of the study confirm that the full-round SHA-256 hash function remains resistant to preimage and collision attacks within the scope of the applied SAT-based approach.

1. Secure hash standard (shs). Fips pub, 2012, vol. 180, no. 4.

2. Alamgir N. Programmatic SAT for SHA-256 Collision Attack. 2024 Available at: https://scholar.uwindsor.ca/etd/9525 (accessed: 12.07.2024).

3. Khovratovich D., Rechberger C., Savelieva A. Bicliques for preimages: attacks on Skein-512 and the SHA-2 family. Lecture Notes in Computer Science. 2012, vol. 7549, pp. 244–263. https://doi.org/10.1007/978-3-642-34047-5_15

4. Homsirikamol E., Morawiecki P., Rogawski M., Srebrny M. Security margin evaluation of SHA-3 contest finalists through SAT-based attacks. Lecture Notes in Computer Science, 2012, vol. 7564, pp. 56–67. https://doi.org/10.1007/978-3-642-33260-9_4

5. Hosoyamada A., Sasaki Y. Quantum collision attacks on reduced SHA256 and SHA-512. Lecture Notes in Computer Science, 2021, vol. 12825, pp. 616–646. https://doi.org/10.1007/978-3-030-84242-0_22

6. Li Y., Liu F., Wang G. New records in collision attacks on SHA-2. Lecture Notes in Computer Science, 2024, vol. 14651, pp. 158–186. https://doi.org/10.1007/978-3-031-58716-0_6

7. Damgard I.B. A design principle for hash functions. Lecture Notes in Computer Science, 1990, vol. 435, pp. 416–427. https://doi.org/10.1007/0-387-34805-0_39

8. Merkle R.C. A certified digital signature. Lecture Notes in Computer Science, 1990, vol. 435, pp. 218–238. https://doi.org/10.1007/0-387-34805-0_21

9. Al-Kuwari S., Davenport J.H., Bradford R. J. Cryptographic hash functions: Recent design trends and security notions. Proc. of the 6th China International Conference on Information Security and Cryptology (Inscrypt ‘10), 2010, pp. 133–150.

10. Gauravaram P. Cryptographic Hash Functions: Cryptanalysis, Design and Applications. PhD thesis. Queensland University of Technology, 2007, 298 p.

11. Courtois N.T., Jackson K., Ware D. Fault-algebraic attacks on inner rounds of DES. Proc. of the E-Smart’10, 2010, pp. 22–24.

12. Nejati S., Horacek J., Gebotys C., Ganesh V. Algebraic fault attack on sha hash functions using programmatic SAT solvers. Lecture Notes in Computer Science, 2018, vol. 11008, pp. 737–754. https://doi.org/10.1007/978-3-319-98334-9_47

13. Zaikin O.S., Davydov V.V., Kiryanova A.P. SAT-based analysis of SHA-3 competition finalists. Numerical Methods and Programming, 2024, vol. 25, pp. 259–273. (in Russian). https://doi.org/10.26089/NumMet.v25r320

14. Alamgir N., Nejati S., Bright C. SHA-256 collision attack with programmatic SAT. CEUR Workshop Proceedings, 2024, vol. 3717, pp. 91–110.

15. Guo J., Liu G., Song L., Tu Y. Exploring SAT for cryptanalysis:(Quantum) collision attacks against 6-round SHA-3. Lecture Notes in Computer Science, 2022, vol. 13793, pp. 645–674. https://doi.org/10.1007/978-3-031-22969-5_22

16. Biham E., Shamir A. Differential cryptanalysis of DES-like cryptosystems. Journal of Cryptology, 1991, vol. 4, no. 1, pp. 3–72. https://doi.org/10.1007/BF00630563

17. Wang X., Yu H. How to break MD5 and other hash functions. Lecture Notes in Computer Science, 2005, vol. 3494, pp. 19–35. https://doi.org/10.1007/11426639_2

18. Wang X., Lai X., Feng D., Chen H., Yu X. Cryptanalysis of the hash functions MD4 and RIPEMD. Lecture Notes in Computer Science, 2005, vol. 3494, pp. 1–18. https://doi.org/10.1007/11426639_1

19. Wang X., Yu H., Yin Y.L. Efficient collision search attacks on SHA-0. Lecture Notes in Computer Science, 2005, vol. 3621, pp. 1–16. https://doi.org/10.1007/11535218_1

20. Isobe T., Shibutani K. Preimage attacks on reduced Tiger and SHA-2. Lecture Notes in Computer Science, 2009, vol. 5665, pp. 139–155. https://doi.org/10.1007/978-3-642-03317-9_9

21. Guo J., Ling S., Rechberger C., Wang H. Advanced meet-in-themiddle preimage attacks: First results on full Tiger, and improved results on MD4 and SHA-2. Lecture Notes in Computer Science, 2010, vol. 6477, pp. 56–75. https://doi.org/10.1007/978-3-642-17373-8_4

22. Mendel F., Pramstaller N., Rechberger C., Rijmen V. Analysis of step-reduced sha-256. Lecture Notes in Computer Science, 2006, vol. 4047, pp. 126–143. https://doi.org/10.1007/11799313_9

23. Mendel F., Nad T., Schläffer M. Improving local collisions: New attacks on reduced SHA-256. Lecture Notes in Computer Science, 2013, vol. 7881, pp. 262–278. https://doi.org/10.1007/978-3-642-38348-9_16

24. Clarke E., Kroening D., Lerda F. A tool for checking ANSI-C programs. Lecture Notes in Computer Science, 2004, vol. 2988, pp. 168–176. https://doi.org/10.1007/978-3-540-24730-2_15

25. Semenov A., Otpuschennikov I., Gribanova I., Zaikin O., Kochemazov S. Translation of algorithmic descriptions of discrete functions to SAT with applications to cryptanalysis problems. Logical Methods in Computer Science, 2020, vol. 16, no. 1, pp. 29. https://doi.org/10.23638/LMCS-16(1:29)2020

26. Nejati S. SAT Encoding. Available at: https://github.com/saeednj/ SAT-encoding (accessed: 12.07.2024).

27. Biere A. The Kissat SAT Solver. Available at: https://github.com/arminbiere/kissat.git (accessed: 12.07.2024).

28. Marques-Silva J.P., Sakallah K.A. GRASP: A search algorithm for propositional satisfiability. IEEE Transactions on Computers, 1999, vol. 48, no. 5, pp. 506–521. https://doi.org/10.1109/12.769433

29. Otpuschennikov I. Programs for SHA-256. Available at: https://gitlab.com/satencodings/satencodings/-/tree/master/SHA2?ref_type=heads (accessed: 12.07.2024).

30. Semenov A., Zaikin O., Kochemazov S. Finding effective SAT partitionings via black-box optimization. Springer Optimization and Its Applications, 2021, vol. 170, pp. 319–355. https://doi.org/10.1007/978-3-030-66515-9_11

31. Zaikin O. Inverting cryptographic hash functions via Cube-andConquer. Journal of Artificial Intelligence Research, 2024, vol. 81, pp. 359–399. https://doi.org/10.1613/jair.1.15244

32. Zaikin O. CNF for SHA-256. Available at: https://github.com/olegzaikin/sha256sat.git (accessed: 20.02.2025). (in Russian)

33. Sanadhya S.K., Sarkar P. Attacking reduced round SHA-256. Lecture Notes in Computer Science, 2008, vol. 5037, pp. 130–143. https://doi.org/10.1007/978-3-540-68914-0_8