ГлавнаяАрхивНахождение прообразов неполнораундовой функции сжатия криптографической хеш-функции Skein-512-256 при помощи SAT-решателя

Нахождение прообразов неполнораундовой функции сжатия криптографической хеш-функции Skein-512-256 при помощи SAT-решателя | Прикладная дискретная математика. 2026. № 71. DOI: 10.17223/20710410/71/7

Рассматривается криптографическая хеш-функция Skein-512-256, вышедшая в 2010 г. в финал конкурса NIST на новую криптографическую хеш-функцию. Функция сжатия Skein-512-256 обрабатывает 512-битовый блок сообщения в течение 72 раундов, каждый раунд состоит из 12 операций. Предлагается практическая алгебраическая атака нахождения прообраза на неполнораундовые версии функции сжатия Skein-512-256. Соответствующие вычислительные задачи сводятся к экземплярам проблемы булевой выполнимости (SAT). С помощью последовательного SAT-решателя были найдены прообразы функции сжатия Skein-512-256, состоящей из первого раунда и семи первых операций второго раунда. Задействование параллельного SAT-решателя позволило увеличить число операций второго раунда до восьми. Ранее в литературе была предложена практическая атака нахождения прообраза максимум на один раунд функции сжатия Skein-512-256.
  • Title Нахождение прообразов неполнораундовой функции сжатия криптографической хеш-функции Skein-512-256 при помощи SAT-решателя
  • Headline Нахождение прообразов неполнораундовой функции сжатия криптографической хеш-функции Skein-512-256 при помощи SAT-решателя
  • Publesher Tomask State UniversityTomsk State University
  • Issue Прикладная дискретная математика 71
  • Date:
  • DOI 10.17223/20710410/71/7
Ключевые слова
криптографическая хеш-функция, Skein, атака нахождения прообраза, алгебраический криптоанализ, SAT
Авторы
Ссылки
Алферов А. П., Зубов А. Ю., Кузьмин А. С., Черемушкин А. В. Основы криптографии. 2-е изд. М.: Гелиос АРВ, 2002. 480с.
https://www.schneier.com/academic/skein/ - The Skein Hash Function Family. 2010.
Homsirikamol E., Morawiecki P., Rogawski M., and Srebrny M. Security margin evaluation of SHA-3 contest finalists through SAT-based attacks // LNCS. 2012. V.7564. P.56-67.
Bard G. V. Algebraic Cryptanalysis. N.Y.: Springer, 2009. 356 p.
Семёнов А. А., Беспалов Д. В. Технологии решения многомерных задач логического поиска // Вести. Том. гос. ун-та. 2005. У 14. С. 61-73.
Marques-Silva J. and Sakallah К. GRASP: a search algorithm for propositional satisfiability // IEEE Trans.Computers. 1999. Y. IK. No. 5. P.506-521.
Mironov I. and Zhang Z. Applications of SAT solvers to cryptanalysis of hash functions // LNCS. 2006. V. 4121. P. 102-115.
Heule M. J. H., Kullmann O., Wieringa S., and Biere A. Cube and Conquer: guiding CDCL SAT solvers by lookaheads // LNCS. 2012. V.7261. P.50-65.
Maty as S. M., Meyer С. H., and Oseas J. Generating strong one-way functions with cryptographic algorithm // IBM Techn. Disclosure Bull. 1985. V. 27. No. 10A. P.5658-5659.
Khovratovich D., Rechberger C., and Savelieva A. Bicliques for preimages: attacks on Skein-512 and the SHA-2 family // LNCS. 2012. V.7549. P.244-263.
Отпущенников И. В., Семенов А. А. Технология трансляции комбинаторных проблем в булевы уравнения j j Прикладная дискретная математика. 2011. №1(11). С. 96-115.
Clarke Е. М., Kroening D., and Lerda F. A tool for checking ANSI-C programs // LNCS. 2004. V. 2978. P.168-176.
Заикин О. С., Давыдов В. В., Кирьянова А. П. Применение алгоритмов решения проблемы булевой выполнимости для анализа финалистов конкурса SHA-3 // Ввіч. мет. программирование. 2024. Т. 25. Ввіп. 3. С. 259-273.
Biere A., Fleury M. Gimsatul, IsaSAT and Kissat entering the SAT Competition 2022 // Proceedings of SAT Competition 2022: Solver and Benchmark Descriptions / T. Balyo, M. Heule, M. Iser, M. Järvisalo, M. Suda (eds.). - Helsinki: Department of Computer Science, University of Helsinki, 2022. P. 10-11.
Heule M. J. H., Kullmann O., and Marek V. W. Solving and verifying the Boolean Pythagorean triples problem via Cube-and-Conquer // LNCS. 2016. V.9710. P.228-245.
Zaikin O. Inverting cryptographic hash functions via Cube-and-Conquer // J. Artif.Int. Res. 2024. V.81. P.359-399.
Zaikin O. Inverting step-reduced SHA-1 and MD5 by parameterized SAT solvers // Proc. CP 2024. Leibniz Intern. Proc. Informatics (LIPIcs). 2024. V. 307. P. 31:1-31:19.
Andreev A., Chukharev K., Kochemazov S., and Semenov A. Using backdoors to generate learnt information in SAT solving // Proc. ECAI 2024. P.4173-4180.
Zaikin O. IterCnC: Реализация итеративного препроцессинга КНФ при помощи Cube-and-Conquer [Электронный ресурс] // GitHub. - 2025. - URL: https://github.com/olegzaikin/IterCnC.
Нахождение прообразов неполнораундовой функции сжатия криптографической хеш-функции Skein-512-256 при помощи SAT-решателя | Прикладная дискретная математика. 2026. № 71. DOI: 10.17223/20710410/71/7
Нахождение прообразов неполнораундовой функции сжатия криптографической хеш-функции Skein-512-256 при помощи SAT-решателя | Прикладная дискретная математика. 2026. № 71. DOI: 10.17223/20710410/71/7