Hi Bas, You’re most welcome, respected sir. It was a pleasure to work on this and I certainly hope that I was able to provide something of value to this working group. Also, I laughed so hard while writing the introduction that my sides literally hurt. This was the reward I gave myself for the effort spent on this.
> Would you agree that this can be summarized as: our existing informal > understanding is now formalized. Yes. I suspect the question behind your question is: can we lay to rest the concerns behind draft-usama-tls-risks-of-mlkem. My answer is “yes” to both your question and my imagined one. Onward! Nadim Kobeissi Symbolic Software • https://symbolic.software > On 4 Jun 2026, at 5:25 PM, Bas Westerbaan <[email protected]> wrote: > > 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 <https://symbolic.software/> >> >> _______________________________________________ >> TLS mailing list -- [email protected] <mailto:[email protected]> >> To unsubscribe send an email to [email protected] >> <mailto:[email protected]>
_______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
