Hello Nadim,
On 6/6/26 08:25, Nadim Kobeissi wrote:
Hi Nathaniel,
The reasons why I wouldn’t submit my analysis to top-tier conferences are:
1) The paper’s too short,
2) The findings aren’t novel or surprising.
When we submitted our previous analyses, we addressed 1) by adding CryptoVerif
models and a reference implementation, and 2) by finding attacks.
I want to push back here and say that you are underselling your work. I
would not reject this kind of paper as a PC member of a conference.
There are several additional modeling improvements for related drafts
that could be made where it would probably be great at a conference. I
stress, could, but not must.
Part of the finding that is novel is that the IETF didn't require this
work, that important people in the IETF are discouraging the use of the
FATT, and maybe the IETF will continue to push for pq only constructions
against the scientific results.
I hope that the latter is not true, but your work has put that very
point to the test. Thank you for advancing the discussion with your
contributions.
I don’t appreciate your implying that just because I’m not targeting a venue
that my results are somehow less comprehensive or reliable. I wrote my latest
analysis with serious effort, having done my PhD mostly on ProVerif and having
more than a decade of ProVerif experience. and if you want to question the
reliability of the results, I suggest you do so by finding concrete issues. I
found your email very annoying.
I read the emails the same way. I am glad to see that it appears to be a
misunderstanding. You do not deserve any shade or mistreatment.
Furthermore, your work here is excellent and the new models are
extremely useful. I have run the verification of the new pq models and
the results appear to match what is claimed in your paper. I have not
had time to check carefully but so far everything looks great. I will
think about all of the resulting verification runs more carefully and
than I will send feedback off-list.
Thank you Nadim! Thank you also to Usama for making this discussion happen!
Kind regards,
Jacob Appelbaum
Nadim Kobeissi
Symbolic Software • https://symbolic.software
On 5 Jun 2026, at 9:14 PM, Nathanael Ritz <[email protected]> wrote:
Hi Andrew,
Comments inline with [NR].
On Fri, Jun 5, 2026 at 11:58 AM Andrew Lee <[email protected]
<mailto:[email protected]>> wrote:
> Interestingly, despite the availability of scientific methods to
identify the best path forward, as proven by Dr. Kobeissi in this thread,
there was no interest in treading this path prior to making dangerous
recommendations to the populace.
[NR] There is a difference between a peer-reviewed study vs the good faith
input of a handful of individual contributors. There is also a difference
between availability of results between the good faith input of contributors
vs the constraints an author puts themselves under for publication at a top
tier security symposium.
From example, the IETF has been notified plenty of times that there are
“missing attacks” on the TLS key schedule from existing formal analysis that
reportedly affects the security of Remote Attestation over secure channels
like TLS depending on the timing of the attempted binding. However, because
the study is under presumably double-blind review, the authors are not in a
position to disclose exactly what those attacks look like, so the community is
left guessing at what mitigations may or may not be possible. This isn’t
nefarious — there are plenty of good (scientific) reasons why double-blind
review is the way it is. But there is a distinct trade-off.
In contrast, when individuals like myself or others such as Nadim can move
quickly to explore an open question like the impact of a KEM on the TLS key
schedule vs classical DHE, certain disclosures on List or such related efforts
may be treated more seriously than another, even if the outcome between both
of them is effectively equivalent (or so one may hope). But who judges that?
Prior presence, publication history and visible credentials absolutely affect
optics. It just so happens that the “quick” turnaround of the results can be
corroborated by separate individuals in this case.That’s all well and good,
but it doesn’t necessarily have the same “scientific” standing that a peer-
reviewed paper may have. Again, a significant trade-off.
That doesn’t mean a published paper is perfect or that individual good-faith
self-publications are totally unreliable. I am just saying that formal
analysis isn’t a commodity resource.
> [snip]
*> It would be a strong signal should the WG adopt this new custom as a
standard, go forward, requiring formal/symbolic analysis prior to making
any recommendations.*
[NR] And this moves towards the FATT process. While Usama, Nadim and I all
expressed interest or “energy” to do independent symbolic analysis to evaluate
the impact of PQ-KEM on TLS, none of the above are named members of the FATT
team. And the even then, FATT is specifically organized so that it cannot act
as an impediment to the normal progress of a draft. Specifically, the TLSWG
repo states clearly in part that, “the working group is under no obligation to
follow the FATT recommendations. If the FATT fails to provide output within a
reasonable time frame as determined by the working group chairs the processing
of the document should continue as normal.”https://github.com/tlswg/tls-fatt
<https://github.com/tlswg/tls-fatt>
The point is that the TLS FATT team is designed to be a helpful resource — but
by design is meant to be *helpful*, not uniquely bindingly authoritative on
TLSWG output.
Access to formal analysis is scarce for a reason. It’s complex, the results
often appear opaque to non-experts and I would personally expect those who
have developed their career around the skill are perhaps less likely to commit
to volunteering their time sufficient enough to avoid considerable delays. Of
course, I think the community should be very grateful to folks like Nadim who
is willing to modernize previously published models and take the results and
recommendations seriously. And Usama’s call for new models and soliciting for
help in producing them is admirable on its own.
But I guess it is just entirely unrealistic to expect the IETF to demand such
work from anyone, either from individuals or TLS FATT team members to the
point of declaring deep suspicion if such a scarce resource is not available
or called upon.
Further, the UFMRG exists for a reason (also identified by the specified FATT
process on the TLSWG GH repo), but if you take a look at that list, it appears
there are few souls regularly participating in that space as of late. And I
feel like that reinforces my point about how scarce access to formal analysis
actually is and why the chairs may hesistate to call for it on one draft or
another.
(I have not been part of this particular List long enough yet for me to feel
comfortable making any remarks regarding recent debates regarding consensus at
all, btw).
Cheers,
Nathanael
_______________________________________________
TLS mailing list -- [email protected]
To unsubscribe send an email to [email protected]
_______________________________________________
TLS mailing list -- [email protected]
To unsubscribe send an email to [email protected]
_______________________________________________
TLS mailing list -- [email protected]
To unsubscribe send an email to [email protected]
