MIME-Version: 1.0
References: <1A7A2227-C395-44C4-8FF3-6A70EAB70038@symbolic.software>
In-Reply-To: <1A7A2227-C395-44C4-8FF3-6A70EAB70038@symbolic.software>
From: Phillip Hallam-Baker <phill@hallambaker.com>
Date: Mon, 2 Nov 2026 10:46:27 -0500
Message-ID: 
 <CAMm+LwjZLpe3G2D6xeoT6bx9h7xJdqbozgHep9-ky3qmcHOOyw@mail.gmail.com>
To: Nadim Kobeissi <nadim@symbolic.software>
Content-Type: multipart/alternative; boundary="000000000000455b2d065f4d0d12"
Message-ID-Hash: EWKQNV5QOI3BKU7VSJMSS5HYG3JJNGPB
CC: cfrg@ietf.org
Precedence: list
Subject: [CFRG] Re: Stop Calling Them Provers: The Case for Calling ProVerif and
 Tamarin Symbolic Protocol Analyzers
Archived-At: 
 <https://mailarchive.ietf.org/arch/msg/cfrg/epWCLLfDlhoepooqFxd1rwuFSV4>

--000000000000455b2d065f4d0d12
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

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=E2=80=AFAM Nadim Kobeissi <nadim@symbolic.softw=
are>
wrote:

> Hi everyone,
>
> I welcome discussion on my new pre-print. My new paper, "Stop Calling The=
m
> 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 proof=
s,
> and gaps between the procedures justified on paper and those the tools ru=
n.
>
> I also discuss damning bugs: Tamarin will "verify" that no message is eve=
r
> 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 add=
s
> 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 i=
n
> a thesis, and no proof. SAPIC+'s state optimization, which exports to bot=
h
> 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 =E2=80=A2 https://symbolic.software
>
> _______________________________________________
> CFRG mailing list -- cfrg@irtf.org
> To unsubscribe send an email to cfrg-leave@irtf.org
>

--000000000000455b2d065f4d0d12
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr"><div class=3D"gmail_default" style=3D"font-size:small">I d=
id my doctorate on formal methods in the 1980s, my college tutor was the la=
te Tony Hoare, he was very clear on the risks of over-reliance on formal sy=
stems. All that a formal system can do is show that a system is correct wit=
h respect to a specification, it cannot find bugs in the specification.</di=
v><div class=3D"gmail_default" style=3D"font-size:small"><br></div><div cla=
ss=3D"gmail_default" style=3D"font-size:small">One of his famous examples w=
as 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, &#39;t=
he physicists used to repeat each other&#39;s experiments and now they run =
each other&#39;s code&#39;. He reminded me of that several times, my schola=
rship put me in the nuclear physics department next door.</div><div class=
=3D"gmail_default" style=3D"font-size:small"><br></div><div class=3D"gmail_=
default" style=3D"font-size:small">The problem I have with these systems is=
 a bit more subtle: reliance on formal methods encourage us to design syste=
ms 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=
.</div><div class=3D"gmail_default" style=3D"font-size:small"><br></div><di=
v class=3D"gmail_default" style=3D"font-size:small">These are powerful tool=
s and=C2=A0the more powerful the tool used, the greater the understanding t=
hat is required of what it is applied to.</div><div class=3D"gmail_default"=
 style=3D"font-size:small"><br></div><div class=3D"gmail_default" style=3D"=
font-size:small"><br></div></div><br><div class=3D"gmail_quote gmail_quote_=
container"><div dir=3D"ltr" class=3D"gmail_attr">On Mon, Nov 2, 2026 at 7:0=
1=E2=80=AFAM Nadim Kobeissi &lt;nadim@symbolic.software&gt; wrote:<br></div=
><blockquote class=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;border=
-left:1px solid rgb(204,204,204);padding-left:1ex">Hi everyone,<br>
<br>
I welcome discussion on my new pre-print. My new paper, &quot;Stop Calling =
Them Provers&quot;, argues we should call ProVerif and Tamarin what they ar=
e: symbolic protocol analyzers. I base this argument on an audit of their p=
ublished soundness arguments which found false statements, missing proofs, =
and gaps between the procedures justified on paper and those the tools run.=
<br>
<br>
I also discuss damning bugs: Tamarin will &quot;verify&quot; that no messag=
e is ever decrypted, even when the attacker can encrypt under the published=
 key and hand the ciphertext straight to the decrypting process.<br>
<br>
A proof is something someone other than its author can check. When ProVerif=
 prints &quot;The query is proved, there is no attack&quot;, its manual add=
s that it &quot;displays no attack derivation and no attack trace.&quot; Go=
ubault-Larrecq called it in 2008: security &quot;is demonstrated through th=
e absence of a proof&quot;. Tamarin keeps a proof tree, but replays it with=
 the same solver that built it. A solver bug corrupts the search and the ch=
eck together.<br>
<br>
Tamarin&#39;s central solver optimization gets a paragraph of justification=
 in a thesis, and no proof. SAPIC+&#39;s state optimization, which exports =
to both tools, rests on a lemma that is false as printed.<br>
<br>
Calling these tools provers makes it such that &quot;we ran Tamarin/ProVeri=
f&quot; starts standing in for &quot;we proved it secure&quot; in papers, a=
udit reports and pitch decks. The authors of these tools have been curiousl=
y comfortable with this misleading practice, but it&#39;s time to put an en=
d to it.<br>
<br>
Pre-print available here: <a href=3D"https://eprint.iacr.org/2026/2683" rel=
=3D"noreferrer" target=3D"_blank">https://eprint.iacr.org/2026/2683</a><br>
<br>
Nadim Kobeissi<br>
Symbolic Software =E2=80=A2 <a href=3D"https://symbolic.software" rel=3D"no=
referrer" target=3D"_blank">https://symbolic.software</a><br>
<br>
_______________________________________________<br>
CFRG mailing list -- <a href=3D"mailto:cfrg@irtf.org" target=3D"_blank">cfr=
g@irtf.org</a><br>
To unsubscribe send an email to <a href=3D"mailto:cfrg-leave@irtf.org" targ=
et=3D"_blank">cfrg-leave@irtf.org</a><br>
</blockquote></div>

--000000000000455b2d065f4d0d12--