The Dolev-Yao vs. Computational Model

Automatic provers of cryptographic protocols operate either in the symbolic (Dolev-Yao) model, or in the computational model. Reasoning in the symbolic model ist easier, and the proofs are accessible to non-experts. But they fail to model the real crypto world in all its gory details. Reasoning in the computational model is much more difficult, and the proofs are best read and understood by expert cryptanalysts. But the reward is, that they catch errors that won't show up in the symbolic model. In this crypto bite, we'll briefly explore both models, and mention tools that operate in each of them.

The Symbolic (Dolev-Yao) Model

In the symbolic Dolev-Yao model[DY83], we treat cryptographic primitives as black boxes. They are perfect, in the sense that no adversary can break them at all. We don't care how they are implemented, and what algorithm they represent. All that matters is how they interact with other black boxes and with the users (protocols).

For example, consider symmetric encryption. Every symmetric encryption scheme defines, among others, a probabilistic encryption and a deterministic decryption algorithm:

  • senc(m, k): encrypt plaintext message m with key k
  • sdec(m, k): decrypt ciphertext message m with key k

Let's ignore for a moment the additional constraint that the key k must have been generated by a legitimate key generation algorithm. This, we'll always assume.

What is the main gist of symmetric encryption? This is that if we encrypt a message with some key, then we can decrypt the ciphertext using the same key. This is the correctness property of symmetric encryption. We can express this property with the equation:

\[ \forall m \in \mathcal M, \forall k \in \mathcal K \colon \operatorname{sdec}(\operatorname{senc}(m, k), k) = m \]

Here, \(\mathcal M\) is the set of all (plaintext) messages, and \(\mathcal K\) is the set of all keys generated by a key generation algorithm for the symmetric encryption scheme.

The equation sdec(senc(m,k),k) = m is all it takes to capture the essence of symmetric encryption and decryption.

We stress that it senc() and sdec() can be e.g. DES, 3DES, AES, Salsa20, Trivium, and a myriad of other symmetric block and stream ciphers. As far as reasoning in the symbolic model goes, it doesn't matter.

The Dolev-Yao Adversary

The point here is that if an adversary in the Dolev-Yao model has only access to the message senc(m,k), she has no chance in hell to recover anything about m or k. Neither can she recover all of m or k, nor can she recover f(m) or g(k), where f(m) extracts some information out of m and g(k) extracts some information out of k (e.g. the most significant bit). That's why we say that the cryptographic primitives are perfect: they can't be broken, and they have no hidden vulnerabilities.

Moreover, the adversary can't even break these cryptographic primitives with negligible probability. In the computational model, she could, but not here in the symbolic model.

Still, a Dolev-Yao adversary is powerful: she has essentially full reign over the network. Therefore, she can read, write, modify, drop, insert messages in transit. This means, among others, that she can mount man in the middle attacks.

She can also perform all kinds of analyses like a CPA (chosen plaintext attack), CCA (chosen ciphertext attack) and so on, depending on the protocol under attack.

It is also useful to think of a Dolev-Yao adversary as being computationally unbounded, but since we don't care about breaking cryptographic algorithms with negligible probability, this is a seldom used property.

Reasoning in the Dolev-Yao Model

It is (relatively) easy to reason in the symbolic model. Assuming that all cryptographic primitives are black boxes defined by their equations, reasoning in the Dolev-Yao model morphs into a syntactic exercise in symbolic manipulations, using a set of rules.

If you took a class in Mathematical Logic, you'll recall inference rules. Reasoning in the symbolic model is essentially applying inference rules to a set of terms (facts), until we either reach the desired conclusion (typically a security property that we want to prove), or we find a counter-example (which we could immediatly translate into a successful attack).

(... to add: logic solvers)

In other words, we could write symbolic provers that could prove or disprove some desired properties in languages like PROLOG, where the facts of the protocol are represented by PROLOG terms, and the inference rules translate directly into PROLOG rules. But nobody does this, because the underlying engine used by PROLOG isn't up to the task.

Provers in the Symbolic Model

At the time of writing, there are two popular cryptographic provers in the symbolic model:

We'll cover them in detail in separate crypto bites.

The Computational Model

(... to be written)

The Adversary in the Computational Model

(... to be written)

Reasoning in the Computational Model

(... to be written)

The Sequence of Games Technique

(... to be written)

[BR04, BP06, Shoup06, BR08, Blanchet11]

Provers in the Computational Model

Currently, there are two popular cryptographic provers in the computational model:

We'll cover them in separate crypto bites.

Sources

(... more links to the literature to be added)