ENG
РУС
Search
Menu
About the Edition
Open Access Statement
Editorial Board
Editorial Policy
Editorial Ethics
Rules for peer-review
Rules for presentation of papers
Forms of Submitted Documents
Recommendations for the Design of References to Our Journal
Editorial Staff
Information for Subscribers
Summaries of the Issue
List of Authors
Issues
Publishers license agreement
Procedure of work with personal data
Publications
2025
2024
2023
2022
2021
2020
2019
2018
2017
2016
2015
2014
2013
2012
2011
2010
2009
2008
2007
2006
2005
2004
2003
2002
2001
Editor-in-Chief

Nikiforov
Vladimir O.
D.Sc., Prof.
Partners













































doi: 10.17586/2226-1494-2025-25-3-428-437

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

V. V. Davydov, M. D. Pikhtovnikov, A. P. Kiryanova, O. S. Zaikin


Read the full article  ';
Article in Russian

For citation:
Davydov V.V., Pikhtovnikov M.D., Kiryanova A.P., Zaikin O.S. Analysis of the cryptographic strength of the SHA-256 hash function using the SAT approach. Scientific and Technical Journal of Information Technologies, Mechanics and Optics, 2025, vol. 25, no. 3, pp. 428–437 (in Russian). doi: 10.17586/2226-1494-2025-25-3-428-437


Abstract
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.

Keywords: cryptographic hash function, SHA-256, SAT, logical cryptanalysis, differential cryptanalysis

Acknowledgements. The work of Vadim Davydov and Anastasia Kiryanova was performed within the framework of the State Assignment (project No. FSER-2025-0003). Oleg Zaikin was funded by the Mathematical Center in Akademgorodok under the Agreement No. 075-15-2025-349 with the Ministry of Science and Higher Education of the Russian Federation. The present paper is an extension of results obtained during the summer school-conference “Cryptography and information security” in 2024.

References
  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 SHA-256 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-the-middle 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. NejatiS. SATEncoding. 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-and-Conquer. Journal of Artificial Intelligence Research, 2024,vol. 81,pp. 359–399. https://doi.org/10.1613/jair.1.15244
  32. Zaikin O. CNFforSHA-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


Creative Commons License

This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License
Copyright 2001-2025 ©
Scientific and Technical Journal
of Information Technologies, Mechanics and Optics.
All rights reserved.

Яндекс.Метрика