I really enjoyed working on this paper. I intend to have an entire investigative series where I do deep dives and either prove/disprove things in cryptography that people are asking open questions about, purely so that I can publish papers where the introduction involves an alternate universe where I’m a 1920s private eye, which increasingly becomes more elaborate paper after paper as the backstory grows.
If anyone has anything they’d like me to look at, try your luck. I may just take the case. Nadim Kobeissi Symbolic Software • https://symbolic.software > On 4 Jun 2026, at 7:19 PM, John Mattsson <[email protected]> wrote: > > > 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]
