Hi all, Thanks Nadim for providing this analysis. For those only on the mailing list: I have left some comments on Nadim’s PR at https://github.com/tlswg/draft-ietf-tls-mlkem/pull/20. I’m not against citing preprints, but there is also some published work we can reference.
I mildly prefer not having any recommendations for hybrids or not in this particular draft, but to be honest I mainly just want to move forward with things. I’ve superficially read through the paper and its description of the modeling of TLS 1.3 and KEMs. The modeling choices seems appropriate. The results are what we would expect, so in a way this is speaking to my confirmation bias, but I’m inclined to believe that the results are correct. As everybody is putting their peer reviewer hats on, I’d love to see a bit more discussion of related work in the paper, and would encourage Nadim to archive his artifacts with something like Zenodo. ;-) Cheers, Thom > Op 4 jun 2026, om 13:50 heeft Nadim Kobeissi <[email protected]> het > volgende geschreven: > > 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]
