On Tue, Jun 09, 2026 at 03:17:52AM +0200, Muhammad Usama Sardar wrote: > [concluding email proposing the way forward; sorry for the length] > > Hi John, all, > > I took a few hours to read the whole thread again and carefully put this > together. Thanks for taking the time to read it and sharing your opinion. > > On 08.06.26 08:28, John Mattsson wrote: > > # *My proposed next steps* > > /My/ remaining objections are: > > 1. FATT review of artifacts as per FATT process [0]: FWIW, having > missed /initial/ FATT review may not necessarily imply that we also > miss the /final/ FATT review too. > > As I understand, /during/ WGLC is due to process reasons. In any > case, the sooner the FATT review is requested the better. Artifacts > are available; if author of draft is fine, these can probably be > sent now to FATT with say 2 weeks period that they can assess it at > their convenience. As delta to reftls is quite small, it would > likely be easy to assess. As other debates on ML-KEM are still > happening and these debates do not seem to me to be moving towards > convergence and I don't expect things to magically settle in 2 > weeks, there is absolutely no "delay" added by FATT review by any means.
I do not think FATT review is needed. Even if I have not looked at the proof itself, I think the results are correct, and it is extremely unlikely that there is any flaw in way ML-KEM or X25519MLKEM768 is integrated into TLS. (Technically formal proof only guarantees anything if all the assumptions hold, which is unlikely in practice. What one can expect from proof like this is discovering flaws or potential flaws.) However, review would cause delay, as it would also concern X25519MLKEM768. On debates about ML-KEM, I do not expect those to convege until ECC keys are dropping like flies left and right. > 2. PR#20 or #22 or something on these lines on symbolic analysis of > /integration/ of KEMs in TLS with citation of paper or artifacts is > added. I believe it is important to have this for the readers -- > particularly non-cryptographers -- in the security considerations to > make informed decisions. That paper seems way too technical for any non-cryptographers, and too technical even for many cryptographers. I think it might be an informative reference, as I do not think it contains anything the security considerations do not already assert. If the security considerations are clear enough is different matter: Section 5.1 reads a bit jargony to me, but it not expected to have been copy-edited yet. > # *My /personal/ position* > > I am not sure if any of the above two points would help any of other ca. 24 > opposing. At least with these two, I would stop opposing and move to 'no > opinion' for the draft. The crypto involved in ML-KEM is too complex for me > to check and more secure alternatives like X25519MLKEM768 are available. The way TLS uses ML-KEM is very simple. The math inside ML-KEM is more complicated, but mostly just matrix and vector math over a finite ring (the NTT stuff is just for speed). The FO part has been formally proven correct. Where things get really hard is if the underlying problem is hard enough. That is beyond anyone's capability to check, and the best that can be done is trying and failing to find a flaw (hence NISTPQC taking ~decade). > I think non-cryptographers like me can just wait to see whether ML-KEM or > X25519 breaks first. But whichever breaks first, X25519MLKEM768 will still > be secure. This hampers my support for standalone ML-KEM. Except that ML-KEM breaking first is still a big problem (unless it turns out CRQCs will never exist)... > This is /my/ personal position. WG is free to ignore one or both of above > items, in which case I will stay opposed (but not strongly), as these are > important considerations to me, and I am fine to be in the rough if others > do not share this opinion. I believe one reason of formal analysis is to get > assurance /ourselves/, and another IMHO equally important reason is to get > it evaluated by experts and put it in security considerations for the > /community/, so that community can make reasonable decisions. As the results were predictable, those have effectively already been incorporated into security considerations. Furthermore, any flaws would have been extremely surprising, and likely a serious problem. > Key reuse vulnerability is fixed via 8446bis; thanks to John for substantial > technical guidance in modeling this and to all who offered attestation for > the change. Moreover, integration of ML-KEM in TLS is checked in symbolic > model. That's almost as far as I could envision and help. Explaining why > ML-KEM itself is secure is up to cryptographers. As for security of ML-KEM itself: "Lots of people have tried, and nobody has been able to break it". Which is the case for most crypto (and the rest tends to be inpractical for most purposes). This includes ECC. > I would note that in the process, I may have offended several people, in > particular where I questioned things regarded "obvious" or "intuitive." I > sincerely apologize for that. Intuition and actually doing formal proof are > two different things. In cryptography, proving simple-looking statement with no obvious flaws can be quite hard. E.g., fast key erasure DRBGs (recursively expand seeds into output, which is overwritten as used, and the next seed). Or the various stuff about IND-CCA security of composites. That was pretty nasty. > One request I have is: Perhaps people -- both sides -- could be nice to > bring in /novel/ arguments on list and not repeat arguments already captured > in [3]. If there are novel arguments not already captured in [3], I would be > interested in hearing them to proceed further with the ISE path. Well, coming up with novel arguemnts seems pretty hard... -Ilari _______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
