Hi all, My read is that the two points Usama listed are reasonable if they stay narrowly scoped.
First, if formal-analysis artifacts already exist, a time-bounded FATT review seems consistent with the published FATT process. I would not treat that as a new gating criterion or as a reason to restart the broader ML-KEM discussion, but as a focused check of the artifacts against the claimed protocol-integration properties. Second, I think the Security Considerations would benefit from a short factual paragraph citing the symbolic-analysis artifact/paper for what it actually establishes: that the TLS integration has been modeled, what assumptions the model makes, and which integration properties were checked. That helps readers distinguish the cryptographic hardness assumptions of the primitive from the protocol-integration properties checked by the model. I would keep the implementation negative cases separate from those two points. They are useful, but orthogonal: malformed or missing shares, transcript/key-schedule binding, fallback/retry behavior, duplicate or ambiguous negotiation inputs, and fail-closed handling are implementation-facing checks rather than a process argument about the draft. Best, Songbo Bu On Thu, 11 Jun 2026 00:31:48 +0200, Muhammad Usama Sardar <[email protected]> wrote: > Hi Ilari, > > Thanks for taking the time and sharing detailed opinion. As > always, you are making good points here, which I agree to some > extent. > > One question I have is that: Could you please share your insight > why -- as I understand -- you seem to believe ECC will break > before ML-KEM? Unless I am missing something cryptographically, > both seem quite probable to me: no scientific rationale, just my > takeaway from the long bet [0]. I am asking because you are not > the first one. John also kindly keeps reminding me to update the > formal models that T in PQ/T will "soon" (2029?) be exactly 0. But > I haven't seen any argument why ML-KEM cannot break before that > "soon" and become 0 before X25519 part. Do we have any > cryptographic assurance for that? If so, could you possibly share > a reference for reading? > > On 10.06.26 15:37, Ilari Liusvaara > wrote: > > 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. > > As I mentioned a concrete clause, it is part of the FATT process. At least 3 > WG participants have already issued attestations. Since the analysis is done, > I see no reason why not to get it reviewed. > > Even if I have not looked at the proof itself, I think the results are > correct, > > That is probably the difference. FATT will actually look at the > proof, and attest to certain things, such as whether there is any > backdoor in the proofs (cf. background in [2]) or whether his proofs > are doing any "marketing" like my proofs. > > (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.) > > Sure, let's say I am more confident now about the absence of > potential flaws in the integration and happy to give up objection > conditional on two small and easy items. > > However, review would cause delay, as it would also concern > X25519MLKEM768. > > Hybrid is off-topic. The review I have requested is for standalone > ML-KEM draft. Hybrids could only be affected if some flaw > was discovered. That's not the case. Hybrid is in the publication > queue. I don't understand why you mention hybrids. > > On debates about ML-KEM, I do not expect those to convege until ECC > keys are dropping like flies left and right. > > Could you please explain why you think that would happen to ECC keys > first and not to ML-KEM keys first? > > 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, > > That seems like a strong statement. I am happy to present myself as > a counter-example for this statement. I am non-cryptographer and I > believe I understand all the technical details in the paper. > > I think it might be an > informative reference, > > Both PRs mentioned cite it as informative ref. > > as I do not think it contains anything the > security considerations do not already assert. > > I don't seem to find any reference to integration of ML-KEM in TLS > at symbolic level in the latest editor's copy. Could you please point me to > concrete reference which covers this analysis? > > 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. > > I don't see Sec. 5.1 in the editor's copy [1], which is the baseline > for these two PRs. Could you please confirm if you are looking at > [1]? > > # *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). > > Thanks for sharing your insights. > > 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)... > > Could you please share your insight on the big problem at an > abstraction level that I can understand (i.e., without going to very > deep cryptography)? > > 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. > > As mentioned above, I don't see anything on symbolic analysis or > integration. > > 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". > > I am not sure. What you mention seems to be cryptanalysis. > Isn't computational (vs. symbolic) proof actually > providing at least some level of guarantee on security of primitive? Do you > believe there is a clear boundary between the two? > > 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. > > Thanks for sharing your insights. > > 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... > > Thanks. I assume that as your attestation that my draft has > covered all major arguments and is ready for ISE path. > > Kind regards, > > -Usama > > [0] https://github.com/FiloSottile/ecc-vs-lattices-long-bet > > [1] > https://tlswg.org/draft-ietf-tls-mlkem/draft-ietf-tls-mlkem.html#section-5 > > [2] > https://mailarchive.ietf.org/arch/msg/tls/sqgOm7G34vpupyy7lyAVNU0r4Vg/ _______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
