Анализ криптографической стойкости хеш-функции SHA-256 при помощи SAT-подхода

Введение. В современных системах обеспечения информационной безопасности криптографические хешфункции играют значительную роль и выполняют такие важные задачи, как обеспечение целостности данных и их эффективное сжатие. Одной из наиболее значимых и широко применяемых криптографических хешфункций является SHA-256 из семейства SHA-2. Исследование криптографической стойкости SHA-256 является актуальной научной задачей и решается с применением современных подходов криптоанализа к атакам нахождения прообразов и коллизий с акцентом на практическую осуществимость таких атак.
Метод. В представленной работе для поиска прообразов неполнораундовых версий функции сжатия SHA-256 применен логический криптоанализ, согласно которому исходная задача криптоанализа сводится к проблеме булевой выполнимости (SAT). Для поиска коллизий совместно применены логический и дифференциальный криптоанализы.
Основные результаты. Выполнено сравнение эффективности различных способов сведения функции сжатия SHA-256 к SAT. Впервые найдены прообразы для 17- и 18-раундовых функций сжатия SHA-256, а также прообразы для ослабленной 19-раундовой функции сжатия. Построены базовые дифференциальные пути, с помощью которых быстрее найдены коллизии 18-раундовой функции сжатия. В результате сведения к SAT известных дифференциальных путей найдены коллизии 19-раундовой функции сжатия.
Обсуждение. Продемонстрирована возможность комбинирования двух методов криптоанализа с целью повышения эффективности анализа криптографических алгоритмов. Результаты исследования подтвердили, что полнораундовая хеш-функция SHA-256 остается устойчивой к атакам, направленным на нахождение прообразов и коллизий, в рамках примененного SAT-подхода.

1. Secure hash standard (shs) // Fips pub. 2012. V. 180. N 4.

2. Alamgir N. Programmatic SAT for SHA-256 Collision Attack. 2024 [Электронный ресурс]. URL:https://scholar.uwindsor.ca/etd/9525 (дата обращения: 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. V. 7549. P. 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. V. 7564. P. 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. V. 12825. P. 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. V. 14651. P. 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. P. V. 435. P. 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. V. 435. P. 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. P. 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. P. 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. V. 11008. P. 737–754. https://doi.org/10.1007/978-3-319-98334-9_47

13. Заикин О.С., Давыдов В.В., Кирьянова А.П. Применение алгоритмов решения проблемы булевой выполнимости для анализа финалистов конкурса SHA-3 // Вычислительные методы и программирование. 2024. Т. 25. С. 259–273. 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. V. 3717. P. 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. V. 13793. P. 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. V. 4. N 1. P. 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. V. 3494. P. 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. V. 3494. P. 1–18. https://doi.org/10.1007/11426639_1

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

20. Isobe T., Shibutani K. Preimage attacks on reduced Tiger and SHA2 // Lecture Notes in Computer Science. 2009. V. 5665. P. 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. V. 6477. P. 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. V. 4047. P. 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. V. 7881. P. 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. V. 2988. P. 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. V. 16. N 1. P. 29. https://doi.org/10.23638/LMCS-16(1:29)2020

26. Nejati S. SAT Encoding [Электронный ресурс]. URL: https://github.com/saeednj/SAT-encoding (дата обращения: 12.07.2024).

27. Biere A. The Kissat SAT Solver [Электронный ресурс]. URL: https://github.com/arminbiere/kissat.git (дата обращения: 12.07.2024).

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

29. Otpuschennikov I. Programs for SHA-256 [Электронный ресурс]. URL: https://gitlab.com/satencodings/satencodings/-/tree/master/SHA2?ref_type=heads (дата обращения: 12.07.2024).

30. Semenov A., Zaikin O., Kochemazov S. Finding effective SAT partitionings via black-box optimization // Springer Optimization and Its Applications. 2021. V. 170. P. 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. V. 81. P. 359–399. https://doi.org/10.1613/jair.1.15244

32. Заикин О. КНФ для SHA-256 [Электронный ресурс]. URL: https://github.com/olegzaikin/sha256sat.git (дата обращения: 20.02.2025).

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