Hi Yaakov, Thanks, it’s great to see folks actually engaging with the work.
> 1. The new code is a relatively small addition to the original ProVerif, and > thus it is enough to focus on it. That’s correct. I intentionally made the changes strictly incremental on top of the previous models in order to facilitate review. > 2. The modeling of section 3 captures at a very very high level the essence > of what a KEM is. > As I stated in a previous email, the commutativity issue is an artifact of DH > which is used to show that the two parties > share a secret, the new code (which is along the lines of what I too > proposed) shows the same feature for a generic KEM. Yep, the Dolev-Yao symbolic model largely restricts how granularly we can define ML-KEM, or any KEM, so the idea here was to define something that provides a contrast to the commutativity of DH. I welcome increases in precision to how we can define these things, if not in ProVerif then maybe in competing tools like Tamarin. > The kem-leak rule models at a very high level the collapse of a broken KEM – > i.e., the shared secret becoming directly recoverable by another party. I > would have preferred modeling a more specific break of LWE-based ML-KEM, > but that would be both harder and more restrictive. I welcome your ideas there. > The kem-leak rule only models a strong complete break where the attacker > immediately recovers the entire secret. > There can be softer breaks (like the MATZOV one). CryptoVerif is a better tool for this. > I am not sure that all edge cases (what if the KEM returns “failed” or the FO > receives invalid input) have been included. If you want to lay out those edge cases, I can take a look and see which ones would make most sense in the model. I can go looking again in the RFCs myself, but I’d appreciate pointers which will likely give me starting points and save time. > 6. All such analyses model protocol behavior, and can not answer > algorithmic questions. > Don’t expect it to answer open questions like whether ML-KEM is broken > classically or to a CRQC. This is a given; that’s not the kind of analysis that ProVerif is meant to do. > I personally prefer a more classic scientific paper style, rather than the > more playfully literary one > (and was it a Tuesday or a Thursday???) but chacun a son gout. So, I allowed myself a playful style, but I made sure to contain it purely in the first half of the introduction, so that it can exist, hopefully make people laugh, but not actually be an impediment to reading and understanding the paper seriously. Thanks, Nadim Kobeissi Symbolic Software • https://symbolic.software > On 8 Jun 2026, at 7:08 PM, Yaakov Stein <[email protected]> > wrote: > > > Can we all calm down? > > Were I to receive this paper for review (and I was on the editorial boards of > several journals) > I would say as follows: > > The new code is a relatively small addition to the original ProVerif, and > thus it is enough to focus on it. > The modeling of section 3 captures at a very very high level the essence of > what a KEM is. > As I stated in a previous email, the commutativity issue is an artifact of DH > which is used to show that the two parties > share a secret, the new code (which is along the lines of what I too > proposed) shows the same feature for a generic KEM. > The kem-leak rule models at a very high level the collapse of a broken KEM – > i.e., the shared secret becoming directly recoverable by another party. I > would have preferred modeling a more specific break of LWE-based ML-KEM, > but that would be both harder and more restrictive. > The kem-leak rule only models a strong complete break where the attacker > immediately recovers the entire secret. > There can be softer breaks (like the MATZOV one). > I am not sure that all edge cases (what if the KEM returns “failed” or the FO > receives invalid input) have been included. > All such analyses model protocol behavior, and can not answer algorithmic > questions. > Don’t expect it to answer open questions like whether ML-KEM is broken > classically or to a CRQC. > I personally prefer a more classic scientific paper style, rather than the > more playfully literary one > (and was it a Tuesday or a Thursday???) but chacun a son gout. > > Summing up, the enhanced model does what it set out to do, namely adds a > generic KEM to TLS > and shows that by exploiting the fact that decapsulating an encapsulated > secret returns the original secret > we regain the same situation as for DH. > > This is hardly surprising, but is reassuring that it can be formally obtained. > Had this not been obtained I would be highly suspect of the modeling. > > Furthermore, the paper shows that if the KEM breaks but we have hybridized > it with a non-broken mechanism > that the other mechanism saves the day. > Once again, not surprising, but reassuring. > > Rich – please count one peer review out of the usual three (but admittedly > not double-blind). > Nadim – let your work speak for itself. > > Y(J)S > > From: Nadim Kobeissi <[email protected]> > Sent: Monday, June 8, 2026 6:00 PM > To: Salz, Rich <[email protected]> > Cc: Nathanael Ritz <[email protected]>; [email protected] > Subject: [TLS] Re: FATT Chance: On the Robustness of Standalone and Hybrid > ML-KEM Key Exchange in TLS 1.3 > > Rich, seriously, cut it out. > > If you want to critique a work, critique it by reading it and providing > technical, scientific rebuttals against it. > > Counting the number of authors or the publication venue is such a stupid way > to critique scientific work. > > This is the second time you make this idiotic claim. It’s deeply stupid. > That’s not how you critique someone’s work or judge its value. > > I am absolutely certain that if the paper was *also* published on ePrint and > *also* had a single author, but that author’s name was Karthikeyan Bhargavan > or Cas Cremers, you wouldn’t be repeating this deeply brain-dead line of > reasoning. > > Nadim Kobeissi > Symbolic Software • https://symbolic.software <https://symbolic.software/> > > > On 8 Jun 2026, at 4:39 PM, Salz, Rich <[email protected] > <mailto:[email protected]>> wrote: > > > > On 6/8/26, 12:28 AM, "Nathanael Ritz" <[email protected] > <mailto:[email protected]>> wrote: > > > Independent machine-checked symbolic analysis using ProVerif [REF] > > This gives too much credit to one individual’s work that is not in a > peer-reviewed journal or conference. Nothing against Nadim, he deserves all > the credit for what he did, but let’s not overstate it. For example, maybe > the first word should be “An …" > _______________________________________________ > TLS mailing list -- [email protected] <mailto:[email protected]> > To unsubscribe send an email to [email protected] <mailto:[email protected]> > > This message is intended only for the designated recipient(s). It may contain > confidential or proprietary information. If you are not the designated > recipient, you may not review, copy or distribute this message. If you have > mistakenly received this message, please notify the sender by a reply e-mail > and delete this message. Thank you. > _______________________________________________ > TLS mailing list -- [email protected] <mailto:[email protected]> > To unsubscribe send an email to [email protected] <mailto:[email protected]>
_______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
