This is indeed good outcome, it is probably worth sharing with pqc-forum.
Indeed, improving robustnes with some other schemes may be useful, but
going forward one may want to try to do hybridization with new
post-quantum schemes. For example, some people call isogeny crypto a
post-post-quantum crypto and maybe one day we can see MLKEM hybridized
with some new approach to isogeny-based key exchange (or anything else
with small keys).
Anyway, Good stuff.
Kris
On 04/06/2026 18:50, Nadim Kobeissi wrote:
I really enjoyed working on this paper. I intend to have an entire
investigative series where I do deep dives and either prove/disprove
things in cryptography that people are asking open questions about,
purely so that I can publish papers where the introduction involves an
alternate universe where I’m a 1920s private eye, which increasingly
becomes more elaborate paper after paper as the backstory grows.
If anyone has anything they’d like me to look at, try your luck. I may
just take the case.
Nadim Kobeissi
Symbolic Software • https://symbolic.software
On 4 Jun 2026, at 7:19 PM, John Mattsson <[email protected]>
wrote:
Thanks Nadim!
Great work! Good that we can put this discussion behind us.
"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."
Note that once a CRQC emerges, which some people say may happen very
soon, the X25519 component no longer provides any security, and
ML-KEM becomes a single point of failure in both X25519MLKEM768 and
ML-KEM768. I think formal analysis in the not so distant future
should focus on quantum attackers and treat ECC and RSA as not
providing any security. If people want robustness, the TLS WG should
start working on ML-KEM + HQC-KEM hybrid KEMs [1].
Many TLS libraries enforce handshake timeouts, so unless the key
exchange algorithm is completely broken, an attacker cannot
practically keep a connection open long enough to forge the Finished
message. It is great that TLS WG have clarified that static keys MUST
NOT be used for key exchange. This significantly lower the risk for
these kind of attacks.
Cheers,
John Preuß Mattsson
[1]
https://csrc.nist.gov/csrc/media/Events/2025/workshop-on-guidance-for-kems/documents/papers/ml-kem-is-great-paper.pdf
*From: *Nadim Kobeissi <[email protected]>
*Date: *Thursday, 4 June 2026 at 13:50
*To: *[email protected] <[email protected]>
*Subject: *[TLS] FATT Chance: On the Robustness of Standalone and
Hybrid ML-KEM Key Exchange in TLS 1.3
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 [email protected]
_______________________________________________
TLS mailing list -- [email protected]
To unsubscribe send an email to [email protected]
