Вычислительные методы и программирование
RUS  ENG    ЖУРНАЛЫ   ПЕРСОНАЛИИ   ОРГАНИЗАЦИИ   КОНФЕРЕНЦИИ   СЕМИНАРЫ   ВИДЕОТЕКА   ПАКЕТ AMSBIB  
Общая информация
Последний выпуск
Архив

Поиск публикаций
Поиск ссылок

RSS
Последний выпуск
Текущие выпуски
Архивные выпуски
Что такое RSS



Выч. мет. программирование:
Год:
Том:
Выпуск:
Страница:
Найти






Персональный вход:
Логин:
Пароль:
Запомнить пароль
Войти
Забыли пароль?
Регистрация


Вычислительные методы и программирование, 2024, том 25, выпуск 3, страницы 259–273
DOI: https://doi.org/10.26089/NumMet.v25r320
(Mi vmp1122)
 

Методы и алгоритмы вычислительной математики и их приложения

Применение алгоритмов решения проблемы булевой выполнимости для анализа финалистов конкурса 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
Тип публикации: Статья
УДК: 519.6
Образец цитирования: О. С. Заикин, В. В. Давыдов, А. П. Кирьянова, “Применение алгоритмов решения проблемы булевой выполнимости для анализа финалистов конкурса SHA-3”, Выч. мет. программирование, 25:3 (2024), 259–273
Цитирование в формате AMSBIB
\RBibitem{ZaiDavKir24}
\by О.~С.~Заикин, В.~В.~Давыдов, А.~П.~Кирьянова
\paper Применение алгоритмов решения проблемы булевой выполнимости для анализа финалистов конкурса SHA-3
\jour Выч. мет. программирование
\yr 2024
\vol 25
\issue 3
\pages 259--273
\mathnet{http://mi.mathnet.ru/vmp1122}
\crossref{https://doi.org/10.26089/NumMet.v25r320}
Образцы ссылок на эту страницу:
  • https://www.mathnet.ru/rus/vmp1122
  • https://www.mathnet.ru/rus/vmp/v25/i3/p259
  • Citing articles in Google Scholar: Russian citations, English citations
    Related articles in Google Scholar: Russian articles, English articles
    Вычислительные методы и программирование
     
      Обратная связь:
     Пользовательское соглашение  Регистрация посетителей портала  Логотипы © Математический институт им. В. А. Стеклова РАН, 2025