[CFRG] Re: Stop Calling Them Provers: The Case for Calling ProVerif and Tamarin Symbolic Protocol Analyzers

[Phillip Hallam-Baker <[e-mail]>]

I did my doctorate on formal methods in the 1980s, my college tutor was the
late Tony Hoare, he was very clear on the risks of over-reliance on formal
systems. All that a formal system can do is show that a system is correct
with respect to a specification, it cannot find bugs in the specification.

One of his famous examples was specification of a sort function that did
not require the output to be a permutation of the input. This example
brings to mind his aphorism, 'the physicists used to repeat each other's
experiments and now they run each other's code'. He reminded me of that
several times, my scholarship put me in the nuclear physics department next
door.

The problem I have with these systems is a bit more subtle: reliance on
formal methods encourage us to design systems that allow for formal
validation rather than systems that are robust in real world use when
implemented by programmers of ordinary skill in the art.

These are powerful tools and the more powerful the tool used, the greater
the understanding that is required of what it is applied to.



On Mon, Nov 2, 2026 at 7:01 AM Nadim Kobeissi <[e-mail]>
wrote:

> Hi everyone,
>
> I welcome discussion on my new pre-print. My new paper, "Stop Calling Them
> Provers", argues we should call ProVerif and Tamarin what they are:
> symbolic protocol analyzers. I base this argument on an audit of their
> published soundness arguments which found false statements, missing proofs,
> and gaps between the procedures justified on paper and those the tools run.
>
> I also discuss damning bugs: Tamarin will "verify" that no message is ever
> decrypted, even when the attacker can encrypt under the published key and
> hand the ciphertext straight to the decrypting process.
>
> A proof is something someone other than its author can check. When
> ProVerif prints "The query is proved, there is no attack", its manual adds
> that it "displays no attack derivation and no attack trace."
> Goubault-Larrecq called it in 2008: security "is demonstrated through the
> absence of a proof". Tamarin keeps a proof tree, but replays it with the
> same solver that built it. A solver bug corrupts the search and the check
> together.
>
> Tamarin's central solver optimization gets a paragraph of justification in
> a thesis, and no proof. SAPIC+'s state optimization, which exports to both
> tools, rests on a lemma that is false as printed.
>
> Calling these tools provers makes it such that "we ran Tamarin/ProVerif"
> starts standing in for "we proved it secure" in papers, audit reports and
> pitch decks. The authors of these tools have been curiously comfortable
> with this misleading practice, but it's time to put an end to it.
>
> Pre-print available here: https://eprint.iacr.org/2026/2683
>
> Nadim Kobeissi
> Symbolic Software • https://symbolic.software
>
> _______________________________________________
> CFRG mailing list -- [e-mail]
> To unsubscribe send an email to [e-mail]
>