ntvНаучно-технический вестник информационных технологий, механики и оптикиScientific and Technical Journal of Information Technologies, Mechanics and Optics2226-14942500-0373Университет ИТМО10.17586/2226-1494-2025-25-3-428-437ntv-466Research ArticleКОМПЬЮТЕРНЫЕ СИСТЕМЫ И ИНФОРМАЦИОННЫЕ ТЕХНОЛОГИИCOMPUTER SCIENCEАнализ криптографической стойкости хеш-функции SHA-256 при помощи SAT-подходаAnalysis of the cryptographic strength of the SHA-256 hash function using the SAT approachhttps://orcid.org/0000-0002-5544-2434ДавыдовВ. В.DavydovV. V.

Давыдов Вадим Валерьевич — кандидат технических наук, криптограф-исследователь

Москва, 121205;

Доцент

190000, Санкт-Петербург;

научный сотрудник

Санкт-Петербург, 197101

sc 57203909696

Vadim V. Davydov — PhD, Cryptography Researcher

Moscow, 121205;

Associate Professor

190000, Saint Petersburg;

Scientific Researcher

197101, Saint Petersburg

sc 57203909696

vadimdavydov@outlook.comhttps://orcid.org/0009-0000-2173-0844ПихтовниковМ. Д.PikhtovnikovM. D.

Пихтовников Михаил Денисович — студент

Таганрог, 347922

Michail D. Pikhtovnikov — Student

Taganrog, 347922

pikhtovnikov347@mail.ruhttps://orcid.org/0009-0006-0344-5111КирьяноваА. П.KiryanovaA. P.

Кирьянова Анастасия Павловна — аспирант

Санкт-Петербург, 197101

Anastasia P. Kiryanova — PhD Student

197101, Saint Petersburg

anastaciakosanovskaya@gmail.comhttps://orcid.org/0000-0002-0145-5010ЗаикинО. С.ZaikinO. S.

Заикин Олег Сергеевич — кандидат технических наук, научный сотрудник

Новосибирск, 630090;

ведущий научный сотрудник

Иркутск, 664033

sc 56786079600

Oleg S. Zaikin — PhD, Researcher

Novosibirsk, 630090;

Leading Researcher

Irkutsk, 664033

sc 56786079600

oleg.zaikin@icc.ruООО «КуАпп»; Санкт-Петербургский государственный университет аэрокосмического приборостроения; Университет ИТМОРоссияQApp; Saint Petersburg State University of Aerospace Instrumentation (SUAI); ITMO UniversityRussian FederationЮжный федеральный университетРоссияSouthern Federal UniversityRussian FederationУниверситет ИТМОРоссияITMO UniversityRussian FederationНовосибирский государственный университет; Институт динамики систем и теории управления имени В.М. Матросова Сибирского отделения Российской академии наукРоссияNovosibirsk State University; Matrosov Institute for System Dynamics and Control Theory of Siberian Branch of RASRussian Federation202503072025253428437Copyright © Давыдов В.В., Пихтовников М.Д., Кирьянова А.П., Заикин О.С., 20252025Давыдов В.В., Пихтовников М.Д., Кирьянова А.П., Заикин О.С.Davydov V.V., Pikhtovnikov M.D., Kiryanova A.P., Zaikin O.S.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://ntv.elpub.ru/jour/article/view/466

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

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.

криптографическая хеш-функцияSHA-256SATлогический криптоанализдифференциальный криптоанализcryptographic hash functionSHA-256SATlogical cryptanalysisdifferential cryptanalysisРабота Вадима Валерьевича Давыдова и Анастасии Павловны Кирьяновой выполнена в рамках государственного задания (проект FSER-2025-0003). Олег Сергеевич Заикин выполнил свою часть работы при поддержке Математического центра в Академгородке, соглашение с Министерством науки и высшего образования Российской Федерации № 075-15-2025-349. Работа является расширенной версией результатов, полученных в рамках летней школы-конференции «Криптография и информационная безопасность» в 2024 году.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.ReferencesSecure hash standard (shs) // Fips pub. 2012. V. 180. N 4.Secure hash standard (shs). Fips pub, 2012, vol. 180, no. 4.Alamgir N. Programmatic SAT for SHA-256 Collision Attack. 2024 [Электронный ресурс]. URL:https://scholar.uwindsor.ca/etd/9525 (дата обращения: 12.07.2024).Alamgir N. Programmatic SAT for SHA-256 Collision Attack. 2024 Available at: https://scholar.uwindsor.ca/etd/9525 (accessed: 12.07.2024).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_15Khovratovich 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_15Homsirikamol 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_4Homsirikamol 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_4Hosoyamada 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_22Hosoyamada 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_22Li 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_6Li 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_6Damgard 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_39Damgard 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_39Merkle 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_21Merkle 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_21Al-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.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.Gauravaram P. Cryptographic Hash Functions: Cryptanalysis, Design and Applications. PhD thesis. Queensland University of Technology. 2007. 298 p.Gauravaram P. Cryptographic Hash Functions: Cryptanalysis, Design and Applications. PhD thesis. Queensland University of Technology, 2007, 298 p.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.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.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_47Nejati 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Заикин О.С., Давыдов В.В., Кирьянова А.П. Применение алгоритмов решения проблемы булевой выполнимости для анализа финалистов конкурса SHA-3 // Вычислительные методы и программирование. 2024. Т. 25. С. 259–273. https://doi.org/10.26089/NumMet.v25r320Zaikin 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.v25r320Alamgir N., Nejati S., Bright C. SHA-256 collision attack with programmatic SAT // CEUR Workshop Proceedings. 2024. V. 3717. P. 91–110.Alamgir N., Nejati S., Bright C. SHA-256 collision attack with programmatic SAT. CEUR Workshop Proceedings, 2024, vol. 3717, pp. 91–110.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_22Guo 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_22Biham 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/BF00630563Biham 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/BF00630563Wang 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_2Wang 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_2Wang 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_1Wang 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_1Wang 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_1Wang 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_1Isobe 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_9Isobe 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_9Guo 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_4Guo 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_4Mendel 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_9Mendel 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_9Mendel 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_16Mendel 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_16Clarke 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_15Clarke 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_15Semenov 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)2020Semenov 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)2020Nejati S. SAT Encoding [Электронный ресурс]. URL: https://github.com/saeednj/SAT-encoding (дата обращения: 12.07.2024).Nejati S. SAT Encoding. Available at: https://github.com/saeednj/ SAT-encoding (accessed: 12.07.2024).Biere A. The Kissat SAT Solver [Электронный ресурс]. URL: https://github.com/arminbiere/kissat.git (дата обращения: 12.07.2024).Biere A. The Kissat SAT Solver. Available at: https://github.com/arminbiere/kissat.git (accessed: 12.07.2024).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.769433Marques-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.769433Otpuschennikov I. Programs for SHA-256 [Электронный ресурс]. URL: https://gitlab.com/satencodings/satencodings/-/tree/master/SHA2?ref_type=heads (дата обращения: 12.07.2024).Otpuschennikov I. Programs for SHA-256. Available at: https://gitlab.com/satencodings/satencodings/-/tree/master/SHA2?ref_type=heads (accessed: 12.07.2024).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_11Semenov 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_11Zaikin 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.15244Zaikin 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Заикин О. КНФ для SHA-256 [Электронный ресурс]. URL: https://github.com/olegzaikin/sha256sat.git (дата обращения: 20.02.2025).Zaikin O. CNF for SHA-256. Available at: https://github.com/olegzaikin/sha256sat.git (accessed: 20.02.2025). (in Russian)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_8Sanadhya 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

The authors declare that there are no conflicts of interest present.