Hi Nadim, Thank you for your recent updates to reftls and putting together this paper. The outcome also seem to align with my own WIP (although my hybrid modelling attempt dies to state explosion right now). Even with what I had put together myself, the reality was that I could see PQ-KEMs act as single points of failure just like DHE if standard cryptographic assumptions could not hold. So the conclusion your paper makes, regarding the strict improvement that a hybrid could provide makes sense.
Of course, symbolic models cannot reason over implementation challenges and so the next question may be fall more to pure speculation. I am curious if you might anticipate potential implementation errors moving from classical DHE or pure PQ-KEM towards a hybrid that risks compromising both methods due to complexity? Again, as I understand, symbolic models can merely affirm the consequences of dual compromise, but can’t help us reason about implementation challenges, I get that. So this question is more or less probing your personal PoV as an applied cryptographer Thanks again, Nathanael On Thu, Jun 4, 2026 at 5:52 AM 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]
