Применение алгоритмов решения проблемы булевой выполнимости для анализа финалистов конкурса SHA-3

Рассматриваются финалисты конкурса SHA-3, организованного для принятия нового стандарта криптографической хеш-функции. Все пять финалистов до сих пор являются стойкими к поиску прообраза, т.е. для них невозможно за реальное время найти вход по известному выходу. Исследуется возможность нахождения прообразов неполнораундовых версий рассмотренных криптографических хеш-функций. Соответствующие задачи сведены к проблеме булевой выполнимости (SAT) с помощью инструментального средства CBMC, предназначенного для проверки свойств программ на языке C. Для решения построенных экземпляров SAT использован современный решатель Kissat. В сравнении с ранее опубликованными результатами, для четырех из пяти функций-финалистов удалось найти прообразы более сложных неполнораундовых версий.