That gap between looking right and being right is why protocol designers now reach for automated proof tools. When a specification says a handshake has been analysed in Tamarin, or a paper claims a ProVerif model of a messaging protocol found no attacks, something real has been established. It is worth knowing exactly what.
The short version: these tools prove that a mathematical description of your protocol resists a mathematical description of an attacker. Both descriptions are yours to write. The proof is only as good as the descriptions, and it says nothing at all about the code you ship.
Two different models, two different guarantees
Protocol analysis splits into two families, and conflating them is the most common misreading of a verification claim.
The symbolic model, often called the Dolev-Yao model after the 1983 paper that formalised it, treats cryptography as perfect and abstract. Encryption is a black box: without the key, a ciphertext is an opaque term that reveals nothing. A hash cannot be inverted, ever, by anyone. The attacker controls the network completely, can read, drop, reorder, and forge any message, and can run any number of protocol sessions in parallel, but cannot break a primitive. Tamarin and ProVerif work here.
The computational model treats cryptography as it actually behaves: keys are bitstrings, the attacker is a probabilistic algorithm with bounded running time, and security means the attacker's advantage over guessing is negligible. This is where the reduction proofs in cryptography papers live. CryptoVerif and EasyCrypt automate parts of it.
The symbolic model is far easier to automate and can search enormous state spaces without human help. It also cannot see any attack that depends on a primitive being imperfect. A protocol that is symbolically secure can still fall to a padding oracle, a length-extension trick, or a nonce collision, because in the symbolic world those things do not exist.
Symbolic proof: "assuming your crypto is flawless, the message flow has no logical flaw." Computational proof: "assuming this specific hardness assumption holds, an attacker with bounded resources gains negligible advantage." Neither says the implementation is correct.
What Tamarin and ProVerif do
You write a model. In ProVerif that means describing the protocol in a variant of the applied pi calculus: processes that send and receive on channels, apply functions, and branch. In Tamarin it means multiset rewriting rules that describe how the system's state evolves. In both, you also declare an equational theory that tells the tool what your primitives do, including relationships like Diffie-Hellman's property that raising a public value to a private exponent commutes.
Then you write the properties you want. These are not vague goals but precise logical statements: if a responder finishes a session believing it is talking to A, then A really did start a matching session. Or: a session key learned by the attacker after a compromise cannot decrypt messages sent before it, which is how you state forward secrecy formally.
The tool then either proves the property holds over unboundedly many parallel sessions, or produces a trace showing how an attacker breaks it. That trace is the valuable output. It is a concrete attack script, not a warning, and it is why these tools find real problems in real specifications.
Where this has changed real protocols
TLS 1.3 is the clearest case. Rather than standardising first and analysing later, the IETF working group ran formal analysis alongside drafting. A symbolic Tamarin analysis by Cremers, Horvat, Hoyland, Scott and van der Merwe modelled the handshake including pre-shared keys, resumption and 0-RTT, and found a flaw in the interaction between client authentication and session resumption in an intermediate draft. It was fixed before publication. Separate computational analyses covered the same ground with different assumptions. The result is a protocol whose reduction in complexity from TLS 1.2 was driven partly by what the analysts could not prove about the older design.
The Signal protocol received a detailed computational security proof from Cohn-Gordon, Cremers, Dowling, Garratt and Stebila in 2017, several years after deployment. It confirmed the core design, including the double ratchet, provided the properties it claimed. WireGuard's handshake has a Tamarin proof from Donenfeld and Milner. TreeKEM, the group key agreement inside MLS (RFC 9420), went through multiple published analyses during standardisation, and several of them changed the design.
There is a pattern in that history. Analysis run against a finished, deployed protocol mostly comes back with confirmation. Analysis run during drafting has changed the drafts, repeatedly, which is an argument for the timing more than for the tooling.
The four places the guarantee stops
| Gap | What it means in practice |
|---|---|
| The model is not the protocol | Someone hand-wrote an abstraction of the specification. If they omitted a message field, simplified a state machine, or modelled two related sub-protocols separately, the proof covers the abstraction and not the thing itself. |
| The properties are not all the properties | The tool proves what you asked. If nobody wrote down a query for post-compromise security or for identity misbinding, no result covers them. A proof with three lemmas is a proof about three lemmas. |
| The attacker model excludes real attackers | Dolev-Yao attackers do not measure timing, watch power draw, or read memory across a CPU boundary. Side channels live entirely outside the model, which is why constant-time implementation is a separate discipline. |
| The code is not the model | Heartbleed was a missing bounds check. Apple's goto fail was a duplicated line that skipped signature verification. Neither protocol had a design flaw. Both were catastrophic. |
The last gap is the one people underestimate. A verified specification and a verified implementation are different achievements requiring different tools. Projects like HACL* and EverCrypt, developed in the F* proof assistant and shipped inside Firefox's NSS library, close part of it by producing C code carrying machine-checked proofs of memory safety, functional correctness against a mathematical spec, and secret independence of timing. That work is expensive and it covers primitives rather than whole applications.
How to read a verification claim
When a vendor or a specification says a protocol is formally verified, four questions separate a substantive claim from a badge:
- Is the model published? The .spthy or .pv file should be available. If nobody can inspect the abstraction, nobody can check what it left out.
- Which properties were proved? Named, specific lemmas. Secrecy alone is a weak result if authentication was never queried.
- What was assumed away? Good analyses list their simplifications explicitly. A paper that admits it did not model the retry mechanism is more useful than one that never mentions it.
- Does the proof cover the deployed variant? Protocols acquire extensions. A proof of the core handshake may not survive the addition of a resumption mode or a new ciphersuite negotiation path, which is one reason cryptographic agility has to be designed rather than bolted on.
None of this makes formal verification less valuable. Model checkers routinely find flaws that survived years of expert review, because human review of concurrent systems does not scale and machines do not get bored on session seventeen. Lowe's result on Needham-Schroeder is the founding example, and thirty years later the tools are better and the protocols are far larger.
What it does mean is that "formally verified" is a sentence fragment. The full sentence names the tool, the model, the properties, and the assumptions, and a project that publishes all four is telling you something you can check. One that publishes the phrase alone has told you nothing you can act on.