Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Содержание
Введение
Модель Долев–Яо, названная в честь её авторов Дэнни Долева и Эндрю Яо, — это формальная модель, используемая для доказательства свойств интерактивных криптографических протоколов.
The Dolev–Yao model, named after its authors Danny Dolev and Andrew Yao, is a formal model used to prove properties of interactive cryptographic protocols.
Сеть
Сеть представлена набором абстрактных машин, способных обмениваться сообщениями. Эти сообщения состоят из формальных термов. Эти термы раскрывают часть внутренней структуры сообщений, но некоторые их элементы, как ожидается, останутся скрытыми от злоумышленника.
The network is represented by a set of abstract machines that can exchange messages. These messages consist of formal terms. These terms reveal some of the internal structure of the messages, but some parts will hopefully remain opaque to the adversary.
Противник
Враг в этой модели может подслушивать, перехватывать и синтезировать любое сообщение и ограничен лишь ограничениями используемых криптографических методов. Иными словами: "нападающий владеет сообщением". Эту всемогущесть очень сложно смоделировать, и многие модели угроз упрощают её, как это было сделано для атакующего в области повсеместных вычислений.
The adversary in this model can overhear, intercept, and synthesize any message and is only limited by the constraints of the cryptographic methods used. In other words: "the attacker carries the message." This omnipotence has been very difficult to model, and many threat models simplify it, as has been done for the attacker in ubiquitous computing.
Алгебраическая модель
Криптографические примитивы моделируются абстрактными операторами. Например, асимметричное шифрование для пользователя представлено функцией шифрования и функцией дешифрования. Их основными свойствами являются то, что их композиция является функцией тождества и что зашифрованное сообщение не раскрывает никакой информации о исходном сообщении. В отличие от реального мира, противник не может манипулировать битовым представлением шифрования или угадать ключ. Однако злоумышленник может повторно использовать любые сообщения, которые были отправлены и, следовательно, стали известны. Злоумышленник может шифровать или дешифровать эти сообщения любыми известными ему ключами, чтобы подделать последующие сообщения. Протокол моделируется как набор последовательных прогонов, чередующихся между запросами (отправкой сообщения по сети) и ответами (получением сообщения из сети).
Cryptographic primitives are modeled by abstract operators. For example, asymmetric encryption for a user is represented by the encryption function and the decryption function Their main properties are that their composition is the identity function and that an encrypted message reveals nothing about Unlike in the real world, the adversary can neither manipulate the encryption's bit representation nor guess the key. The attacker may, however, re use any messages that have been sent and therefore become known. The attacker can encrypt or decrypt these with any keys he knows, to forge subsequent messages. A protocol is modeled as a set of sequential runs, alternating between queries (sending a message over the network) and responses (obtaining a message from the network).
Замечание
Символический характер модели Долева-Яо делает её более удобной для анализа, чем вычислительные модели, и позволяет применять алгебраические методы, но может быть менее реалистичной. Тем не менее, оба типа моделей для криптографических протоколов взаимосвязаны. Кроме того, символические модели особенно хорошо подходят для демонстрации уязвимости протокола, а не его безопасности, при заданных предположениях о возможностях злоумышленников.
The symbolic nature of the Dolev–Yao model makes it more manageable than computational models and accessible to algebraic methods but potentially less realistic. However, both kinds of models for cryptographic protocols have been related. Also, symbolic models are very well suited to show that a protocol is broken, rather than secure, under the given assumptions about the attackers capabilities.