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:
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.My background in formal verification of TLS 1.3 (e.g.https://inria.hal.science/hal-01528752/file/RR-9040.pdf)
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.
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.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.
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. -UsamaPS: 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/
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
