> 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 <john.mattsson= [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]> > *Date: *Friday, 20 February 2026 at 13:27 > *To: *Nadim Kobeissi <[email protected]>, [email protected] <[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: > > 1. Please do not publish this draft. OR > 2. 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] > To unsubscribe send an email to [email protected] >
_______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
