ProVerif: Automated Protocol Verification
Specify and verify TLS handshake properties with ProVerif.
ProVerif: Automated Protocol Verification is a free Cryptology Academy lesson on CoddyKit — lesson 3 of 4. You can read the complete lesson below for free — then practise it hands-on in the browser with a built-in code editor and a 24/7 AI tutor. It is part of the Cryptology Academy learning path, one of 4 lessons in the course, and your progress syncs across the web and the CoddyKit app.
What Is ProVerif?
ProVerif (Bruno Blanchet, 2001) is an automated cryptographic protocol verifier. It takes a protocol described in applied pi calculus and automatically decides secrecy and authentication properties.
How ProVerif Works
ProVerif translates the protocol into Horn clauses and applies a resolution-based algorithm to derive what the attacker can learn. If a secrecy fact is derivable, the protocol is broken; otherwise, it is proved secure.
ProVerif Input Language
Protocols are described declaratively: declare channels, types, functions (enc, dec, sign, verify), equations (dec(enc(m,k),k)=m), and processes communicating over channels.
Declaring Cryptographic Primitives
Example ProVerif declarations:
(* Symmetric encryption *)
fun senc(bitstring, key): bitstring.
fun sdec(bitstring, key): bitstring.
equation forall m: bitstring, k: key; sdec(senc(m, k), k) = m.
(* Asymmetric encryption *)
fun pk(skey): pkey.
fun aenc(bitstring, pkey): bitstring.
fun adec(bitstring, skey): bitstring.
equation forall m: bitstring, sk: skey; adec(aenc(m, pk(sk)), sk) = m.Writing a Simple Protocol Process
Model Alice and Bob as parallel processes:
(* Alice sends nonce to Bob, encrypted *)
let Alice(skA: skey, pkB: pkey) =
new na: nonce;
out(c, aenc((na, pk(skA)), pkB));
in(c, m: bitstring);
let nb = adec(m, skA) in
out(c, aenc(nb, pkB)).
(* Main process: run attacker with full channel control *)
process
new skA: skey; new skB: skey;
out(c, pk(skA)); out(c, pk(skB)); (* publish public keys *)
(Alice(skA, pk(skB)) | Bob(skB, pk(skA)))Stating Security Queries
ProVerif checks queries like:
(* Secrecy: attacker cannot learn na *)
query attacker(na).
(* Authentication: if Bob completes, Alice started *)
query event(BobFinished(nb)) ==> event(AliceStarted(nb)).Interpreting ProVerif Output
ProVerif outputs "RESULT ... is true" (proved secure) or "RESULT ... is false" and prints a counterexample attack trace showing the attacker's messages. The trace shows exactly how the attack works.
Verifying TLS 1.3 with ProVerif
Bhargavan et al. (2016) used ProVerif to analyse a model of TLS 1.3. They found and reported an attack on the 0-RTT resumption mechanism, which was fixed before the RFC was finalised.
Limitations: Approximation and Loops
ProVerif overapproximates: it may report false attacks (say "false" when the protocol is actually secure) but never misses real attacks. Unbounded protocol sessions may not terminate — ProVerif unrolls loops heuristically.
When ProVerif Says "Cannot Be Proved"
If ProVerif cannot determine the result within its approximation, it outputs "CANNOT BE PROVED." This is not a proof of insecurity — it means the tool ran out of its heuristic power. Tamarin may succeed in these cases.
Knowledge Check
What does a ProVerif output of "RESULT ... is false" mean for a secrecy query?
Lesson Recap
ProVerif automates protocol verification using Horn-clause resolution. Protocols are written in applied pi calculus with cryptographic equations. Queries ask about secrecy and authentication. False means proved secure; true means broken (with attack trace). Limitations: approximations may give "cannot be proved."
Frequently asked questions
Is the “ProVerif: Automated Protocol Verification” lesson free?
Yes — the full text of “ProVerif: Automated Protocol Verification” is free to read here on the web, and the Cryptology Academy course includes 4 lessons in total. To practise it interactively (a built-in code editor and a 24/7 AI tutor) and unlock the rest of the Cryptology Academy course, upgrade to CoddyKit PRO.
What will I learn in “ProVerif: Automated Protocol Verification”?
Specify and verify TLS handshake properties with ProVerif. You practise Cryptology Academy with hands-on code you run directly in the browser, and a 24/7 AI tutor answers your questions as you work through the lesson.
Do I need any experience to start Cryptology Academy?
No prior experience is required. Cryptology Academy on CoddyKit is structured for beginners through advanced learners; this is — lesson 3 of 4, so you can start here or from the beginning and move at your own pace.
How long does the “ProVerif: Automated Protocol Verification” lesson take?
Most CoddyKit lessons take about 5–10 minutes. Each one is bite-sized and interactive, so you make steady progress and pick up exactly where you left off across the web and the app.
Can I write and run code in this Cryptology Academy lesson?
Yes. Every Cryptology Academy lesson includes a built-in code editor, so you write and run real code right in your browser and get instant AI feedback — no local setup required.
All lessons in this course
- Why Informal Proofs Are Not Enough
- Dolev-Yao Attacker Model & Symbolic Crypto
- ProVerif: Automated Protocol Verification
- Tamarin & Computational Proofs