On Sat, Jun 6, 2026 at 7:44 AM Nadim Kobeissi <[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 > > 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: > > 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 > > _______________________________________________ > 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] >
_______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
