Hi Usama, Thanks, I wholly agree with your message. > Nadim, perhaps you could propose a PR [2] summarizing your analysis in > something like one paragraph? >
Done: https://github.com/tlswg/draft-ietf-tls-mlkem/pull/20 Nadim Kobeissi Symbolic Software • https://symbolic.software > On 6 Jun 2026, at 3:12 PM, Muhammad Usama Sardar > <[email protected]> wrote: > > > Hi all, > > sorry for the length; I waited for the discussion to settle to some extent. > TL;DR is I like John's summary. > >> I think the paper’s genuinely strong contributions are, in the symbolic >> (Dolev–Yao) model: >> >> 1. KEM-based key exchange in TLS 1.3 is secure. >> 2. Hybrid key exchange following draft-ietf-tls-hybrid-design remains secure >> unless both components are broken simultaneously. >> 3. A compromise of the key exchange also compromises handshake >> authentication, not just confidentiality. >> 4. Key share reuse breaks forward secrecy. [...] >> I would support TLS specifications citing the paper for contributions 1–4 >> [...] > > John's summary matches my understanding of the paper, and I would be happy if > the above are added to the security considerations section of draft citing > the paper for interested readers to read more. Slight addition I will make to > #2 is that this is the reason for preference of hybrid over standalone. > > >> 6. The claim that X25519MLKEM768 is robust is made under a classical >> Dolev–Yao attacker model. The relevant threat model to analyze >> quantum-resistant TLS is a quantum Dolev–Yao attacker. In that setting, >> ECDHE is broken by assumption, and the hybrid “both must fail” guarantee >> reduces to “ML-KEM must hold”, which is identical to the standalone >> assumption. > The claim that CRQC will break all ECDHE keys has been disputed. I have no > personal opinion but as such, this needs more research on what CRQCs can > actually break. Since this has come up a few times now, I'll add it to the > list in the draft. > > >> X25519MLKEM768 is already the de facto standard. In addition to making it >> RECOMMENDED=Y, I think it should be MTI. > I agree. I would recall that you have mentioned making it MTI a couple of > times and I have agreed with you a couple of times :) Rather than keep > re-stating and re-agreeing, I would appreciate if you or someone could tell > what the next step might be, or a sample of draft of what is the right way to > make it MTI. Unless someone is eager to take it, I will happily prepare a > draft, if one is required. > > === > > >> Following up on the implementation-test point, I think the artifact would be >> most useful if kept small and explicitly non-blocking: a list of negative >> cases implementers can run against hybrid key exchange code, not a condition >> for progressing the draft. > > I very much value this work. > > >> The cases I would start with are: [...] > That looks a very good start to me. > > >> If others think this is worth capturing, [...] > I think this is pretty much worth capturing. I would welcome this > contribution. > >> If there is a preferred place for such cases – draft text, a GitHub issue, >> or a separate test-artifact note – I can help shape it there. > Maybe discuss on the list first -- preferably as a new thread with a suitable > subject because your contribution seems orthogonal to the subject of this > thread, and maybe give a weeks or so for people to have a look and give some > feedback. > After incorporating that feedback, PR is most welcome here [0]. You are also > welcome as co-author. My current plans for the draft are: > Building rough agreement on statement for preference of hybrids and citation > of Nadim's paper for fine details > Summary of formal methods (symbolic and computational) works for hybrid and > standalone ML-KEM > Capturing the views of IETF on hybrid vs. standalone ML-KEM > Implementation guidance: you are welcome to lead this part as I currently > don't have much to add here. > > But I am very open to your or others' suggestions if this is too much for a > single draft. > > === > >> we add a statement on preference of hybrids and refer to the paper in the >> security considerations of draft-ietf-tls-mlkem. >> We already do that by marking the hybrid as RECOMMENDED=Y and the >> pure-ML-KEM as RECOMMENDED=N >> > Sure, writing it in security considerations explicitly with a few fine > details -- as John has mentioned -- and reference to paper would give the > readers the rationale for this to make informed choices. > > === > > >> 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. > FWIW, I would really like that we follow the FATT process in its true spirit > rather than this "new custom" of making someone -- who has served the WG > since the initiation of FATT process in doing the formal analysis for drafts > -- go to the extent of writing a draft just to say that in his estimation, > specific draft would benefit from a FATT review. > > In return, he is made to justify: > > why formal analysis is required? > what formal analysis will bring out? > if this document needs formal analysis then why another document already in > publication queue does not need formal analysis? > IMHO, these are maybe the kinds of questions that the FATT process is > intended to evaluate, not for me to justify. > > I do not recommend adopting this "new custom" at all. Let's just follow FATT > process, please! > > Anyway, all is well that ends well. I want to thank everyone who issued > attestations on the need for FATT review and in particular I really > appreciate Nadim's dedicated efforts, specially doing it at high priority. > > === > > >> all versions of draft-ietf-tls-mlkem including before adoption have had >> Recommended=N for all parameter sets > What I recollect is that some folks proposed to add a statement on the > preference for hybrids and it was not added in the draft. I may have > misunderstood others but I surely did [1]. > > === > > >> Deirdre, could you please add a statement to draft-ietf-tls-mlkem >> referencing that hybrids are preferred, ideally citing my analysis once it >> hits ePrint? I know that we have the RECOMMENDED=Y/N column, but I believe >> that adding this statement to the draft could enrich it with context that >> reflects our current understanding and provides valuable context to future >> readers. This is especially the case since Table 2, for example, in my >> analysis provides a granular and pedagogical overview of exactly how formal >> analysis has shown differences between pure DH, pure ML-KEM, and hybrid >> constructions. > +1 > > Nadim, perhaps you could propose a PR [2] summarizing your analysis in > something like one paragraph? > > === > > >> So I don't think in general being under submisison should preclude posting >> results to IETF lists. > That's also my understanding. The results under discussion were shared with > all relevant lists, e.g., [3-6], to protect the potential harm that > integrating remote attestation within handshake (intra-handshake attestation) > can do. A clear solution was provided to do remote attestation over the > established TLS connection (post-handshake attestation). There are several > slides and even recordings available, including but not limited to IETF and > IRTF [7], Moreover, there were several attestations already: > > vendor acknowledgement [8] > Security advisory [9] > CVE [10] > A promise to release artifacts under Apache-2.0 license was already made. I > would love to hear if someone genuinely thinks something is missing in the > detailed explanation in say [3-10], and will make every effort to clarify it > after discussion with my co-authors. > > === > > >> I want to push back here and say that you are underselling your work. > I share this feeling. For several months, there has been a dispute, several > appeals, bunch of circular tabletop discussions, etc. FWIW, putting an end to > all of that using formal methods and setting the WG back to normal operation > is a very valuable and practical contribution, and I hope the reviewers you > get will appreciate this. > > Best regards, > -Usama > > > [0] https://github.com/muhammad-usama-sardar/risks-of-mlkem > [1] https://github.com/tlswg/draft-ietf-tls-mlkem/issues/16 > [2] https://github.com/tlswg/draft-ietf-tls-mlkem > [3] https://mailarchive.ietf.org/arch/msg/seat/8tzc62Xe7sKnyInFHkMAx6z6QjU/ > [4] https://mailarchive.ietf.org/arch/msg/tls/8lyqHh9y7_Lv6b1iXhpUqYrp0M0/ > [5] https://mailarchive.ietf.org/arch/msg/rats/6gbqx0XY8WYrH3Mx4vO8n2-uKgY/ > [6] https://mailarchive.ietf.org/arch/msg/ufmrg/ZWK0uMM92OdwlPbgXBvQApDpe5Q/ > [7] > https://github.com/CCC-Attestation/formal-spec-KBS#upcoming-and-recent-talks-and-research-visits > [8] > https://web.archive.org/web/20260227160554/https://www.ultraviolet.rs/blog/tee-tls-privacy/ > [9] > https://github.com/ultravioletrs/cocos/security/advisories/GHSA-vfgg-mvxx-mgg7 > [10] https://www.cve.org/CVERecord?id=CVE-2026-33697 > > _______________________________________________ > 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]
