Модель Долева – Яо


Модель Долева-Яо [ 1] , названная в честь ее авторов Дэнни Долева и Эндрю Яо , представляет собой формальную модель, используемую для доказательства свойств интерактивных криптографических протоколов. [2] [3]

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

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

Это всемогущество было очень сложно смоделировать, и многие модели угроз упрощают его, как это было сделано для злоумышленника в вездесущих вычислениях . [4]

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

Протокол моделируется как набор последовательных запусков, чередующихся между запросами (отправка сообщения по сети) и ответами (получение сообщения из сети).