The Dolev–Yao model is a formal model used to prove properties of interactive cryptographic protocols.
Contents
The network
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
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, for example, the attacker in ubiquitous computing.
The algebraic model
Cryptographic primitives are modeled by abstract operators. For example, asymmetric encryption for a user
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).
Remark
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.