Применение алгоритмов решения проблемы булевой выполнимости к криптоанализу хэш-функций семейства MD

Задачи поиска коллизий криптографических хэш-функций семейства MD рассматриваются как варианты задачи о булевой выполнимости (SAT). Для построения SAT-кодировок алгоритмов MD4 и MD5 использована система Transalg автоматической трансляции алгоритмических описаний дискретных функций в булевы уравнения. Полученные кодировки оказались существенно экономнее известных аналогов. В построенные SAT-кодировки хэш-функций добавлены дополнительные условия, кодирующие известные разностные атаки на данные функции. Время решения SAT-задач, кодирующих поиск одноблоковых коллизий для функции MD4, составило в среднем менее 1 с на ПК средней производительности. Для решения SAT-задач, кодирующих поиск двухблоковых коллизий для функции MD5, использованы параллельные SAT-решатели и вычислительный кластер. В результате был выделен класс двухблоковых коллизий для MD5 с 10 первыми нулевыми байтами. Построено несколько десятков коллизий такого типа. Рассмотрена также задача обращения хэш-функции MD4 (поиск прообраза для фиксированного хэша). В процессе решения данной задачи разработана техника, использующая так называемые “переменные переключения”. Использование переменных переключения позволило найти новые дополнительные условия (типа “условий Доббертина”), учёт которых ускорил решение проблемы обращения $39$-шагового варианта MD4 в сотни раз.