[TLS] Re: FATT Chance: On the Robustness of Standalone and Hybrid ML-KEM Key Exchange in TLS 1.3

[Nadim Kobeissi <[e-mail]>]

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 <[e-mail]> 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 -- [e-mail]
> To unsubscribe send an email to [e-mail]