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

Рассмотрена реализация разностной атаки на криптографические хеш-функции MD4 (Message Digest 4) и MD5 (Message Digest 5) через сведение задачи поиска коллизий для этих хеш-функций к задаче о булевой выполнимости (SAT, SATisfiability). Новизна полученных результатов заключается в том, что предложены существенно более экономные (в сравнении с известными) SAT-кодировки рассматриваемых алгоритмов, а также в использовании для решения полученных SAT-задач современных многопоточных и параллельных SAT-решателей. Задачи поиска одноблоковых коллизий для MD4 в данной постановке оказались чрезвычайно простыми. Кроме того, найдены несколько десятков двухблоковых коллизий для MD5. В процессе соответствующих вычислительных экспериментов определен некоторый класс сообщений, дающих коллизии: построено множество пар дающих коллизии сообщений, у которых первые 10 байтов нулевые.