The Dolev–Yao model,[1] named after its authors Danny Dolev and Andrew Yao, is a formal model used to prove properties of interactive cryptographic protocols.
[2][3] The network is represented by a set of abstract machines that can exchange messages.
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.
Unlike in the real world, the adversary can neither manipulate the encryption's bit representation nor guess the key.
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).
[5] 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.