Dolev–Yao model

The Dolev - Yao model is a proposed Danny Dolev and Andrew Yao formal model in which interactive protocols can be described. Such a model is required to make a formal statements of such protocols. In order to facilitate the meeting of such statements, simplifying assumptions about the cryptographic components of the protocol, the attacker, the network and its participants are taken. Dolev - Yao is applied the model in cryptology in order to prove the security of protocols.

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

Area

The network is represented by a set of abstract participants. These participants do not need authorization and are connected by channels with each other, can be sent via which messages in both directions. Each time additional participants can join this network and there send and receive messages. Since neither of the the underlying network technology such as Wi-Fi is still predicated on the type of participants something, this model is very general and can be applied to any network.

The attacker model

In the underlying environment model, one must assume that there are also hostile participants who not only listen to the messages sent passively but also actively involved in the network. The possibility must be included that the attacker is on the way between two users, so for example, is an Internet node, which forwards the packets. This allows him to change messages to readdress, duplicate, delete or add. It also has options such as IP spoofing. Such hostile participants are referred to in cryptology literature as an active attacker. There may be a single or a group of attackers also give the normal participants may include. Normally, all instances that do not behave according to the protocol, combined to an attacker. This implies that these parties a channel outside the network share over 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 internally in the network.
• The attacker is an authorized subscriber of the network and can send messages to each participant.
• The attacker has the possibility of any other participant to receive messages.
• The attacker can send its messages to other instances under a false identity.

In summary, the model also think of so that each participant sends its message to the attacker, who then has the opportunity to change it, delete, duplicate, or send it to anyone 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 corresponding decryption function as. The only required properties are that the sequential execution of these functions, the identity mapping is (), and that can be inferred from any information on. This representation idealized concrete encryptions. While an attacker in the real world always has the bit strings he can manipulate, an attacker in the model has only one symbol with which he can not do anything, unless to decipher if he knows the correct key. He does not have the opportunity to guess the key. All the other used cryptographic functions are represented in this way. This was to prove a log "in itself" as safe allowed without addressing any weaknesses in the cryptographic primitives, but also enforces a separate investigation, the extent to which a security proof in the algebraic model is transferable to a real protocol ( Soundness ). Attacks against the idealized cryptographic primitives are not captured in the model and so therefore can not be excluded without further considerations.

Example

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