|
Методы и алгоритмы вычислительной математики и их приложения
Применение алгоритмов решения проблемы булевой выполнимости для анализа финалистов конкурса SHA-3
О. С. Заикинab, В. В. Давыдовcd, А. П. Кирьяноваe a Институт динамики систем и теории управления имени В.М. Матросова Сибирского отделения Российской академии наук, г. Иркутск
b Новосибирский государственный университет
c Санкт-Петербургский государственный университет аэрокосмического приборостроения
d Компания QAPP
e Университет ИТМО
Аннотация:
Рассматриваются финалисты конкурса SHA-3, организованного для принятия нового стандарта криптографической хеш-функции. Все пять финалистов до сих пор являются стойкими к поиску прообраза, т.е. для них невозможно за реальное время найти вход по известному выходу. Исследуется возможность нахождения прообразов неполнораундовых версий рассмотренных криптографических хеш-функций. Соответствующие задачи сведены к проблеме булевой выполнимости (SAT) с помощью инструментального средства CBMC, предназначенного для проверки свойств программ на языке C. Для решения построенных экземпляров SAT использован современный решатель Kissat. В сравнении с ранее опубликованными результатами, для четырех из пяти функций-финалистов удалось найти прообразы более сложных неполнораундовых версий.
Ключевые слова:
проблема булевой выполнимости, SAT-решатель, Kissat, CBMC, проверка свойств программ, криптографическая хеш-функция, поиск прообраза, конкурс SHA-3.
Поступила в редакцию: 26.12.2023
Образец цитирования:
О. С. Заикин, В. В. Давыдов, А. П. Кирьянова, “Применение алгоритмов решения проблемы булевой выполнимости для анализа финалистов конкурса SHA-3”, Выч. мет. программирование, 25:3 (2024), 259–273
Образцы ссылок на эту страницу:
https://www.mathnet.ru/rus/vmp1122 https://www.mathnet.ru/rus/vmp/v25/i3/p259
|
|