← 2026

ProVerif is a piece of software that automatically reasons about the security properties of cryptographic protocols, as per its Wikipedia page. ProVerif has been used to analyze many of the protocols that underpin the modern internet, including TLS 1.3, Wireguard, Signal, electronic voting protocols, etc. Formal analysis of cryptographic protocols is this huge rabbit hole, and there is a crazy amount of different tools for doing so, all serving different purposes. But, ProVerif is my favorite. Here are some tips on how to use it well.

For context to this blog, check out the first few chapters of the excellent ProVerif manual. Yeah yeah being referred to a manual as a prelude to a blog post sucks, but it's a really good manual, and it's my blog! If you want something a bit lighter, Verifpal is like a miniature educational version of ProVerif.

Okay, now for some tips:

Phases

In ProVerif, users can arbitrarily silo protocols into different phases with the phase n syntax. Phases act as synchronization facilities that ensure every peer must stop together at phase n before proceeding to phase n+1. Placing phases right not only allows us to capture perfect forward secrecy and post-compromise security, but allows us to massively cut down on unnecessary intertwinings of operations between peers.

Signature Check, Mac Check, and AEAD Check Rules

A naive way to define the symbolic asymmetric signature relation in ProVerif is like this:

type skey.
type pkey. 
fun pk(skey): pkey.
fun sign(skey, bitstring): bitstring.

reduc forall m: bitstring, sk: skey; 
    checksign(sign(m,k), pk(k)) = m.

You'd think this is an acceptable way of setting things up, but it actually is super bad for the ProVerif reasoning engine. This is because the term reduction checksign here reduces to one of its arguments. This can lead to non-termination, and many headaches. At the time of writing, many examples on the ProVerif website suffer from this issue.

The correct strategy for defining reduction relations for things like checking signatures, checking MACs, and checking AEAD involves ensuring the output is strictly not a term of the input. For example checksign is best defined like this instead:

type skey.
type pkey. 

fun okay():bitstring.
fun pk(skey): pkey.
fun sign(skey, bitstring): bitstring.

reduc forall m: bitstring, sk: skey;
    checksign(pk(sk), m, sign(sk, m)) = okay.

Then in your model have something like:

[...]
if checksign(public_key, message, signature) = okay then
[... the rest of your protocol ...]

This approach was inspired by the approaches of SAPIC+ and A Tale of Two Worlds, a Formal Story of WireGuard Hybridization.

Using nounif To Tune Resolution

One of the best tricks to ensure your ProVerif models terminate is using the nounif resolution tuner to prevent ProVerif from infinitely processing recursive terms. In general, the biggest issue of ProVerif is its tendency to recursively resolve uninteresting terms. One consistent source of this issue is the equational theory for Diffie-Hellman:

type skey.
type pkey.
fun pk(skey): pkey.

fun dh(pkey, skey): key.
equation forall a: skey, b: skey; dh(pk(a), b) = dh(pk(b), a).

To manage term explosion here, you can bound the size of terms like this:

nounif x: pkey, y: skey; attacker(dh(x,y)) / 5000.
nounif z: skey; attacker(pk(z)) phase 1 / 5000.
nounif z: skey; attacker(pk(z)) phase 2 / 5000.
nounif z: skey; attacker(pk(z)) phase 3 / 5000.

In practice, this is highly successful, and is the primary reason why my complete models of Signal terminate at all. Highly, highly recommend.

Channels

One solid channel setup for ProVerif involves creating three channels: c, the primary channel peers use to communicate; p, a private channel to ensure the distribution of key material with secrecy, integrity, and authenticity; a, a channel dedicated to publishing material to the attacker.

Event Orderings

Events denoting sending a message should always be placed before the protocol actually sends a message, and similarly events denoting receiving a message should always be placed after the protocol receives a message. If you do not follow this setup, your authentication queries using these events will fail.

Minimizing Rules

It's paramount to minimize the number of functions, reduction rules, and equations defined in your ProVerif models.

Tagging

One way to ensure the termination of ProVerif for your models is to tag all the messages your protocol sends with immutable, unique names, e.g. free tag_1: bitstring. This way, two similarly structured messages on the same channel are not explored in parallel, and only the correct message is processed. Indeed, there is some theoretical work proving that tagged protocols always terminate. See section 6.7.2 in the ProVerif manual for more details.

Options

Some of the best options to set to improve the performance of ProVerif are:

One thing to note is that options are specified (by the manual) to never sacrifice completeness -- see the ProVerif manual, section 6.6.2.

Reachability Queries

A great way to sanity-check your models is to add reachability queries for events, e.g. query [terms]; event(MyEvent([terms]). During evaluation, ProVerif inverts these queries and evaluates whether or not all possible traces reach this term. That is, ProVerif checks whether not MyEvent([terms]) holds over all traces. Therefore, you're looking for this query to return false.


shz
← 2026