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

Представлен новый метод построения разностных путей в задаче поиска коллизий криптографических хеш-функций, основанный на использовании алгоритмов решения проблемы булевой выполнимости. На начальном этапе метода строится пропозициональная кодировка задачи поиска коллизий рассматриваемой хеш-функции. Затем в полученную кодировку добавляются (в виде КНФ) дополнительные ограничения. Как правило, это значения целочисленных разностей на сообщения, дающие коллизию, а также на отдельные фрагменты дифференциального пути. В качестве отправной точки поиска можно использовать некоторый известный либо случайный дифференциальный путь (во втором случае наличие коллизий, удовлетворяющих такому пути, не гарантируется). Задача варьирования значений разности переменных, кодирующих заполнение хеш-регистров, сводится к SAT. Для эффективного решения соответствующих серий SAT-задач написана MPI-программа, работающая на вычислительном кластере. Основным результатом стало построение дифференциального пути для задачи поиска коллизий криптографической хеш-функции MD4, отличного от известных.