Thanks for doing this, Nadim! Would you agree that this can be summarized as: our existing informal understanding is now formalized.
Best, Bas On Thu, Jun 4, 2026 at 1:53 PM Nadim Kobeissi <[email protected]> wrote: > 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] >
_______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
