Dolev-Yao Attacker Model & Symbolic Crypto

Proposed by Danny Dolev and Andrew Yao in 1983, the Dolev-Yao model is the standard adversary model for symbolic protocol analysis. The attacker controls the entire network.

The Dolev-Yao attacker can: intercept any message, store messages, replay old messages, forge new messages from known components, but cannot break the underlying crypto primitives.

In symbolic models, encryption is a perfect black box: the attacker cannot decrypt without the key, cannot factor large numbers, and cannot forge signatures. This simplifies analysis but may miss implementation-level attacks.

Messages are modelled as terms: enc(k, m), sig(sk, m), hash(m), pair(a, b). The attacker knows certain terms and derives new ones using defined rules (deduction rules).

The attacker's knowledge is closed under deduction: if they know enc(k,m) and k, they can derive m. If they know pair(a,b), they can derive a and b. The closure of initial knowledge = everything the attacker can learn.

Protocol security is stated as: "the attacker's knowledge never contains the secret s in any reachable state." Secrecy = reachability. Authentication = absence of certain bad trace patterns.

Two-party protocol: A→B: {Na, A}_{K_B}; B→A: {Na, Nb}_{K_A}; A→B: {Nb}_{K_B}. In term algebra: Alice sends enc(pubkey_B, pair(Na, A)). We verify that after execution, only B knows Na.

The applied pi calculus (Abadi & Fournet 2001) is a process algebra for modelling protocols. Processes communicate over channels; the attacker controls public channels. ProVerif and Tamarin use this formalism.

A protocol that is secure in the Dolev-Yao model may still be computationally insecure if the cryptographic instantiation is weak. The Computational Soundness theorem (Cortier et al.) bridges the gap for specific primitive classes.

Dolev-Yao cannot model: algebraic properties (e.g., XOR commutativity), side-channel attacks, implementation bugs, or probabilistic failures. Extensions like the equational theory model handle some algebraic properties.

Which capability does the Dolev-Yao attacker NOT have?

Dolev-Yao gives the attacker full network control but assumes perfect crypto. Messages are terms in an algebra; security is a reachability property. Applied pi calculus provides the formal language. Limitations: cannot model algebraic relations, side channels, or implementation bugs.