Hi John,Thanks for sharing your insights and providing useful input for the formal analysis.
On 20.02.26 14:36, John Mattsson wrote:
You are right. The key schedule structurally remains the same but please recall that the key schedule was structurally also the same in RFC8773bis, where FATT did require formal analysis. Also, please note that RFC8773bis was a much smaller change (see [0] for my short comparison of this draft with RFC8773bis).>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.
In 8773bis, it was assumed to be pre-shared, so it was not a problem IMHO. On the contrary, in my understanding, this draft establishes the shared key.
From formal analysis perspective, I believe which key goes into the structure and how that is established matters. So you may not call it "key schedule modification" but I think you will agree that if that key was generated by a weak process, or if someone else has access to this key, it is game over independent of the structure of key schedule. As some folks are pointing out, I think we don't have sufficient evidence yet about the strength of pure ML-KEM-based key establishment.
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.Yes, that is correct for my model as well as Nadim's model. I am not aware of any formal analysis in traditional adversary (non-PQ) settings where this is not the case. If someone knows, please share a pointer.
Agree, this is another reason that warrants a careful formal analysis for security considerations. I recall that I have /intuitively/ supported your concerns on key reuse in the last WGLC [1].If that is correct, then this draft modifies a part of the cryptographic protocol that was formally modelled and analyzed in the past.
-Usama [0] https://mailarchive.ietf.org/arch/msg/tls/4WNwg6BnT5EIird8V77KSkXK4aY/ [1] https://mailarchive.ietf.org/arch/msg/tls/cGVWArNZO-N_r-5u5K8lBoVUitY/
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
