Analysis of Hybrid Key Exchange and Standalone ML-KEM in TLS 1.3

Internet-Draft	Analysis of Hybrid Key Exchange and Stan	June 2026
Sardar	Expires 13 December 2026	[Page]

Abstract

The draft presents symbolic and computational analysis of hybrid key exchange and standalone ML-KEM. In our observation, we believe that hybrid key exchange is preferable over standalone ML-KEM until a powerful CRQC exists which breaks all the bits of pre-quantum. This draft also offers opinions of the IETF participants and some preliminary discussion to help the developers and policymakers make informed choices. Finally, it offers minimal implementation guidance for hybrids.¶

1. Introduction

Readers are assumed to be familiar with [NistFips203], [I-D.ietf-tls-rfc8446bis], and [I-D.ietf-tls-mlkem]. Please note that the draft has currently several hyperlinks.¶

1.1. Objectives

The draft serves three objectives:¶

Summary of formal methods (symbolic and computational) works for hybrid key exchange and standalone ML-KEM¶
Capturing the opinions of the IETF participants to avoid repetition¶
Minimal implementation guidance for hybrids¶

1.1.1. Summary of Formal Methods Works

The draft covers the formal methods for the security considerations of [I-D.ietf-tls-mlkem]. This includes symbolic and computational analysis (to be interpreted as in SoK) of integration of standalone ML-KEM in the context of TLS. Specifically, it covers the formal analysis [FATT-CHANCE] in ProVerif on the potential issue of asymmetry. The analysis confirms that asymmetry is not a problem.¶

1.1.2. Capturing the Opinions of IETF

The draft also aims to reduce the endless repetition of arguments from both sides presented on several lists by documenting these arguments so they can simply be referred to. This draft captures what we understand them to be saying. The goal is that people can be a bit more fair and balanced to acknowledge others' opinions, rather than stating their opinion as universal truth, or else present substantial scientific evidence if they claim their opinion to be universal truth. In our understanding, the question largely boils down to: whether the traditional or post-quantum cryptographic primitive breaks first?¶

1.1.3. Minimal Implementation Guidance for Hybrids

The implementation concern is not only whether ML-KEM is secure as a primitive, but whether a TLS deployment can show that both hybrid components were validated, transcript-bound, and fail-closed under the negotiated group.¶

1.2. Motivation

[rfc3552] requires to document the risks in the security considerations. To support those requirements for [I-D.ietf-tls-mlkem], this draft aims to formally study the security of standalone ML-KEM in TLS 1.3.¶

1.3. Intuition

Leaking out the ECDHE key from hybrid key exchange should downgrade the security to the level of a standalone ML-KEM. Therefore, hybrid key exchange is in general more secure, unless:¶

ECDHE is fully broken, in which case it still falls equivalent to standalone ML-KEM,¶
in the hypothetical scenario that there is an implementation bug in the ECDHE part which is triggered only in composition. We have not yet seen any concrete evidence of such a scenario on the list.¶

We believe that in general:¶

1. Migration from ECDHE to hybrid key exchange is security improvement.
2. Migration from hybrid key exchange to standalone ML-KEM is security
regression, unless CRQC exists to break all ECC keys.

1.3.1. Expected Learning

We believe formal methods can provide additional value for security considerations of this draft in order to maintain the high cryptographic assurance of TLS.¶

Since we have no guarantee on whether ECDHE will break before ML-KEM,
it seems appropriate to do thorough cryptographic analysis.
We believe the Harvest Now, Decrypt Later (HNDL) attack applies
equally well to standalone ML-KEM.

Adversary can record all traffic and decrypt it when ML-KEM is broken. The opinions of WG participants here vary from "ML-KEM is secure" to "ML-KEM is probably already secrectly broken." Formal methods can operate under the assumption that ML-KEM is secure, and focus on the integration of ML-KEM in TLS under this assumption.¶

As an example, formal methods can help justify design choices, such as the preference for hybrid key exchanges. It can also help identify all the assumptions under which the properties hold.¶
As a relevant data point in the context of standardization, LAKE WG has done formal analysis for EDHOC-PSK with KEM (ref).¶
Computational analysis (cf. SoK) -- using tools such as CryptoVerif -- seems like a reasonable approach to ensure security of ML-KEM in TLS, such as binding shared secret ss to the TLS transcript hash.¶

We believe that the focus of symbolic analysis ought to be on the
*integration* details (transcript binding, key schedule, agreement)
for standalone ML-KEM in the context of TLS, rather than the
*primitive* itself.

2. Conventions and Definitions

The key words "MUST", "MUST NOT", "REQUIRED", "SHALL", "SHALL NOT", "SHOULD", "SHOULD NOT", "RECOMMENDED", "NOT RECOMMENDED", "MAY", and "OPTIONAL" in this document are to be interpreted as described in BCP 14 [RFC2119] [RFC8174] when, and only when, they appear in all capitals, as shown here.¶

Symbolic analysis: see SoK ¶
Computational analysis: see SoK ¶
Standalone ML-KEM refers to [I-D.ietf-tls-mlkem].¶
Hybrid key exchange refers to [I-D.ietf-tls-ecdhe-mlkem] and [I-D.ietf-tls-hybrid-design].¶

We believe that symbolic and computational models are complementary and not a substitute of each other.¶

2.1. Key Exchange and Key Encapsulation

In traditional key exchange (DHKE), both endpoints send their public key shares g^x and g^y to derive a shared secret g^xy.¶

In key encapsulation, there is essentially only one endpoint (say client) which generates the key pair (dk,ek) where dk represents the secret decapsulation key and ek represents the public encapsulation key. In a KEM, only one of the endpoints (client in above example) sends the public encapsulation key ek and the peer (server) sends a ciphertext ct.¶

4. Symbolic Analysis

For brevity, we omit other assumptions in the properties below and focus on the difference. This assumes hybrid constructor to be secure.¶

4.1. Minimum Viable Modeling

Based on the discussion on list, simply replacing ideal DHKE by ideal ML-KEM in the formal model is not very useful. We ought to focus on the more security-critical questions about integration of ML-KEM in TLS. We present a few high-level observations to consider for security considerations of [I-D.ietf-tls-mlkem]:¶

The model ought to consider that any agent could have initiated the TLS, rather than assigning the agents with static roles of client and server in the model. When agents are assigned non-static roles, it would be interesting to see whether the asymmetry issue becomes visible in some property. We consider it very critical for security considerations of [I-D.ietf-tls-mlkem] and this is the key point of this draft.¶
Different failure modes proposed on list can be modeled.¶
A large part of the problem is the careful investigation of what to model, under what threat model, under what system model, under what implementation scenarios etc. We believe some of this is important for security considerations of [I-D.ietf-tls-mlkem].¶
It will be interesting to see some analysis about any subtle cases where hybrid key exchange in TLS is not at least as good as standalone ML-KEM in TLS. Our understanding is that some participants would like to see some statement on the comparison since hybrid key exchange is the de facto industry standard.¶
We believe brainstorming about some robustness (vs. security) properties would also be useful. Even if the security properties hold, does standalone ML-KEM make side-channel leakage easier? This might be a valuable consideration for the implementers.¶
Analysis may be helpful to ensure that the changes -- such as the removal of hash function (cf. Appendix C.1, bullet 3 in [NistFips203]) -- from Kyber to ML-KEM preserve the security proofs of Kyber.¶

Any analysis on these or related security and robustness matters is very welcome.¶

4.2. Hybrid Key Exchange

Hybrid key exchange still maintains the DHKE part. From formal (symbolic) analysis perspective, g^x and g^y are still sent in hybrid key exchange, g^xy is still computed and we believe the commutativity property is applicable for that part as-is. From formal (symbolic) analysis perspective, ML-KEM is complementary to that.¶

Specifically, from Section 4 of [I-D.ietf-tls-ecdhe-mlkem], for the symbolic analysis, X25519MLKEM768 in TLS may be viewed as:¶

client's key_exchange value = ek || gx
server's key_exchange value = ct || gy
shared secret = ss || gxy

Formally, the property hybrid key exchange provides is:¶

Security properties of TLS hold unless *both* `gxy` and `ss` are
available to the adversary.

As presented in Section 3.1, hybrid key exchange preserves ECDHE component gxy, and concatenates ML-KEM component ss as an additional factor. So as long as at least one of these two secrets is not available to the adversary, all security properties should hold. In particular, even if ML-KEM is completely broken, i.e., ss is available to the adversary, the protocol retains the security level of ECDHE.¶

4.3. Standalone ML-KEM

On the other hand, the formal property standalone ML-KEM provides is:¶

Security properties of TLS hold unless `ss` is available to the
adversary.

4.4. Results

For the FATT process [TLS-FATT], the symbolic analysis [FATT-CHANCE] was done in ProVerif by Nadim Kobeissi, who concludes:¶

The hybrid neutralizes every weakness standalone ML-KEM carries,
both the confidentiality single point of failure and the
authentication (key-confirmation) failure that rides along
with it, by demanding that both of its components fail at once;
and moving from today’s classical (EC)DHE to a hybrid never gives
up ground, because the classical guarantee survives intact inside
the combination. That is the precise sense in which the hybrid
strictly dominates standalone.

None of this says standalone ML-KEM is broken. Under its stated
assumption, that ML-KEM holds, it is secure under our models.
The argument against it is one of robustness, not of any
present-day attack: it stakes everything on a single, relatively
young assumption, where the hybrid keeps a mature fallback in
reserve. For a deployer who cannot afford to be wrong about
lattice cryptography for the lifetime of the data being protected,
that distinction is the whole game. The two caveats bound the
picture honestly: reuse is a real and quantifiable cost rather
than a catastrophe, and the role-asymmetry worry, while genuinely
the draft’s headline concern, did not surface as a distinct
vulnerability in the server-authenticated, one-initiator-per-session
setting analyzed here.

Results confirm integration of KEM in TLS is secure as long as the primitive itself is secure. In our understanding, results also imply a clear preference for hybrids under the Dolev-Yao model, in the sense that if the shared secret from ML-KEM becomes available to the adversary (for example, due to implementation bug), both confidentiality and authentication are broken in standalone ML-KEM, whereas under same condition, both confidentiality and authentication still hold as long as (EC)DHE is still not available to the adversary. We believe this applies until a powerful CRQC exists which breaks all the bits of pre-quantum, where the condition of (EC)DHE being available to the adversary is violated.¶

The artifacts are available here for independent review.¶

5. Implementation-Facing Negative Cases

The formal analysis above is not an implementation test suite and does not replace protocol conformance testing. However, a short set of negative cases can help implementers check that the intended hybrid binding property is reflected in their APIs, transcript handling, and key schedule integration.¶

In particular, implementations of hybrid key exchange ought to reject, or fail safely on, cases such as the following:¶

malformed or missing shares: The negotiated group is a hybrid group, but one component of the peer key share is missing, malformed, or associated with a different group.¶
mixed transcript context: The ECDHE and KEM values are individually well-formed, but assembled from different handshakes, transcript contexts, or negotiated groups.¶
fallback after hybrid negotiation: A peer attempts to continue the handshake as standalone ECDHE or standalone ML-KEM after a hybrid group was negotiated.¶
premature secret derivation: Application traffic secrets are derived before both hybrid components have been validated and accepted under the negotiated group.¶
API/logging ambiguity: Exported state, logs, traces, or implementation APIs make a hybrid exchange appear as if only one component was used or accepted.¶

These cases are not intended to create a new formal proof obligation. They are implementation-facing checks that help bridge the formal "both components are bound and accepted" property to concrete failure modes that implementations can accidentally mishandle.¶

5.1. Argument Matrix for Implementation Review

The discussion above can be read as an argument matrix for implementers and reviewers. The point is not to resolve every policy preference in this document, but to make each recurring argument map to a concrete review question.¶

Table 1
Argument	Implementation-facing review question	Why it matters
Hybrid key exchange retains two components.	Does the implementation make it clear that both the ECDHE and ML-KEM components were present, validated, and bound to the same negotiated group and transcript?	Otherwise a successful handshake may not actually reflect the formal "both components are bound and accepted" property.
Standalone ML-KEM has a single KEM shared secret.	Are failures in encapsulation, decapsulation, transcript binding, and key-schedule input handled as fail-closed errors rather than as retry or fallback paths?	A standalone construction has no second key-exchange component to preserve confidentiality if the ML-KEM path is mishandled.
Hybrid fallback is useful only when it is explicit.	After a hybrid group is negotiated, can either endpoint silently continue as standalone ECDHE or standalone ML-KEM?	Silent continuation changes the negotiated security property and makes interop failures hard to distinguish from downgrades.
Cost claims are deployment-dependent.	Are claimed savings measured separately for wire bytes, CPU, memory, latency, code complexity, and operational rollout?	Treating "cost" as a single value can hide whether a deployment is trading away cryptographic robustness for a negligible or unmeasured gain.
Formal models do not cover every implementation interface.	Do APIs, logs, exported state, and test harnesses expose enough detail to show which component failed or succeeded?	Reviewers need observable evidence that the implementation behavior matches the protocol-level claim.

This matrix is deliberately small. It is intended to help a reviewer decide whether a concrete implementation or deployment argument belongs in the formal-methods discussion, in implementation guidance, or in a separate operational cost analysis.¶

6. Issues That Formal Methods Probably Cannot Solve

The answers to the following issues are largely dependent on several factors, and the opinions vary largely.¶

It is necessary to mention that even several respectable cryptographers in the community are not aligned on the issue -- for example see the long bet. Hence, our personal opinion is probably not that important. Probably the best we can do is to capture our understanding of the views of WG participants.¶

Disclaimer: This is not meant to be an exhaustive list.
This is also not meant to pritoritize any concerns over others.
This is a sincere attempt to slowly capture the opinions
to avoid endless repetitions from both sides.
Some substantive concerns may be missing.
If your substantive concern is missing, it is unintentional.
Please simply submit a *precise* and *concise* PR, preferably
with a reference.

6.1. Which breaks first: ML-KEM-768 or X25519?

In our understanding, the key open question boils down to:¶

Which of the two cryptographic mechanisms breaks first?
How does that relate to the CRQC being developed?
How many bits of pre-quantum cryptography can that CRQC actually
break?
Since all of three can be kept secret for some time,
the opinions vary a lot on the different possible combinations.

6.2. Does CRQC Break All Bits of Pre-quantum?

Some participants believe that CRQC will break all bits of pre-quantum cryptographic, while some others believe that it will break only a few bits.¶

6.3. Policy/Regulations

Some countries have a regulatory preference for hybrid key exchange.¶

6.4. Recommendation of Designers

The authors of Kyber/ML-KEM (see this) say:¶

For users who are interested in using Kyber, we recommend the
following:

* Use Kyber in a so-called hybrid mode in combination with
established "pre-quantum" security; for example in combination
with elliptic-curve Diffie-Hellman.
[...]

A WG participant shares that:¶

I recently asked one of the members of the CRYSTALS team
whether this is still his view, and the response was:
"Yes, of course."

6.5. Thorough Review

Please see a very thorough review here, which is self-sufficient.¶

6.6. 'Significantly Harder' Argument

Some participants believe in the 'significantly harder' argument, which assumes independence of breakage of ML-KEM and traditionals:¶

If the probablity of one being broken over the next n years is p, and
the probability of the other being broken over the next n years is q,
then the probability of both being broken is pq.

Please see this for what "broken" may mean here modulo some exclusions.¶

Given the very different type of cryptographic constructions involved, independence might be a reasonable assumption. However, some participants disagree with 'significantly harder' argument with a reasonable counter-argument that in reality, cryptography is much more complicated than that (cf. this):¶

Depending on the algorithms and the composition method,
the probability can clearly be q, or smaller than pq.

In our understanding, most other counter-arguments seem to break the exclusions.¶

Please note that this argument is based on the security of primitives, rather than the composition of primitives in protocols. Hence, formal methods probably have nothing to help here.¶

6.7. Urgency

It is unclear whether and if applicable when Cryptographically-Relevant Quantum Computer (CRQC) will eventually become practical. The opinions vary from never because of complicated physics (see this) to be prepared for it as early as 2029 (see Google 2029 and Cloudflare 2029). Technically, please note that Google has not even released the quantum circuit underlying their recent claims -- apparently the reason for this urgency. So Google's claims may not yet be justified.¶

Moreover, in our understanding, these deadlines are for PQ-based protection in general regardless of hybrid key exchange or standalone KEMs in TLS. Since hybrid key exchange is wildly in use, these deadlines are mainly for quantum-safe authentication.¶

In any case, some participants see no reason to create panic for publication of [I-D.ietf-tls-mlkem] based on this because many implementations -- such as OpenSSL -- have already implemented standalone ML-KEM, and it is just a matter of enabling it. And frankly, nobody needs permission from the IETF to enable it.¶

6.8. "Cost"

"Cost" has been presented on the list as the motivation for standalone ML-KEM in TLS but we have not seen any supporting analysis. Our observation from Section 4 of [I-D.ietf-tls-ecdhe-mlkem] is that -- for example -- for X25519MLKEM768, the traditional part seems negligible compared to ML-KEM part in key_exchange:¶

Table 2
Bytes in field	PQ part (ML-KEM)	Traditional part (X25519)
Client share	1184	32
Server share	1088	32

We believe other "costs" will depend on several factors -- including but not limited to implementation details and deployment scenario -- and it is quite subjective.¶

There seems to be a need for a thorough study to understand the "cost." We invite the WG participants to perform cost analysis and share the results with the WG.¶

6.9. Is Publication Necessary?

Code Points for ML-KEM have already been assigned. [I-D.barnes-tls-this-could-have-been-an-email] provides detailed rationale as to why publication of such documents and the debates around that may be unnecessary. In our understanding, [I-D.pwouters-crypto-current-practices] makes similar arguments.¶

[I-D.ietf-tls-mlkem]: Connolly, D., "ML-KEM Post-Quantum Key Agreement for TLS 1.3", Work in Progress, Internet-Draft, draft-ietf-tls-mlkem-07, 12 February 2026, <https://datatracker.ietf.org/doc/html/draft-ietf-tls-mlkem-07>.
[I-D.ietf-tls-rfc8446bis]: Rescorla, E., "The Transport Layer Security (TLS) Protocol Version 1.3", Work in Progress, Internet-Draft, draft-ietf-tls-rfc8446bis-14, 13 September 2025, <https://datatracker.ietf.org/doc/html/draft-ietf-tls-rfc8446bis-14>.
[NistFips203]: "Module-lattice-based key-encapsulation mechanism standard", National Institute of Standards and Technology (U.S.), DOI 10.6028/nist.fips.203, August 2024, <https://doi.org/10.6028/nist.fips.203>.
[RFC2119]: Bradner, S., "Key words for use in RFCs to Indicate Requirement Levels", BCP 14, RFC 2119, DOI 10.17487/RFC2119, March 1997, <https://www.rfc-editor.org/rfc/rfc2119>.
[RFC8174]: Leiba, B., "Ambiguity of Uppercase vs Lowercase in RFC 2119 Key Words", BCP 14, RFC 8174, DOI 10.17487/RFC8174, May 2017, <https://www.rfc-editor.org/rfc/rfc8174>.
[TLS-FATT]: IETF TLS WG, "TLS FATT Process", June 2025, <https://github.com/tlswg/tls-fatt>.

9.2. Informative References

[FATT-CHANCE]: Kobeissi, N., "FATT Chance: On the Robustness of Standalone and Hybrid ML-KEM Key Exchange in TLS 1.3", Cryptology ePrint Archive, Report 2026/1147 , 2026, <https://eprint.iacr.org/2026/1147>.
[I-D.barnes-tls-this-could-have-been-an-email]: Barnes, R., "Stop Doing Cryptographic Algorithm Drafts when Email to IANA is All You Need", Work in Progress, Internet-Draft, draft-barnes-tls-this-could-have-been-an-email-00, 23 February 2026, <https://datatracker.ietf.org/doc/html/draft-barnes-tls-this-could-have-been-an-email-00>.
[I-D.ietf-tls-ecdhe-mlkem]: Kwiatkowski, K., Kampanakis, P., Westerbaan, B., and D. Stebila, "Post-quantum hybrid ECDHE-MLKEM Key Agreement for TLSv1.3", Work in Progress, Internet-Draft, draft-ietf-tls-ecdhe-mlkem-05, 26 May 2026, <https://datatracker.ietf.org/doc/html/draft-ietf-tls-ecdhe-mlkem-05>.
[I-D.ietf-tls-hybrid-design]: Stebila, D., Fluhrer, S., and S. Gueron, "Hybrid key exchange in TLS 1.3", Work in Progress, Internet-Draft, draft-ietf-tls-hybrid-design-16, 7 September 2025, <https://datatracker.ietf.org/doc/html/draft-ietf-tls-hybrid-design-16>.
[I-D.ietf-tls-hybrid-design-09]: Stebila, D., Fluhrer, S., and S. Gueron, "Hybrid key exchange in TLS 1.3", Work in Progress, Internet-Draft, draft-ietf-tls-hybrid-design-09, 7 September 2023, <https://datatracker.ietf.org/doc/html/draft-ietf-tls-hybrid-design-09>.
[I-D.pwouters-crypto-current-practices]: Wouters, P., "Current practices for new cryptography at the IETF", Work in Progress, Internet-Draft, draft-pwouters-crypto-current-practices-00, 3 November 2024, <https://datatracker.ietf.org/doc/html/draft-pwouters-crypto-current-practices-00>.
[I-D.usama-tls-fatt-extension]: Sardar, M. U., "Extensions to TLS FATT Process", Work in Progress, Internet-Draft, draft-usama-tls-fatt-extension-07, 2 May 2026, <https://datatracker.ietf.org/doc/html/draft-usama-tls-fatt-extension-07>.
[rfc3552]: Rescorla, E. and B. Korver, "Guidelines for Writing RFC Text on Security Considerations", BCP 72, RFC 3552, DOI 10.17487/RFC3552, July 2003, <https://www.rfc-editor.org/rfc/rfc3552>.