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

[Muhammad Usama Sardar <[e-mail]>]

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:

 1. Building rough agreement on statement for preference of hybrids and
    citation of Nadim's paper for fine details
 2. Summary of formal methods (symbolic and computational) works for
    hybrid and standalone ML-KEM
 3. Capturing the views of IETF on hybrid vs. standalone ML-KEM
 4. 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:

 1. vendor acknowledgement [8]
 2. Security advisory [9]
 3. 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