Проблема булевой выполнимости и ее применение в криптоанализе

Алгоритмы решения проблемы булевой выполнимости (SAT – от Satisfiability) и реализующие их средства (SAT-решатели) позволяют определить выполнимость конкретной булевой формулы – существует ли такой набор определенных булевых значений («ложь»/«истина») переменных формулы, при которых результат формулы становится истинным.

Проблема булевой выполнимости хорошо изучена; существуют различные методы сведения разного рода частных задач к формулировке на их основе конкретной булевой формулы и последующего решения определенного экземпляра задачи с помощью алгоритмов решения проблемы булевой выполнимости. Алгоритмический аппарат также активно развивается; в частности, предложены эффективные алгоритмы, позволяющие автоматизировать поиск значений переменных, приводящих к решению проблемы булевой выполнимости [1]. Алгоритмы, лежащие в основе SAT-решателей, хорошо распараллеливаются, что позволяет эффективно использовать вычислительные кластеры [2].

В анализе криптографических алгоритмов существует достаточно много задач, которые могут быть сведены к решению проблемы булевой выполнимости, что позволяет использовать хорошо изученный математический и эффективный алгоритмический аппарат решения SAT-задач для доказательства криптографических свойств (или для получения информации о криптографических свойствах) анализируемого алгоритма. В этой статье мы совместно с моей коллегой – ведущим аналитиком компании «Актив» Мариной Скоробогатовой – подготовили небольшой обзор применений подхода сведения задач криптоанализа к SAT-задачам, который и предлагаем вам под катом.

О задаче булевой выполнимости и ее применении в криптоанализе

На практике обычно применяются булевы формулы в конъюнктивной нормальной форме (КНФ), представляющие собой конъюнкцию дизъюнктов логических переменных или их отрицаний (литералов). Простейший пример формулы в КНФ, содержащей 2 переменных и 2 операции конъюнкции [3]:

Для сравнения с реальными формулами, которые могут быть использованы в криптоанализе: полнораундовый алгоритм шифрования DES кодируется немногим более 10 тыс. переменных и 60 тыс. конъюнкций (отметим, что это минимальный размер формулы – для одной пары блоков известного открытого текста и шифртекста) [4]. 

Как было сказано выше, в криптоанализе различных алгоритмов можно использовать редукцию основной задачи к SAT-задаче, задействуя для ее решения существующий алгоритмический аппарат, а также разработанные в достаточно большом количестве программные средства (SAT-решатели). Отметим, что практически все алгоритмы решения SAT-задач основаны на построении и предъявлении набора булевых переменных, при котором анализируемая формула выполняется. 

Данный подход получил название «логического криптоанализа» (logical cryptanalysis), которое было изначально предложено в работе [4]. Впоследствии также стал применяться термин «SAT-криптоанализ» (SAT-based cryptanalysis, SAT cryptanalysis), подчеркивающий использование проблемы булевой выполнимости; SAT-криптоанализ может рассматриваться как частный случай алгебраического криптоанализа [3].

Какие алгоритмы и задачи могут быть проанализированы

Основные направления применения SAT-решателей с целью анализа различных криптографических алгоритмов можно классифицировать следующим образом (приведены примеры известных работ, в которых были достигнуты некоторые результаты с помощью SAT-криптоанализа):

1. Анализ алгоритмов блочного шифрования:

• поиск секретного ключа (атаки на основе известных или выбранных открытых текстов [4-6]);

• поиск классов слабых ключей (например, по отношению к дифференциальному или линейному криптоанализу [7]);

• верификация ряда криптографических свойств блочных шифров (например, доказательство отсутствия универсальных или определенных классов слабых ключей [4, 7]).

2.Анализ алгоритмов аутентифицированного шифрования [8, 9]:

• извлечение внутреннего состояния и раскрытие открытого текста;

• поиск секретного ключа;

• нахождение коллизий – различных внутренних состояний, приводящих к одинаковому значения тега аутентификации (криптографической контрольной суммы, позволяющей проверить целостность шифруемых и присоединенных данных);

• подделка аутентифицированного сообщения.

3.Анализ алгоритмов поточного шифрования и генераторов псевдослучайных последовательностей:

• поиск секретного ключа поточного шифра (атака на основе известного открытого текста [10]);

• поиск начального заполнения генератора ключевого потока [10, 11].

4.Анализ функций хеширования:

• поиск прообразов [7, 10, 12];

• поиск коллизий (в том числе, путем поиска дифференциального пути с помощью SAT-решателя для последующего применения дифференциального криптоанализа [10]) [12].

Как выполняется SAT-криптоанализ 

Основная идея проведения SAT-криптоанализа состоит в том, чтобы закодировать поставленную криптоаналитическую задачу в виде КНФ и использовать SAT-решатели для нахождения выполняющего ее набора.

Этапы выполнения SAT-криптоанализа можно упрощенно описать следующим образом (на примере анализа алгоритма блочного шифрования по известным парам открытых текстов и шифртекстов):

1. Биты открытого текста, ключа и шифртекста представляются в виде последовательностей булевых переменных (соответственно, P, K и C). Каждая переменная принимает значения 1 (true) или 0 (false).

2. Кодируется исследуемое свойство анализируемого алгоритма в виде булевой формулы F(P, K, C), такой, что F(P, K, C) = 1 тогда и только тогда, когда C = E_K(P), где E_K – алгоритм зашифрования на ключе K. Могут применяться вспомогательные переменные, а также различные варианты оптимизации полученной формулы или ее разбиения на более простые подзадачи для увеличения вероятности нахождения решения.

3. Из выполнимости или невыполнимости формулы F(P, K, C) получается информация об исследуемом свойстве криптоалгоритма. Кроме того, получив выполняющий КНФ набор значений переменных, можно узнать неизвестные биты ключа.

Примеры успешного применения

Приведем некоторые из многих известных примеров успешно решенных криптоаналитических задач, относящихся к алгоритмам различных типов:

1. Первые версии алгоритма ACORN (алгоритм аутентифицированного шифрования с присоединенными данными, известен тем, что в 2019 г. был выбран в портфолио низкоресурсных алгоритмов европейского криптографического проекта CAESAR [13]) были успешно атакованы с помощью SAT-криптоанализа с различными целями атак: от извлечения внутреннего состояния и последующего нахождения секретного ключа по внутреннему состоянию и открытому тексту до подделки аутентифицируемого сообщения [8]. После публикации данных результатов автор алгоритма ACORN создал новую версию алгоритма [14], противостоящую описанным в работе [8] атакам; именно эта версия впоследствии вошла в портфолио проекта CAESAR.

2. С помощью SAT-криптоанализа были найдены коллизии для ряда известных полнораундовых алгоритмов хеширования:

   · для алгоритма хеширования MD4 [15];
   · для в недавнем прошлом стандарта хеширования SHA-1 [16].

3. Для алгоритма блочного шифрования MESH-64(8) с помощью SAT-криптоанализа в работе [7] было доказано отсутствие определенных классов слабых ключей.

Ограничения по применению

Основным фактором, ограничивающим применение SAT-криптоанализа, является быстрый рост количества элементов формулы в зависимости от числа кодируемых в формуле преобразований (в частности, от количества итераций блочного шифра), в результате которого формула становится нерешаемой современными алгоритмами.

SAT-криптоанализ наиболее эффективен для решения частных задач в контексте применения других видов криптоанализа [10, 12]. В качестве примеров таких задач можно привести следующие:

• ограничение ключевого множества для последующего поиска ключа шифрования методом перебора по ограниченному множеству [7];

• поиск невозможных дифференциалов для последующего применения дифференциального криптоанализа на основе невозможных дифференциалов [17];

• поиск дифференциальных путей для последующего нахождения коллизий хеш-функций [18].

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

Заключение

SAT-криптоанализ показал себя эффективным методом анализа криптографических алгоритмов. К настоящему моменту он был успешно применен для решения различных задач по криптоанализу алгоритмов хеширования и блочных/поточных шифров. Алгоритмы решения SAT-задач активно развиваются, можно ожидать в ближайшем будущем новых значительных результатов, полученных с помощью SAT-криптоанализа.