Thanks Nadim! Great work! Good that we can put this discussion behind us.
"This single point of failure reaches authentication as well as confidentiality: with the sole key-exchange secret exposed and no secret pre-shared key salting the key schedule, the server Finished message becomes forgeable, so a client can complete a handshake that no server completed, while the hybrid stays safe unless both components break." Note that once a CRQC emerges, which some people say may happen very soon, the X25519 component no longer provides any security, and ML-KEM becomes a single point of failure in both X25519MLKEM768 and ML-KEM768. I think formal analysis in the not so distant future should focus on quantum attackers and treat ECC and RSA as not providing any security. If people want robustness, the TLS WG should start working on ML-KEM + HQC-KEM hybrid KEMs [1]. Many TLS libraries enforce handshake timeouts, so unless the key exchange algorithm is completely broken, an attacker cannot practically keep a connection open long enough to forge the Finished message. It is great that TLS WG have clarified that static keys MUST NOT be used for key exchange. This significantly lower the risk for these kind of attacks. Cheers, John Preuß Mattsson [1] https://csrc.nist.gov/csrc/media/Events/2025/workshop-on-guidance-for-kems/documents/papers/ml-kem-is-great-paper.pdf From: Nadim Kobeissi <[email protected]> Date: Thursday, 4 June 2026 at 13:50 To: [email protected] <[email protected]> Subject: [TLS] FATT Chance: On the Robustness of Standalone and Hybrid ML-KEM Key Exchange in TLS 1.3 Hi everyone, Two post-quantum upgrades to TLS 1.3 are being standardized in parallel: a hybrid key exchange (already deployed) that runs an elliptic-curve Diffie-Hellman exchange alongside ML-KEM, and a standalone mode that uses ML-KEM on its own. The Internet-Draft draft-usama-tls-risks-of-mlkem points out that the machine-checked symbolic proofs of TLS 1.3 rely on the commutativity of Diffie-Hellman, which ML-KEM does not share: a key encapsulation mechanism is asymmetric, one endpoint generating a key pair and the other encapsulating against it. The existing proofs therefore no longer apply, a new one is needed, and the draft argues that hybrids should be preferred. I’m writing in order to supply that proof. In this paper, I extend the reftls ProVerif models with a faithful, non-commutative KEM and analyze classical (EC)DHE, standalone ML-KEM, and the hybrid together, as unbounded concurrent sessions against a single active attacker free to break any cryptographic component. The central result is a sharp and tight contrast in robustness: standalone ML-KEM is a single point of failure, secure only while ML-KEM itself is unbroken, whereas the hybrid stays secure as long as either of its components survives: an attacker must break both, in one session, to learn anything. This single point of failure reaches authentication as well as confidentiality: with the sole key-exchange secret exposed and no secret pre-shared key salting the key schedule, the server Finished message becomes forgeable, so a client can complete a handshake that no server completed, while the hybrid stays safe unless both components break. The three modes also interoperate without ever confusing one another's keys, so migrating from (EC)DHE to a hybrid is a strict improvement. Two further experiments address the draft's remaining concerns: reusing an ML-KEM key forfeits the forward secrecy that an ephemeral key preserves, and a principal acting as both initiator and responder exposes no role-confusion attack arising from the asymmetry. At the symbolic level, and under stated assumptions, the analysis substantiates the draft's case for preferring hybrid key exchange. The paper is temporarily available here while I wait for it to be published on ePrint (hopefully soon): https://github.com/symbolicsoft/reftls/blob/master/paper/tls-hybrid.pdf Once it’s on ePrint, please cite the ePrint version should you decide to cite the paper for any future work. The ProVerif models are available here: https://github.com/symbolicsoft/reftls/tree/master/pv Happy to answer any questions. Nadim Kobeissi Symbolic Software • https://symbolic.software
_______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
