Модель атакующего Долева—Яо и символьная криптография

Предложенная Danny Dolev и Andrew Yao в 1983 году, модель Dolev-Yao является стандартной моделью противника для символьного анализа протоколов. Злоумышленник контролирует всю сеть.

Злоумышленник в модели Dolev-Yao может: перехватывать любое сообщение, хранить сообщения, повторно воспроизводить старые сообщения, подделывать новые сообщения из известных компонентов, но не может взломать базовые криптографические примитивы.

В символических моделях шифрование представляет собой идеальный чёрный ящик: злоумышленник не может расшифровать данные без ключа, разложить большие числа на множители или подделать подписи. Это упрощает анализ, но может не учитывать атаки на уровне реализации.

Сообщения моделируются как термы: enc(k, m), sig(sk, m), hash(m), pair(a, b). Злоумышленнику известны определённые термы, и он выводит новые, используя заданные правила (правила дедукции).

Знания злоумышленника замкнуты относительно дедукции: если ему известны enc(k,m) и k, он может вывести m. Если ему известен pair(a,b), он может вывести a и b. Замыкание исходных знаний = всё, что может узнать злоумышленник.

Безопасность протокола формулируется так: «знания злоумышленника никогда не содержат секрет s ни в одном достижимом состоянии». Секретность = достижимость. Аутентификация = отсутствие определённых нежелательных шаблонов трасс.

Протокол для двух участников: A→B: {Na, A}_{K_B}; B→A: {Na, Nb}_{K_A}; A→B: {Nb}_{K_B}. В алгебре термов: Alice отправляет enc(pubkey_B, pair(Na, A)). Мы проверяем, что после выполнения протокола только B знает Na.

Прикладное π-исчисление (Abadi и Fournet, 2001) — это алгебра процессов для моделирования протоколов. Процессы обмениваются данными по каналам; злоумышленник контролирует общедоступные каналы. ProVerif и Tamarin используют этот формализм.

Протокол, безопасный в модели Долев—Яо, всё ещё может быть вычислительно небезопасным, если криптографическая реализация слаба. Теорема о вычислительной состоятельности (Cortier и др.) устраняет этот разрыв для определённых классов примитивов.

Модель Долев—Яо не может описывать алгебраические свойства (например, коммутативность XOR), атаки по побочным каналам, ошибки реализации или вероятностные сбои. Расширения, например модель эквациональной теории, учитывают некоторые алгебраические свойства.

Модель Долев—Яо предоставляет злоумышленнику полный контроль над сетью, но предполагает идеальную криптографию. Сообщения являются термами алгебры, а безопасность — свойством достижимости. Прикладное π-исчисление предоставляет формальный язык. Ограничения: модель не может описывать алгебраические связи, атаки по побочным каналам или ошибки реализации.