Hi Nadim, Nathanael, Thanks for sharing the paper and the models. One implementation-facing angle that may be worth spelling out, even if it is outside what the symbolic model can prove, is which negative tests would best catch hybrid-specific integration mistakes.
For example, it would be useful for implementers to have test cases that exercise: - transcript binding of the complete selected key-share / KEM material, including group identifiers; - rejection when one component is malformed, absent, or associated with a different negotiated group; - no derivation of an application secret unless both advertised components are present and accepted under the negotiated hybrid group; - downgrade/confusion cases where a peer attempts to make a hybrid exchange look like a standalone KEM exchange, or vice versa. That would not change the proof result, but it may help bridge the gap Nathanael mentioned: the symbolic model says what must be true for hybrid robustness, while implementers still need fairly concrete checks to avoid accidentally losing one side of the hybrid binding. Best, Songbo Bu On Thu, 4 Jun 2026 06:36:21 -0600, Nathanael Ritz [email protected] wrote: 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]
