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]
