Hi Eric, You're right that "supports preferring" is a normative phrasing, and that a symbolic analysis establishes facts rather than a recommendation. I’m happy to state it as a fact.
You've also already said you'd accept stating it for failure of the traditional component and not just the PQ one, so I think we agree that the symmetric, either-component framing is the right one. The only thing I'd push back on is *which* fact, because the sentence below leaves out the half of the result that the surrounding paragraph actually turns on. > I wouldn't oppose a factual statement, such as "Machine-checked symbolic > analysis [REF] confirms that PQ/T key establishment is secure [potentially > this could be made more precise] even if either of the components is > compromised." That sentence describes the hybrid in isolation, but the paragraph it sits in is comparing standalone ML-KEM to hybrid, and "secure even if either component is compromised" says nothing about standalone, so it can't actually speak to the comparison the text is making. The analysis establishes a relation between the two modes, run concurrently under one attacker over shared keys: the hybrid stays secure as long as either component survives, whereas standalone ML-KEM's security rests on ML-KEM alone. Both halves are machine-checked as tight: one control shows that the ML-KEM-secure assumption is load-bearing for standalone (delete it from the statement and a standalone session leaks with no surviving excuse), and another shows that the hybrid leaks only when both components are weak. That dominance relation is the factual content behind the "conservative approach ... retaining at least the security currently offered by traditional algorithms" rationale already in the paragraph; it isn't an extra normative claim layered on top. > it mostly confirms the intuitive analysis that hybrids are secure in the case > of failure of either individual component For the hybrid's robustness, granted! I'd go further than you do: that part isn't only intuitive, it already has computational backing in the hybrid-combiner proofs of Bindel et al. and of Blanchet and Jacomme in CryptoVerif. But that is two of the paper's five findings! The other three don't confirm intuition; two of them answer questions raised in this very discussion. Briefly: (3) A broken sole key-exchange secret costs more than confidentiality; it costs handshake authentication. With the lone key-exchange secret public and no secret PSK salting the key schedule, the server Finished MAC key is public and the Finished message becomes forgeable, so a client can be driven to complete a handshake that no server ever completed, a loss of key confirmation (injective agreement), even though CertificateVerify still authenticates the server's identity. The contribution is the scope: standalone's single point of failure reaches authentication, and the hybrid resists that too, which the "confidentiality if either survives" framing simply does not contain. (4) Reusing an ML-KEM key trades away forward secrecy: an ephemeral key keeps past traffic secret even if the decapsulation key and the PSK later leak, whereas a reused-then-compromised key hands that traffic over. That substantiates the IND-CCA2 and limited-forward-secrecy guidance the drafts already give (mlkem 5.2-5.3, hybrid 2 and 6); it says nothing about hybrids either way. (5) Non-static roles, which is the central concern of draft-usama-tls-risks-of-mlkem. The worry was that the KEM's initiator/responder asymmetry, which Diffie-Hellman's symmetry concealed, might surface a role-confusion or unknown-key-share attack once one endpoint both initiates and responds. We ran exactly that: a single principal on both ends over shared keys, under both the wire-faithful encoding and a deliberately confusable raw encoding that lets the attacker hand an encapsulation key where a ciphertext is expected. No unknown-key-share, no reflection (in the server-authenticated, one-initiator-per-session setting we analyze). A negative answer to the question that motivated the review is, I'd argue, the opposite of confirming intuition! So I'd suggest keeping the statement factual, as you propose, but restoring the comparison. I'm happy with your sentence with even more precise changes, as you invited: "Machine-checked symbolic analysis of standalone ML-KEM, hybrid, and traditional key establishment, composed concurrently under a single active attacker, confirms that hybrid key establishment remains secure as long as either component is unbroken, whereas the security of standalone ML-KEM rests on ML-KEM alone [FATT]." And if the group wants the authentication point on the record, one more sentence does it: "The same analysis finds that this single point of failure reaches handshake authentication: absent a secret pre-shared key, compromise of the sole key-establishment secret makes the server Finished forgeable, which the hybrid likewise resists [FATT]." Nadim Kobeissi Symbolic Software • https://symbolic.software > On 7 Jun 2026, at 12:34 AM, Eric Rescorla <[email protected]> wrote: > > > > On Sat, Jun 6, 2026 at 7:44 AM Nadim Kobeissi <[email protected] > <mailto:[email protected]>> wrote: >> 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 > > Unless I misunderstand what Nadim says his analysis has shown, it mostly > confirms the intuitive analysis that hybrids are secure in the case of > failure of either individual component. I think the previous text captures > this effectively in terms of failure of the PQ component and wouldn't oppose > changing the text state that it applied to failure of the traditional > component as well, but I think this text implies a much stronger conclusion > than is supported by the analysis. > > I wouldn't oppose a factual statement, such as "Machine-checked symbolic > analysis [REF] confirms that PQ/T key establishment is secure [potentially > this could be made more precise] even if either of the components is > compromised." > -Ekr > >> >> Nadim Kobeissi >> Symbolic Software • https://symbolic.software <https://symbolic.software/> >> >>> On 6 Jun 2026, at 3:12 PM, Muhammad Usama Sardar >>> <[email protected] >>> <mailto:[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] <mailto:[email protected]> >>> To unsubscribe send an email to [email protected] >>> <mailto:[email protected]> >> >> _______________________________________________ >> TLS mailing list -- [email protected] <mailto:[email protected]> >> To unsubscribe send an email to [email protected] >> <mailto:[email protected]> > _______________________________________________ > TLS mailing list -- [email protected] <mailto:[email protected]> > To unsubscribe send an email to [email protected] <mailto:[email protected]>
_______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
