Stop calling ProVerif and Tamarin provers, paper urges

Nadim Kobeissi has published a preprint arguing that ProVerif and Tamarin should be called symbolic protocol analyzers, not provers. The claim matters because clean runs of the tools are routinely treated, in research papers, audit reports, and commercial materials, as equivalent to a proof of security.

Kobeissi’s case rests on an audit of the tools’ published soundness arguments. He reports false statements, missing proofs, and gaps between the procedures justified on paper and the ones the implementations actually execute. He also describes concrete failures, including a Tamarin case in which the tool reports that no message is ever decrypted even when an attacker can encrypt under a published key and deliver the ciphertext directly to the decrypting process.

A proof, he writes, is something someone other than its author can check. ProVerif’s success message is the absence of an attack derivation; Tamarin retains a proof tree but replays it with the same solver that built it, so a solver bug can corrupt search and check together. Central optimizations, he argues, rest on thin or flawed justification. Jean Goubault-Larrecq’s 2008 observation that security is demonstrated through the absence of a proof is cited as the right framing.

On the Crypto Forum Research Group list, Watson Ladd drew the contrast with interactive theorem provers such as Coq, HOL, and Lean: those systems produce a checkable proof term that a small typechecker can verify independently of how it was built. ProVerif, by design, searches a large derivation space; finding an attack is strong evidence, but a report that no attack exists depends on the correctness of that search and can fail closed too early when the solver is wrong.

The practical risk is linguistic. Once “we ran Tamarin” or “we ran ProVerif” is allowed to stand in for “we proved it secure,” overclaiming becomes normal. Kobeissi’s preprint, posted as IACR ePrint 2026/2683, asks the community to retire the prover label and match the vocabulary to what the tools actually deliver.