Tanja’s assessment of my work is correct and adds important context. I wrote my paper upon the request of some folks on the list in order to helpfully close a gap in the FATT review process, but I honestly thought that my results showed that hybrids were preferable over pure ML-KEM, and on top of this, as the paper amply notes, symbolic analysis does not touch upon the lower-level computational notions intrinsic to the protocol’s primitives.
Nadim Kobeissi Symbolic Software • https://symbolic.software > On 7 Jul 2026, at 7:00 PM, Tanja Lange <[email protected]> wrote: > > Dear Muhammad, > Please see inline (though something in your email setting is messing up the > formatting by just indenting; extra > added for making this readable again). > > TL;DR > None of my concerns were addressed. I understand that your concerns are > addressed. > > On Tue, Jul 07, 2026 at 04:19:23AM +0200, Muhammad Usama Sardar wrote: >> Hi Tanja, >> >>> On 07.07.26 00:37, Tanja Lange wrote: >> >>> I do not support publishing this document. >> >> >>>> Significant developments have occurred both within this document and >>>> in the broader TLS ecosystem to address the concerns raised in the last >>>> WGLC. Therefore, the third consensus call is warranted. We ask the working >>>> group to consider document publication in light of these recent changes: >> >> >>> I do not see any of my concerns addressed by the changes, nor do I see any >>> acknowledgment of those concerns in the document. >> >> Respectfully, that's not correct. The WG paid special attention to your >> technical concerns and spent quite some energy in addressing those. See >> inline >> below. >> > I do acknowledge that the concerns of some people were addressed but not the > ones I expressed. I'll respond below to those individually. > >>> For reference, see below for >>> one of my emails from the previous last call. >> >>> Regards >>> Tanja >> >> >>> ----- Forwarded message from Tanja Lange <[email protected]> ----- >> >>> Date: Wed, 25 Feb 2026 21:04:24 +0100 >>> From: Tanja Lange <[email protected]> >>> To: Nadim Kobeissi <[email protected]> >>> Cc: Paul Wouters <[email protected]>, [email protected] >>> Subject: Re: [TLS] Re: WG Last Call: draft-ietf-tls-mlkem-05 (Ends >>> 2026-02-27) >> >>> I very much dislike this definition of "participant" and the assumption >>> that >>> those who don't speak up are in agreement. [...] >> >> I believe that's how IETF works. >> > I observe that is how this WG works, I don't think it should claim any opinion > for those who don't speak up. > >>> I think it is irresponsible of the WG to publish an RFC that encourages >>> risky >>> behavior. Users will take the reputation of the IETF and understand this >>> as a >>> recommendation, whether it says = N or not. >> >> Bas worked very responsibly to set X25519MLKEM768 = Y. I responsibly approved >> his PRs. The WG responsibly agreed to our proposal. >> > This is not addressing my concern about draft-ietf-tls-mlkem. It is improving > the status for ECC+ML-KEM. > >> The draft now responsibly includes promotion of hybrids. >> >> Can you show me a concrete attack resulting from risky behavior? >> > Well, it would have to be a vulnerability rather than an attack, but I assume > that's what you mean. > > Below you mention Nadim's proof. What that shows is that if you give away the > secret key of one of the components of ECC+PQC then the combined system is > still secure. If you only have PQC and give away the secret key for that, it > is > completely insecure. So, I assume that your question is how it could be that > we > give away the secret key for ML-KEM. > > a) If cryptanalysis of ML-KEM succeeds (completely, as in SIKE, or weakening > it > enough as RC4 or RSA-768) the only protection is gone, which makes the outcome > _worse_ than the current situation of pure ECC and worse than for ECC+ML-KEM. > Neither of those will help long-term, but at least the data is not exposed > yet. > b) If there are implementation errors in ML-KEM that remove or weaken the > security the only protection is gone. Same as a) > > I do acknowledge that adding ML-KEM to a functioning and likely more correct > ECC implementation adds risks. If the ML-KEM implementation permits taking > over > the machine then the security situation is worse. It is a risk-assessment step > to weigh this against the risk to user data from quantum attacks. At this > point > I consider the latter sufficiently severe and have sufficient hope for the > security of PQC to recommend using ECC+PQC for anything where data has > long-term value. Users have an expectation of privacy when using TLS, so we > should do our best to ensure that. I know that some TLS user data (e.g. public > YouTube videos) doesn't need long-term confidentiality, some other (e.g. > online > health consultations) does. ECC+PQC is our best bet for achieving that and > NIST > has standardized and fully specified ML-KEM, so I'm on board with the > ECC+ML-KEM RFC. > > None of these considerations puts solo ML-KEM as a safer option, while it > obviously adds risks. > > Just in case you were questioning the part that an RFC would be seen as an > endorsement: > I don't know your motivation, but you removed the bottom part of my email from > February in which I gave the Canadian agency as a clear example for my > statement. We recently got another confirmation that they are waiting for the > RFC in order to link to it. What more evidence does anybody need that the =N > will be ignored? > >>> As much as I like PQC and push for >>> its adoption asap because we're too late (not my fault), I also warn >>> about >>> stability and code quality and we must acknowledge that. I love formally >>> verified software like everybody else and it's the best we can do, >> >> The WG spent quite some time in planning, discussing and executing the formal >> analysis to the extent that nobody was complaining about formal analysis. >> Thanks to Nadim, it was finally formally verified in ProVerif and checked by >> at >> least one FATT member. So we have done "the best" we could do, as you seem to >> be saying. Computational proofs already exist and the WG seemed to believe >> that >> to be sufficient. >> > This might be one part of the misunderstanding. There are (at least) 3 layers > where formal verification is needed > * protocol level, > * proof of primitives level, > * implementation level. > A proof in ProVerif fits in the first category. I wrote "formally verified > software" which is the third kind and not addressed in the RFC and it concerns > the software ecosystem. > >>> but also >>> that is still a research area and we are currently in a situation where >>> code >>> can be formally verified and have bugs at the same time. >> >> That's may be the case but I don't know what we could technically do here >> other >> than forbidding key reuse. Maybe if you would have shared concrete ideas, we >> could have addressed it better. >> > I don't think that the state of ML-KEM is safe for use without additional > protection. This is a fundamental concern with the draft and needs to be > addressed by halting it till the state is better. This needs time and effort. > >>> That's not even >>> addressing the mathematical stability of the problems. >> >> I don't know what could be concretely done here. >> > Put the draft on hold to allow time for research. (Research funding is an > obvious way to support this but I don't expect this WG to solve that.) > >>> Still, it's better to >>> add ML-KEM than not deploying it, but please not without ECC. >> >> FWIW, that's what RECOMMENDED = Y/N does. So I believe it was addressed. >> > This is a change in a different RFC and does not address the concern with this > draft that it should not become an RFC. > >> Best regards, >> >> -Usama >> >> >> [0] https://www.ietf.org/archive/id/draft-ietf-tls-mlkem-08.html#section-5-1 >> > Regards > Tanja > > _______________________________________________ > 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]
