Dolev-Yao model

The Dolev-Yao model is a formal model proposed by Danny Dolev and Andrew Yao in which interactive protocols can be described. Such a model is required to make formal statements about such protocols. To make such statements easier, simplifying assumptions are made about the cryptological components of the protocol, the attacker, the network and its participants. The Dolev-Yao model is used in cryptology to prove the security of protocols .

The original Dolev-Yao model can be split into two parts, which can also be used independently. The Dolev-Yao attacker model is a classic attacker model, with the assumption that the attacker is an active participant in the network and that all messages in it are either sent by him or manipulated. It formalizes the attacker in the network by assigning him certain skills. The algebraic Dolev-Yao model formalizes the description of a protocol and replaces cryptographic procedures with elements of term algebras .

The environment

The network is represented by a number of abstract participants. These participants do not need any authorization and are connected to one another by channels through which messages can be sent in both directions. Other participants can join this network at any time and send and receive messages there. Since neither the technology on which the network is based, such as For example, if something is said about the type of participants in WLAN , this model is very general and can be applied to any network.

The attacker model

In the underlying environment model, it must be assumed that there are also hostile participants who not only passively listen to the messages sent, but also actively intervene in the network. The possibility that the attacker is on the way between two users, for example an Internet node that forwards the packets, must be taken into account. This enables him to change, re-address, duplicate, delete or add new messages. It also has options like IP spoofing . Such hostile participants are referred to as active attackers in the cryptology literature. There could be a single attacker or a group of attackers, which could include normal participants. Normally, all instances that do not behave in accordance with the protocol are combined to form an attacker. This implies that these parties share a channel outside the network through which they can exchange information.

In the Dolev-Yao model, the attacker is characterized by the following properties:

The attacker can intercept any message that is sent within the network.
The attacker is an authorized participant in the network and can therefore send messages to any participant.
The attacker can receive messages from any other participant.
The attacker can send his messages to other entities under a false identity.

The model can also be interpreted in such a way that each participant sends his message to the attacker, who then has the option of changing, deleting, duplicating or sending it to a recipient other than the intended recipient.

The algebraic model

Dolev and Yao model an asymmetric encryption function for a user as an abstract operator and the associated decryption function as . The only required properties are that the sequential execution of these functions is the identical mapping ( ) and that no information about can be inferred from. This representation idealizes concrete encryption. While an attacker in the real world always has bit sequences that he can manipulate, an attacker in the model only has one symbol with which he cannot do anything except to decrypt it if he knows the correct key. Nor does he have the option of guessing the key. All other cryptographic functions used are also represented in this way. This makes it possible to prove a protocol "per se" as secure without going into possible weaknesses of the cryptographic primitives, but also forces separate investigations into the extent to which a proof of security in the algebraic model can be transferred to a real protocol ( soundness ). Attacks against the idealized cryptographic primitives are not recorded in the model and therefore cannot be ruled out without further considerations. ${\ displaystyle X}$ ${\ displaystyle E_ {X}}$ ${\ displaystyle D_ {X}}$ ${\ displaystyle D_ {X} E_ {X} = E_ {X} D_ {X} = 1}$ ${\ displaystyle E_ {X} (M)}$ ${\ displaystyle M}$

example

The unauthenticated Diffie-Hellman key exchange is insecure in the Dolev-Yao model because a man-in-the-middle attack is possible in this model . The attacker can replace the messages sent by the participants with his own.

literature

Danny Dolev, Andrew Yao : On the security of public key protocols . In: IEEE trans. on Information Theory . IT-29, 1983, p. 198–208 ( cs.huji.ac.il [PDF; 1.8 MB ]).
Sergey Kovalev: Attack models for sensor networks . 2009 ( skovalev.de [PDF; 217 kB ] seminar paper).
Michael Backes, Birgit Pfitzmann, Michael Waidner : Soundness Limits of Dolev-Yao Models . In: Workshop on Formal and Computational Cryptography (FCC'06), affiliated with ICALP'06 . 2006 ( uni-saarland.de ).
Wenbo Mao: A structured operational modeling of the dolev-yao threat model . 2009 ( citeseerx.ist.psu.edu [PDF]).