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

[Watson Ladd <[e-mail]>]

On Mon, Nov 2, 2026 at 11:12 PM Nathanael Ritz <[e-mail]> wrote:
>
> Hi,
>
> On Mon, 2 Nov 2026 at 06:01, Nadim Kobeissi <[e-mail]> wrote:
>>
>> <snip>
>>
>> [...] 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.
>>
>
> I can only imagine the framing behind "[...] starts standing in for 'we proved it secure' [...]" is focused at intentional bad-faith marketing attempts or naive interpretations of the tooling (aka in service to pitch decks and the like). In which case, the premise sounds more than plausible.

When an attack is found with ProVerif, it exists. ProVerif is walking
a large tree of derivations, and attempts to show by exhaustion
certain terms can't be derived. This is only possible because of a
lack of equational power in some respects. However, a finding that no
tree exists is dependent on the correctness of the very large search
process, and there can be bugs that cut it off too soon.

Provers like HOL and Coq and Lean use a fundamentally different
approach where a proof is a term that is typechecked. Typecheckers can
be very very small. How the term is derived is irrelevant, so the use
of tactics to make the term in a human (or now AI) approachable way
doesn't impact the correctness. Indeed one could write an independent
checker just for the final term that ignores all the tactics that lead
to it. How to apply to the logic ProVerif instantiates I do not know.
I have to confess to having a lack of appreciation for basic logic in
undergrad that kept me from learning enough about its applications
now.

Sincerely,
Watson