Clarifying this (having received emails misinterpreting my previous email), I’d like to point that the conclusion of the formal analysis very strongly supports the case for hybrids over pure ML-KEM.
This is clearly noted in the abstract and the conclusions, and is very clearly summarized in Table 2 on page 10. Nadim Kobeissi Symbolic Software • https://symbolic.software > On 4 Jun 2026, at 5:28 PM, Nadim Kobeissi <[email protected]> wrote: > > 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]
_______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
