[TLS] Re: New Version Notification for draft-usama-tls-risks-of-mlkem-01.txt

[Nadim Kobeissi <[e-mail]>]

Right, and in addition: I honestly don't expect the ProVerif models to show anything crazy.

First, a symbolic tool like ProVerif cannot meaningfully reason about ML-KEM as a primitive beyond the fact that it's a non-commutative KEM, unlike ECDH. Symbolically, a KEM is just encap(ek) -> (ct, ss) and decap(dk, ct) -> ss, with ss an opaque fresh value that stays secret as long as dk does. That abstraction throws away precisely the things that have actually made people nervous about ML-KEM as a primitive: IND-CCA robustness, the FO transform, decapsulation failures, and especially the binding properties (ciphertext/shared-secret and key binding). Those are computational, primitive-level concerns and are invisible to a Dolev-Yao model. This is the same point others have made here: these models assume the primitive is correct and only check that TLS uses it correctly. So a model that treats ML-KEM as an *ideal* KEM will, almost by construction, report that the integration is fine.

Second, a lot of TLS 1.3 is already non-commutative anyway, as noted earlier in this thread: the ML-KEM share of X25519MLKEM768 is a KEM, so any faithful model of the hybrid already has to model encap/decap rather than g^xy = g^yx. So the non-commutativity is not novel to standalone ML-KEM, and "we have never modeled a non-commutative KEM in TLS" isn't quite right since the hybrid forces exactly that!

The consequence is that, by default, a symbolic model will largely *equate* standalone ML-KEM with the hybrid: structurally they're the same KEM feeding the key schedule, modulo one extra concatenated secret. The only way to make the model say something genuinely different is to model the failure scenarios the hybrid was designed for, which we should do:

  1. Component compromise: leak one of the two shared secrets and check that secrecy/authentication survive. The hybrid should survive single-component loss; standalone obviously cannot. (Note this just re-derives "one primitive = one point of failure," which is equally true of standalone X25519, so it does not single out ML-KEM.)

  2. KEM non-binding: give the adversary a rule whereby a crafted ciphertext decapsulates to a known or related shared secret, and check whether transcript agreement and unknown-key-share-style properties still hold. This is the genuinely ML-KEM-specific thing a refined model could surface, because DH's commutative-but-binding structure hides it.

In other words, the value of this exercise lives entirely in those modeling choices, not in the default run. The ProVerif model may well teach us something new (as such models often do) but I expect any surprise to come from the integration details (transcript binding, key schedule, agreement), not from a headline about ML-KEM itself.

And that's the regime where this work is most worth doing. "I expect nothing crazy" is exactly when symbolic re-analysis has historically paid off in TLS 1.3: Selfie on external PSK, the post-handshake authentication and agreement subtleties, the 0-RTT replay framing, all surfaced by someone keeping a current model around and poking the new feature, even when the primitives were boring. A maintained, KEM-capable reftls-style model is infrastructure that pays off on the *next* handshake change too, regardless of whether ML-KEM produces a headline.

So my motivation is simply this: it's good to keep the TLS tradition of giving any major protocol change a symbolic assessment, and to have that certainty on the record. I'll be honest that it's discouraging to see these efforts met by shutting down the conversation rather than engaging with it. A standing ProVerif assessment of significant changes has served this working group well for years, and I'd rather we keep that habit than lose it.

Back to making some hummus...

Nadim Kobeissi
Symbolic Software • https://symbolic.software

> On 29 May 2026, at 4:16 PM, Nathanael Ritz <[e-mail]> wrote:
> 
> Hi,
> 
> Comments below with [NR]
> 
> On Fri, May 29, 2026 at 4:38 AM Muhammad Usama Sardar <[e-mail] <mailto:[e-mail]>> wrote:
> >  Dear Joe and Sean,
> > I believe I have collected sufficient attestations from the WG that a new proof is required for draft-ietf-tls-mlkem.
> > As I understand, apart from me, there are at least 2 other WG participants (Nadim [0] and Nathanael [1]) who are already doing or have volunteered to do independent formal analysis in ProVerif. I take that as a strong attestation that there is enough WG energy to do the work.
> 
> [NR] I stated clearly that “I am interested in collaborating on new ProVerif models that explore PQ crypto as well.” I did not share any opinion on whether a proof was required for anything.
> 
> Based on the results of the idealized KEM model variant (that I remain open to collaborate further on), I found nothing from the verification output that gives me any reason for concern compared to the DH model evaluating the same properties. Of course, critical feedback on my model construction and evaluated properties is welcome off List.
> 
> Since there appears to be an opening for some misunderstanding, please do not misconstrue my contribution as an implied mandate or imposition against the trajectory and current work of the TLSWG by me.
> 
> Sincerely,
> 
> Nathanael
> 
> On Fri, 29 May 2026 at 04:38, Muhammad Usama Sardar <[e-mail] <mailto:[e-mail]>> wrote:
>> Dear Joe and Sean,
>> 
>> I believe I have collected sufficient attestations from the WG that a new proof is required for draft-ietf-tls-mlkem.
>> 
>> As I understand, apart from me, there are at least 2 other WG participants (Nadim [0] and Nathanael [1]) who are already doing or have volunteered to do independent formal analysis in ProVerif. I take that as a strong attestation that there is enough WG energy to do the work.
>> 
>> So with these attestations, I would like to request the initiation of the FATT process for draft-ietf-tls-mlkem. I believe it would be good to have FATT's evaluation of the artifacts that would be eventually developed by these efforts. Thank you for your kind consideration. 
>> 
>> In addition, I believe all concerns have been addressed in this version. Summary of major changes is:
>> 
>> Added justification based on the FATT process: Section 4
>> Reorganization, specially in motivation (Section 1.1)
>> Added some common arguments: Section 6
>> Comparison with hybrid ML-KEM in Section 4.1
>> Clarification of what "breaking" means in Section 3
>> For those who haven't had a chance to check the draft yet, more feedback on Sec. 3 and 4 is very welcome. For discussion of details of modeling, please contact me off-list.
>> 
>> Best regards,
>> 
>> -Usama
>> 
>> [0] https://mailarchive.ietf.org/arch/msg/tls/pZe6luYQeT4GhbOc1FE1xi-Lmzc/
>> 
>> [1] https://mailarchive.ietf.org/arch/msg/tls/S5QioGFa3T3AFWIAjsNg8BFy5Co/
>> 
>> 
>> 
>> 
>> 
>> -------- Forwarded Message --------
>> Subject: 	New Version Notification for draft-usama-tls-risks-of-mlkem-01.txt
>> Date:	Fri, 29 May 2026 03:02:54 -0700
>> From:	[e-mail] <mailto:[e-mail]>
>> To:	Muhammad Sardar <[e-mail]> <mailto:[e-mail]>, Muhammad Usama Sardar <[e-mail]> <mailto:[e-mail]>
>> 
>> A new version of Internet-Draft draft-usama-tls-risks-of-mlkem-01.txt has been
>> successfully submitted by Muhammad Usama Sardar and posted to the
>> IETF repository.
>> 
>> Name: draft-usama-tls-risks-of-mlkem
>> Revision: 01
>> Title: Potential Risks of Standalone ML-KEM in TLS 1.3
>> Date: 2026-05-29
>> Group: Individual Submission
>> Pages: 16
>> URL: https://www.ietf.org/archive/id/draft-usama-tls-risks-of-mlkem-01.txt
>> Status: https://datatracker.ietf.org/doc/draft-usama-tls-risks-of-mlkem/
>> HTML: https://www.ietf.org/archive/id/draft-usama-tls-risks-of-mlkem-01.html
>> HTMLized: https://datatracker.ietf.org/doc/html/draft-usama-tls-risks-of-mlkem
>> Diff: https://author-tools.ietf.org/iddiff?url2=draft-usama-tls-risks-of-mlkem-01
>> 
>> Abstract:
>> 
>> We attest that standalone ML-KEM in TLS 1.3 breaks the existing
>> formal proofs of TLS in state-of-the-art symbolic security analysis
>> tool, ProVerif. In this draft, we show *exactly* where the ProVerif
>> proofs break, namely transition from symmetric DHKE to asymmetric
>> KEM. More specifically, the existing proofs of TLS in ProVerif are
>> based on commutativity property, whereas commutativity does not apply
>> to standalone ML-KEM in TLS.
>> 
>> We also attest that from a formal analysis perspective, this is a
>> much bigger change than RFC8773bis, which indeed went for FATT review
>> (cf. [TLS-FATT]). We, therefore, formally request the chairs to
>> initiate the FATT review of standalone ML-KEM in TLS. A few WG
>> participants have already volunteered to do formal analysis in
>> ProVerif.
>> 
>> This draft also offers some preliminary discussion to help the
>> developers and policy makers make informed choices. Finally, the
>> draft also aims to reduce the endless repitition of arguments from
>> both sides presented on several lists by documenting these arguments
>> so they can simply be referred to.
>> 
>> 
>> 
>> The IETF Secretariat
>> 
>> 
>> _______________________________________________
>> TLS mailing list -- [e-mail] <mailto:[e-mail]>
>> To unsubscribe send an email to [e-mail] <mailto:[e-mail]>
> _______________________________________________
> TLS mailing list -- [e-mail]
> To unsubscribe send an email to [e-mail]