Of course, I cannot limit the off-topic discussions, but could we please at least stop repeatedly off-tracking by bringing in hybrid KEMs? Simple reason for this is that that draft has IETF consensus and is in publication queue. Given the consensus, I see absolutely no reason to block that. FATT process was specifically designed to /resolve/ concerns rather than /gatekeeping/.
In contrast, standalone MLKEM has a very different profile with ca. 25 oppositions. FWIW, this is exactly what makes formal analysis necessary to resolve the issue and build high confidence.
So may I kindly ask again to keep the focus of the discussion on standalone ML-KEM?
FWIW, my point is simply: 1. Existing proofs of TLS in ProVerif are based on commutativity (verifiable directly by several links of repos provided) 2. Commutativity does not apply to ML-KEM in TLS and hence, a new proof is required.Updated editor's copy addressing all comments is at [4]. For clarity, I am requesting feedback /only/ on Sec. 3 and 4 in [4]. In simple words, please tell me how to fix the ProVerif proofs preserving the cryptographic /soundness/. Please do not go off-topic. Thank you!
If someone has some comments for other sections, please consider creating an issue or PR here [5] rather than posting in this thread. Thank you! I'll surely try to address your issues later, but please don't distract this discussion.
Some clarifications inline: On 24.05.26 22:26, David Benjamin wrote:
Just to clarify if there was any confusion: the whole bunch of above statements -- including proof via commutativity -- were for existing (DHKE-based) ProVerif models.On Sun, May 24, 2026 at 4:10 PM Eric Rescorla <[email protected]> wrote: On Sun, May 24, 2026 at 12:43 PM David Benjamin <[email protected]> wrote: On Sat, May 23, 2026 at 1:27 PM Ilari Liusvaara <[email protected]> wrote: On Fri, May 22, 2026 at 10:16:07PM +0200, Muhammad Usama Sardar wrote: > > Maybe I should have actually cited the original artifacts by Karthik et al. > Specifically, the point under discussion in Sec. 2.1 of -00 can be seen > exactly in their model [1]. Several years ago I basically started with their > model of draft-20 as a baseline and did the following extensions: > > * fixed the key schedule > * updated to the RFC8446bis > * integrated attestation (such as draft-fossati-tls-attestation) > > I have a hard time convincing myself to attest to "shortcomings" in the > proof models. There /may/ be multiple ways to model and they may /all/ be > correct. My position is that this is correct modeling. At least I don't see > why proof via commutativity is wrong.
The problem with commutativity is that it does not work
with quantum-
safe algorithms[1].
Thanks very much for your attestation to my point.
Neither stand-alone nor hybrid algorithms. The
latter is because it is not sound to argue that the
traditional
component makes hybrids secure.
For instance, it is possible to prove that both MLKEM1024 and
X25519MLKEM768 are sound. However, neither can be proven
in the formal
model.
+1. Commutativity may give a correct proof for /this/ model of
TLS, but that's not relevant here.
The question is whether this model is /useful/ today. Does it
correctly model the scenarios the TLS WG is interested in
today? If it does not, this model is no longer useful because
it cannot answer the questions the WG needs to answer.
When TLS 1.3 was being developed, with classical cryptography,
the answer was yes. Our key agreement primitives were
Diffie-Hellman, so a model that relied on
Diffie-Hellman-specific was useful, and indeed TLS 1.3 got
some mileage out of that work.
But it is not 2018 anymore. Post-quantum primitives, broadly,
do not look like Diffie-Hellman, so a model that relies on
commutativity is clearly no longer useful to this working
group. Such a model /cannot/ say anything about
/either/ MLKEM1024 /or/ X25519MLKEM768. It's not
that MLKEM1024 and X25519MLKEM768 are bad for breaking that
model. The model just doesn't apply anymore. To
/usefully/ model the impacts of /either/ primitive on TLS, we
need a model that starts from an idealized KEM, not an
idealized Diffie-Hellman primitive.
FWIW, it appears to me that we do have some formal verification of
TLS 1.3 with MLKEM:
Huguenin-Dumittan and Vaudenay (TLS 1.3 with pure ML-KEM)
https://eprint.iacr.org/2021/844
Zhao, Jiang, and Zhao (TLS 1.3 with pure ML-KEM)
https://eprint.iacr.org/2024/1360
Blanchet and Jacomme (TLS 1.3 with hybrid)
https://bblanche.gitlabpages.inria.fr/publications/BlanchetJacommeCSF24.pdf
I haven't really read these papers so can't speak to them in
detail. I'd be interested in hearing what other WG members think.
I don't see how "by omission" applies here. From abstract to references, my claims of breaking proofs in the draft are limited to ProVerif and none of these papers are using ProVerif, and using completely different level of abstraction.Ah, nice find! I figured this /must/ exist by now, but wasn't sure. The draft, by omission, implied there wasn't, but /surely/ integrating a key agreement as important as ML-KEM, into a protocol as important as TLS, would have attracted the eye of /some/ formal methods enthusiast by now. :-)
Now, the WG has two plausible directions to go based on this:
1. The WG can decide to defer /both/ drafts on someone
updating this particular model to capture a KEM.
(Non-commutativity applies equally to both.)
In any case, hybrid KEM draft is off-topic.
2. The WG can decide that, even though it no longer has the
input of /this model/, it is sufficiently satisfied
that MLKEM1024 and X25519MLKEM768 are valid integrations of
their respective primitives into TLS.
This seems mostly right to me. I suppose it's possible we might
have an analysis that demonstrated that TLS 1.3 with hybrids no
matter what the status of MLKEM, in which case we would have
confidence in the absence of a CRQC. I'm not quite sure how one
would phrase this, perhaps that the attacker gets to supply both
MLKEM shares and the output secret?
Sure. It /is/ conceivable that we:- Are confident that /if X25519 is secure/, TLS 1.3 with X25519MLKEM768 is secure - Are /not/ confident that /if ML-KEM-768 is secure,/ TLS 1.3 with X25519MLKEM768 is secureBut I don't think that situation should be good enough for X25519MLKEM768. I mean, the whole point of X25519MLKEM768 is to incorporate ML-KEM. We're burning a whole kilobyte of ClientHello to do it. If we aren't even satisfied that we integrated ML-KEM correctly, what are we even doing here? The bar for /either/ draft-ietf-tls-ecdhe-mlkem or draft-ietf-tls-mlkem should include being satisfied in the ML-KEM integration.
Seems irrelevant to the requested feedback
I am currently unconvinced by the (mostly off-topic) points made so far, as none of that fixes the proofs.(To be clear, I think we solidly meet that bar, so this is all moot.
Just that, even if we didn't, it would still not be a reason to artificially separate the drafts.)
I am really very lost now. You were the one who said you do not support draft-usama-tls-fatt-extension because of ML-KEM [2]. Now that I have separated it, you seem to have concern on separation. What am I missing here? Could you please clarify?
If you truly believe more modeling is needed, rather than trying to selectively delay only one of two applicable drafts with circuitous discussion, I'd encourage you to apply your formal methods expertise to update those models. Whether the outcome is a updated model that checks out, or a concrete problem with (1) and (2), I think either results would be quite valuable.Thank you for your encouragement. Do you /really/ think that if I had the expertise or if it were so easy for me, I would not have done that by now and instead put up a draft for discussion or ask for permission to talk to FATT? At the risk of endlessly repeating, I am counting on Karthik et al.'s model as the basis, and this commutativity comes directly from that. I don't currently know how to properly fix it for KEMs in a way that preserves the /soundness/ from a cryptographic perspective. Since he is in FATT, either I may be allowed to talk to him, or maybe chairs can ask him to suggest a fix.
Keep in mind that /none/ of these modeling exercises have
anything to do with the security of ML-KEM as a KEM, or of
X25519 as a Diffie-Hellman primitive. No model of this form
will say anything useful about them. They start by assuming
the primitives are correct and checks if TLS used them right.
Questions of /whether/ ML-KEM is a secure KEM need to analyze
the primitive itself, such as what was done throughout the
NIST process. That means this entire discussion of formal
methods has nothing to do with the question of whether or
hedge ML-KEM with an existing, known-quantum-vulnerable algorithm.
This seems like the key point. Most of the concerns I have seen
raised about pure MLKEM are about the strength of the primitive,
not about its TLS integration.
And with the recent 2029 target, things are already highly
critical.
Best regards, -Usama [0] https://github.com/tlswg/tls-fatt#working-group-last-call-wglc [1] https://github.com/muhammad-usama-sardar/tls-fatt-extension/issues/17 [2] https://mailarchive.ietf.org/arch/msg/tls/V_fN1BNpGR2rBox48tYiAMHzy80/[3] https://muhammad-usama-sardar.github.io/risks-of-mlkem/draft-usama-tls-risks-of-mlkem.html#name-urgency
[4] https://muhammad-usama-sardar.github.io/risks-of-mlkem/draft-usama-tls-risks-of-mlkem.html
[5] https://github.com/muhammad-usama-sardar/risks-of-mlkem
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
