> It does not promote it; Yes, but this is a recurring theme in this whole issue, isn’t it?
- It doesn’t promote static client key shares, despite modifying a part of the protocol that was formally modeled and analyzed in the past. - It doesn’t mandate ML-KEM, it’s an optional mode with “Recommended=N”. The pattern: “no, it’s doesn’t quite throw the baby out with the bathwater, but it makes it easier to.” On the whole, this proposed draft offers nothing whatsoever cryptographically to TLS other than damage. I remain deeply confused as to how people are pushing for it. None of this makes any sense. It really doesn’t. Nadim Kobeissi Symbolic Software • https://symbolic.software > On 20 Feb 2026, at 4:54 PM, Deirdre Connolly <[email protected]> wrote: > > > The significant change introduced by this draft is the promotion of static > > client key shares. My understanding is that prior formal analyses of TLS > > 1.3 assumed that client key shares are ephemeral. If that is correct, then > > this draft modifies a part of the cryptographic protocol that was formally > > modelled and analyzed in the past. > > It does not promote it; as with the -hybrid-design and -ecdhe-mlkem > documents, it acknowledges that RFC 8446 does not forbid key reuse and > therefore key agreement mechanisms MUST be secure in the case of reuse, which > ML-KEM is. Here is the text from § Security Considerations on the updated > github copy > (https://github.com/tlswg/draft-ietf-tls-mlkem/blob/main/draft-ietf-tls-mlkem.md) > as the WGLC has been proceeding: > > > Implementations MUST NOT reuse randomness in the generation of ML-KEM > ciphertexts— it follows that ciphertexts also MUST NOT be reused. > > > TLS 1.3 does not require that ephemeral public keys be used only in a single > key exchange session; some implementations may reuse them, at the cost of > limited forward secrecy. ML-KEM is explicitly designed to be secure in the > event that the keypair is reused by its IND-CCA security. While it is > recommended that implementations avoid reuse of ML-KEM keypairs (also called > 'static' keys){{NIST-SP-800-227}} to ensure forward secrecy, implementations > that do reuse MUST ensure that the number of reuses abides by bounds in > {{FIPS203}} or subsequent security analyses of ML-KEM. > > > > On Fri, Feb 20, 2026, 8:37 AM John Mattsson > <[email protected] > <mailto:[email protected]>> wrote: >> Hi Usama, >> >> >From a formal perspective, my concern is about >replacing (EC)DHE by >> >shared_secret [0]. That is a key >schedule modification and as per FATT [1]. >> >> Unless I miss something, I don’t think replacing one shared secret with >> another constitutes a change to the key schedule. Both (EC)DHE and ML-KEM >> can be modelled as KEMs in which both parties contribute to the >> establishment of the shared secret. From that perspective, the key schedule >> remains structurally the same; only the underlying primitive used to derive >> the shared secret changes. >> >> The significant change introduced by this draft is the promotion of static >> client key shares. My understanding is that prior formal analyses of TLS 1.3 >> assumed that client key shares are ephemeral. If that is correct, then this >> draft modifies a part of the cryptographic protocol that was formally >> modelled and analyzed in the past. >> >> Cheers, >> >> John >> >> From: Muhammad Usama Sardar <[email protected] >> <mailto:[email protected]>> >> Date: Friday, 20 February 2026 at 13:27 >> To: Nadim Kobeissi <[email protected]>, [email protected] >> <mailto:[email protected]> <[email protected] <mailto:[email protected]>> >> Subject: [TLS] Re: WG Last Call: draft-ietf-tls-mlkem-07 (Ends 2026-02-27) >> >> Hi Nadim, >> >> I agree with almost everything you are saying, except your comments about >> quoted text from older version -05: please see inline. >> >> On 20.02.26 09:32, Nadim Kobeissi wrote: >> My background in formal verification of TLS 1.3 (e.g. >> https://inria.hal.science/hal-01528752/file/RR-9040.pdf) >> Thank you for this work. A few year ago, we found it as a useful starting >> point. While we discovered some issues (particularly in TLS 1.3 key >> schedule) in that formal analysis and had trouble getting responses from you >> and your co-authors back then (I understand you and Karthik moved on to >> other things and Bruno got too busy), I am happy that you are on this list, >> and hope that I can get some feedback from you to get the formal analysis >> for FATT done faster. >> So I would like to share my preliminary working of formal analysis of this >> specific draft for your opinion/feedback. For reference, from a formal >> analysis perspective, I do have deep and thorough understanding of TLS 1.3 >> (including the key schedule and up to cryptographic level functions like >> HKDF-Extract and HKDF-Expand) but it is my first PQ draft for formal >> analysis and so I'd very much appreciate your insights. >> >> From a formal perspective, my concern is about replacing (EC)DHE by >> shared_secret [0]. That is a key schedule modification and as per FATT [1]: >> >> For example a proposal that modifies the TLS key schedule or the >> authentication process or any other part of the cryptographic protocol that >> has been formally modeled and analyzed in the past would likely result in >> asking the FATT, whereas a change such as modifying the SSLKEYLOG format >> would not. >> >> So this draft "modifies the TLS key schedule" and this part has been >> "formally modeled and analyzed in the past", such as you analyzed in your >> work. Hence, I believe this should need expert review of FATT. What do you >> think? Am I missing something? >> >> The above key change alone breaks my formal proof (and I believe also yours >> since mine is based on yours). What do you think? >> >> Hybrid constructions provide a clean guarantee: key establishment remains >> secure under compromise of either component. This is a property worth >> preserving >> Yes, at least until there is sufficient formal proof for pure PQ. >> FIPS 203 (ML-KEM) [FIPS203] is a FIPS standard for post-quantum >> [RFC9794] key establishment via lattice-based key establishment >> mechanism (KEM). Having a purely post-quantum (not hybrid) key >> establishment option for TLS 1.3 is necessary for migrating beyond >> hybrids and for users that want or need post-quantum security without >> hybrids. >> I shared similar concerns on motivation in last WGLC because this text is >> from -05 whereas the one under WGLC now is -07. There was a typo in the >> subject. Please see -07 if that addresses some of your concerns. >> Please do not adopt this draft. >> It is already adopted. To be clear, did you mean: >> >> Please do not publish this draft. OR >> Please park this draft. >> Thanks. >> >> -Usama >> >> PS: unrelated to this topic, but given your formal analysis background, I'd >> really appreciate any opinion at your earliest convenience in the thread [2] >> for formal analysis of RFC9261. Thank you! >> >> [0] https://datatracker.ietf.org/doc/html/draft-ietf-tls-mlkem-07#figure-1 >> >> [1] https://github.com/tlswg/tls-fatt?tab=readme-ov-file#document-adoption >> >> [2] https://mailarchive.ietf.org/arch/msg/tls/I9UeeY9vwGl_zEzhaSKEOC4ZCKc/ >> >> _______________________________________________ >> 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]
_______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
