ProVerif: Automated Protocol Verification
Specify and verify TLS handshake properties with ProVerif.
ProVerif: Automated Protocol Verification is a free Cryptology Academy lesson on CoddyKit. This is 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, and your progress syncs across the web and the CoddyKit app. The Cryptology Academy course includes 4 lessons in total.
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."
Learn Cryptology Academy with an AI tutor — free
Write and run real code in your browser, get instant help from a 24/7 AI tutor, and pick up where you left off on the web or in the app.
- Courses
- 67
- Lessons
- 261
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. 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. The Cryptology Academy course includes 4 lessons in total.
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, so you can start here or from the beginning and move at your own pace. This is lesson 3 of 4.
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