This blog post is based on a talk I recently gave on verifying cryptographic protocols using ProVerif, and the original slide deck can be found here.1
Motivation
Consider a scenario where Alice wants to send a message to Bob across a network. Though Alice can send a message into the network and Bob can receive it, the network itself is under neither's control. A malicious attacker, Eve, could read Alice's message, modify it before it reaches Bob, or even inject her own messages.
Such a threat model forms the basis for the Dolev-Yao Model. We have honest actors like Alice and Bob, who want to have a conversation, and an active attacker, like Eve, who controls the network entirely, but does not have compute to break encryption. So how do Alice and Bob talk securely?
What is a Cryptographic Protocol?
First, we need to establish a protocol between Alice and Bob. This is any set of rules about how our entities communicate. For example, Alice might initiate all conversations with "Hello", or Bob may acknowledge every message with "Okay". A protocol defines expected behaviour, but it still does not prevent an attacker from interfering.
For secure communication, we also need to encrypt our messages, so that Eve cannot read them, but Alice and Bob can. Luckily, cryptography provides various methods to encrypt and decrypt any string. Using these within our protocol gives us a cryptographic protocol, intended to achieve security goals like confidentiality or authentication.
We cannot simply test our cryptographic protocol using trial and error, since any vulnerability could be catastrophic. This is where we can use formal verification.
What is Formal Verification?
Formal verification is the act of proving or disproving the correctness of a system with respect to some specification, using formal methods of mathematics. A formal verification tool works by abstracting the system into a mathematical model and reasoning about its possible behaviours to check whether the specification holds.
Formal verification is used across the tech industry. Hardware companies such as Intel and AMD use it heavily to verify chip designs and avoid hardware level bugs. It is also used in distributed systems to exhaustively check design correctness, ensuring reliability, fault tolerance, and consistency across networked components.2
To ensure our cryptographic functions cannot be broken, we can use automated theorem provers like Rocq3 or Lean4. These tools can be used to model cryptographic algorithms mathematically and verify them.
However, having secure encryption doesn't mean our cryptographic protocol is secure. Even assuming perfect cryptography, we could have vulnerabilities in our protocol logic, leading to weaknesses such as man-in-the-middle or replay attacks.
How do we verify a protocol?
We have two approaches to verify against such attacks. One is the computational model, where we assume an adversary with finite compute that manipulates bitstrings. Security is defined in terms of the probability that an attacker can break some security goal, (for example, guessing a password). Tools which do this include EasyCrypt5 and CryptoVerif6.
Although this is more realistic, it is also complex to model. It requires more manual effort by programmers to model the protocol accurately without human errors.
In contrast, we have the symbolic model, which uses the Dolev-Yao model. The attacker has full control over the network, but cannot break encryption without knowing the exact key. This is much simpler to model and is more scalable.
One might wonder if the symbolic model abstracts too much, i.e., if it's worth disregarding vulnerabilities exploiting cryptography. However, while this is less realistic, it is still valuable, since it's easier to model larger and more complex protocols like TLS. It's not just theoretical either. In 2021, researchers were able to find vulnerabilities in the EMV protocol for credit cards using the symbolic model.7
What's ProVerif?
ProVerif is one such cryptographic protocol verifier which uses the symbolic model. It allows us to model a protocol, assuming perfect cryptography, and search for possible attacks.
ProVerif can be run on the demo website8, or downloaded as an executable and run from command line.
Let's try and create a secure protocol from scratch using ProVerif. All of the code below is hosted on GitHub.9
Protocol #0: Symmetric encryption
For our first ProVerif example, let's consider the simplest form of encryption, symmetric encryption.
We have two functions:
senc(m, k) = c
sdec(c, k) = m
We have a single key, k, to encrypt and decrypt our message. In other words, we have the following property
sdec( senc(m,k) , k) = m
For simplicity, we assume that Alice and Bob already agree upon a shared key, perhaps from some past interaction.
1. Alice -> Bob: senc(secretA, key)
[Bob decrypts using key to get secretA]
2. Bob -> Alice: senc(secretB, key)
[Alice decrypts using key to get secretB]
Alice sends her secretA, encrypted with the shared key, to Bob. Bob decrypts this using the key, and retrieves the message. Similarly, Bob sends his secret to Alice.
Let's look at how to model this in ProVerif. We would like to verify that secretA and secretB are confidential.
(* Communication channel *)
free c : channel.
(* Types *)
type key.
(* Symmetric encryption *)
fun senc(bitstring, key) : bitstring.
reduc forall m:bitstring, k:key; sdec(senc(m, k), k) = m.
(* Secrets *)
free secretA, secretB: bitstring [private].
free k: key [private].
query attacker(secretA).
query attacker(secretB).
let A(k : key) =
out(c, senc(secretA, k));
in(c, x: bitstring);
let secretB_recv = sdec(x, k) in
0.
let B (k: key)=
in(c, x: bitstring);
let secretA_recv = sdec(x, k) in
out(c, senc(secretB, k)).
(* Main process *)
process
( !A(k) | !B(k) )
All communication here happens through the channel c. This is a public channel controlled by Eve, and she can read all messages sent here and inject her own.
For symmetric encryption, we make a new type called key, which is used in our encryption and decryption functions.
query attacker(secretA). is used to check if our attacker, Eve, can somehow find secretA, the message Alice sends to Bob.
We can run this using ProVerif, and we see that our secret is safe from Eve.
$ proverif 0_shared_key.pv
Verification summary:
Query not attacker(secretA[]) is true.
Query not attacker(secretB[]) is true.
Protocol #1: Known Public Keys
In the previous protocol, we assumed only Alice and Bob would have the shared key. However, this is difficult to realise in practice. Instead, we use asymmetric encryption.
We have two keys, our private/secret key sk, and our public key pk.
The public key can be derived from the private key, but the private key cannot be reversed from the public key.
pub(sk) = pk
For encryption, we use the other party's public key and send it to them. They can then use their own private key to decrypt the message.
aenc(m, pk) = c
adec(c, sk) = m
For now, let's assume that Alice and Bob have already shared their public keys with each other in some past interaction. Note that these public keys can still be exposed to the network, since Eve cannot use them to decrypt messages.
1. Alice -> Bob: aenc(secretA, pkB)
[Bob decrypts using skB to get secretA]
2. Bob -> Alice: aenc(secretB, pkA)
[Alice decrypts using skA to get secretB]
Our ProVerif processes now look like this
let A(pkB: pub_key, skA: priv_key) =
out(c, aenc(secretA, pkB));
in(c, x: bitstring);
let secretB_recv = adec(x, skA) in
0.
let B(pkA: pub_key, skB: priv_key)=
in(c, x: bitstring);
let secretA_recv = adec(x, skB) in
out(c, aenc(secretB, pkA)).
(* Main process *)
process
new skA: priv_key; let pkA = pub(skA) in out(c, pkA);
new skB: priv_key; let pkB = pub(skB) in out(c, pkB);
( !A(pkB, skA) | !B(pkA, skB) )
Running this in ProVerif, we can confirm that our secrets are still confidential.
$ proverif 1_asym_enc_known_pubkey.pv
Verification summary:
Query not attacker(secretA[]) is true.
Query not attacker(secretB[]) is true.
Protocol #2: Share public keys over network
In our previous protocol, we assumed Alice and Bob had already shared their public keys. In practice, however, this is a huge challenge. We need a better way to distribute Alice's and Bob's public keys.
Since our public keys are already shared on the network, what happens if Alice tries to get Bob's public key from the network? This would mean we wouldn't need to assume that these keys are already shared.
Our protocol would now look something like this
1. Network -> Alice: pkB
2. Alice -> Bob: aenc(secretA, pkB)
[Bob decrypts using skB to get secretA]
3. Bob -> Alice: aenc(secretB, pkA)
[Alice decrypts using skA to get secretB]
We can model this similarly in ProVerif, but on verifying it, we see this!
$ proverif 2_asym_enc_over_network.pv
Verification summary:
Query not attacker(secretA[]) is false.
Query not attacker(secretB[]) is false.
Eve can somehow find both secretA and secretB! How does this happen??
Fortunately, ProVerif also gives us a trace describing exactly this.
Let's go through the trace for Eve decrypting secretA.
-- Query not attacker(secretA[]) in process 1.
Translating the process into Horn clauses...
Completing...
Starting query not attacker(secretA[])
goal reachable: attacker(secretA[])
Derivation:
1. The attacker has some term k.
attacker(k).
2. By 1, the attacker may know k.
Using the function pub the attacker may obtain pub(k).
attacker(pub(k)).
3. The message pub(k) that the attacker may have by 2 may be received at input {9}.
So the message (aenc(secretA[],pub(k)),pub(skA[])) may be sent to the attacker at output {10}.
attacker((aenc(secretA[],pub(k)),pub(skA[]))).
4. By 3, the attacker may know (aenc(secretA[],pub(k)),pub(skA[])).
Using the function 1-proj-2-tuple the attacker may obtain aenc(secretA[],pub(k)).
attacker(aenc(secretA[],pub(k))).
5. By 4, the attacker may know aenc(secretA[],pub(k)).
By 1, the attacker may know k.
Using the function adec the attacker may obtain secretA[].
attacker(secretA[]).
6. By 5, attacker(secretA[]).
The goal is reached, represented in the following fact:
attacker(secretA[]).
Eve creates her own private key k and derives her public key pub(k). She sends this to Alice, who believes this to be Bob's public key. She encrypts her secret using Eve's public key and sends it over the network, where Eve can decrypt it!
Similarly Eve can find secretB using her own keys. I will leave the analysis of this to the reader and I encourage trying the example yourself in ProVerif!
This is a classic Man-in-the-Middle attack. Note that this is not a flaw in our encryption algorithm, instead, Eve was able to exploit the lack of authentication.
Protocol #3: Public key with auth
The problem here was that Alice and Bob couldn't trust anything on the network. They need some way to know that each message is authentic and hasn't been tampered with by Eve.
To solve this, we can use digital signatures. Like in asymmetric encryption, we have a public and private key. We will call these spk and ssk.
pub(ssk) = spk
Any message can be signed using the private key before being sent.
sign(m, ssk) = ms
A signed message can still be read, i.e., there is no encryption here. Additionally, we can verify the signature using the corresponding public key. Since the private signing key cannot be derived from the public key, we know that the message must be from the intended sender, since only they have the private signing key.
getmesg(ms) = m
checksign(ms, spk) = m
Also note that we must still assume that Alice and Bob share their public signing keys. In practice, trusted public signing keys are embedded in the OS or browser itself. With multiple people, we store the public signing keys for a trusted certification authority (CA) instead of Alice or Bob directly.10 However, this is beyond our scope, and we won't be modelling this.
Let's look at our protocol now.
1. Network -> Alice: pkB
2. Alice -> Bob: sign( aenc( (pkA, K), pkB) , sskA)
[Bob verifies Alice's message using spkA]
[Bob decrypts using skB to get pkA, K]
3. Bob -> Alice: sign( aenc(K, pkA), sskB)
[Alice verifies Bob's message using spkB]
[Alice decrypts using skA to get K]
4. Alice -> Bob: senc(secretA, K)
[Bob decrypts using K to get secretA]
5. Bob -> Alice: senc(secretB, K)
[Alice decrypts using K to get secretB]
You might notice that we've gone back to using symmetric encryption here. This is because in practice, asymmetric encryption takes more time and power to compute, and is usually not used for every message. Instead, we use asymmetric encryption to create a shared key and then use symmetric encryption with that key.
We can model this in ProVerif and confirm that it works!
$ proverif 3_asym_enc_with_auth.pv
Verification summary:
Query not attacker(secretA[]) is true.
Query not attacker(secretB[]) is true.
Conclusion
We have seen how vulnerabilities in cryptographic systems can arise from bad protocol design. Formal verification tools like ProVerif can be used to analyse such protocols to find attacks and verify security properties.
However, these guarantees only apply to the abstract model being analysed. Formal methods like this do not address implementation bugs or computational weaknesses, and must be complemented with other techniques in practice.
Additionally, we have barely scratched the surface of cryptographic protocols. Real-world protocols such as Signal or TLS are a lot more complex, as they aim to provide stronger guarantees like authentication, freshness, and resilience across many sessions.