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

[Nadim Kobeissi <[e-mail]>]

Hi everyone,

I’ve spent the past hour or so digging into this discussion, and have what I hope are a few key substantive points I’d like to contribute as someone who previously worked on the formal analysis of TLS 1.3 in ProVerif. While I have three points, unfortunately, one of them is about conduct from a WG chair (I’ll leave that one for last).

First off, I’d like to weigh in on the papers that Eric cited, since their relevance insofar as they contribute to formal modeling and analysis of pure ML-KEM TLS 1.3 has been discussed. It is worth being specific about what each one actually shows:

1. Huguenin-Dumittan & Vaudenay (eprint 2021/844). This is a pen-and-paper game-based proof, not automated verification model, which I think is what the FATT is mainly concerned with. The main theorem shows the TLS 1.3 handshake with the DH key exchange replaced by a KEM is secure in the Dowling et al. MultiStage model whenever the KEM is OW-CPA. ML-KEM, being IND-CCA, trivially satisfies this. The authors themselves note the resulting bound is "very much non-tight," and QROM is left as an open problem. Effectively, this is qualitative reassurance for pure-KEM TLS 1.3, not a tight practical bound.

2. Zhao, Jiang & Zhao (eprint 2024/1360) closes both of those gaps: the paper tightens the ROM bound from O(q^6) to O(q) (O(1) for rigid D-OW-CPA KEMs like NTRU and Classic McEliece), and provides the first QROM proof. CRYSTALS-Kyber (= ML-KEM-PKE) is the named instantiation. This is still pen-and-paper, but this is the closest thing that seems to have been cited so far to a tight, QROM-valid computational analysis of pure-KEM TLS 1.3.

3. Blanchet & Jacomme (CSF ’24) is actually a mechanized CryptoVerif proof of draft-ietf-tls-hybrid-design-09 (the X25519+MLKEM hybrid draft) under post-quantum sound semantics the authors had to develop for the tool. Theorem 3 establishes forward secrecy of hybrid TLS 1.3 against quantum attackers under PQ-IND-CCA2 of the KEM, PQ-PRF for HMAC, PQ-CR for the hash, and classical EUF-CMA for signatures.

So, Eric's framing appears to be correct, as far as I can tell: pure-KEM TLS 1.3 is covered by (1) and (2), and the hybrid is mechanically verified by (3).

Secondly, none of these are ProVerif proofs, which I think is what Muhammad is pushing for. Separately from the merits of any specific draft, the broader symbolic verification literature for TLS 1.3 does have a real gap: existing ProVerif models bake DH commutativity equations into the primitive layer, so they cannot speak to KEM-based key exchange, pure or hybrid. Now, of course, you can choose to simply not care about ProVerif models, or, say, prefer Tamarin models, that’s your prerogative! But if you think ProVerif models are worth anything, then updating those models with an idealized-KEM abstraction is legitimate, useful work, and contributions on that front would be welcome from anyone willing to do them.

To be clear about my own view: Muhammad's advocacy has been argued in a way that conflates "the model no longer applies" with "the protocol is risky," and uses procedural levers (FATT) asymmetrically across the standalone and hybrid drafts, points that David, Ilari, Ekr, Mattsson, and Bas have already addressed at length. But the underlying methodological request, a KEM-aware ProVerif model of TLS 1.3, is independently legitimate, and dismissing this along with the framing is mistaken and illegitimate on its own. What I’m saying is that we can reject the procedural argument while welcoming the modeling work.

Thirdly,  I also have to raise something this list has not registered, though many people on this list have seen it. While this thread was active, Thomas Ptacek posted on Bluesky:

  "If I was participating in a cryptography standards group and said
   something that caused an academic cryptographer to vocally question
   their support of formal methods, I would immediately take a 3 year
   sabbatical from computers and go work at Whole Foods or something.”
— https://bsky.app/profile/sockpuppet.org/post/3mmpcnwd5ss2c 

The referents are unambiguous: Muhammad, and Bas's earlier message on this thread. My problem is that a chair of this working group then publicly liked that post (and in fact was the first to like the post), followed by many long-standing participants on this mailing list.

I want to be precise about what I am and am not raising. I am not asking that anyone be sanctioned for what Ptacek wrote, as he is not an IETF participant and his post is his own. I am asking the AD, as someone who has been often the victim of exactly this type of intimidation, bullying and abuse, to address what it means for a sitting WG chair to publicly endorse, via a named account on a public platform, a post that tells a list participant to leave the field and instead go work at a grocery store. By any plain reading, the Bluesky post is a personal attack on a contributor that does not engage their argument. A chair amplifying it is unacceptable.

Muhammad's arguments have already drawn detailed pushback from people with significantly more institutional standing in this WG, and that pushback was the right way to engage him. Mockery from outside the WG, endorsed by a chair and then by many veterans of this list, is a different thing, and the people watching whether IETF participation is safe for them include people we want here. The signal that gets sent to a junior researcher, a non-Western contributor (as Muhammad clearly is), or anyone making contentious arguments is that public ridicule is an available response from WG leadership. That is not a signal this group should be sending.

Concretely, I would ask the responsible AD to:

1. Make a clear public statement that endorsement of personal attacks or statements intended to publicly humiliate contributors, including via likes on social platforms, is not consistent with the conduct expected of WG chairs.

2. Ask the chair in question to undo the like and post a brief acknowledgment to this list.

3. Consider whether the appearance of impartiality has been sufficiently affected that recusal from procedural rulings on draft-usama-tls-risks-of-mlkem, and on any FATT review requests originating from the same author, is warranted.

Thank you,

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

> On 25 May 2026, at 5:29 PM, Muhammad Usama Sardar <[e-mail]> wrote:
> 
> Thanks Simon, Bas, and Uri for your inputs. Please see inline:
> 
>> Muhammad Usama Sardar <[e-mail]> <mailto:[e-mail]> writes:
>> 
>>> 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.
>> I find the above a good summary of the situation, and I worry that this
>> concern get lost in this thread.
>> 
>> Introducing ML-KEM in a way that breaks our formal analysis of TLS seems
>> like a serious problem to me.
>> 
>> Is this a fatal problem with the ML-KEM proposal?
> Unfortunately, it's a very hard question for me and I can't answer that until I have eithera security proof or an impossibility proof. I currently have neither of those.
> 
> All I can attest to at this moment is that it breaks the current ProVerif proofs. I can add a bunch of nits on top in the draft but I am not sure that is useful right now because the top-level issue of commutativity is unresolved. In particular, I haven't seen anyone proposing a fix to the problem highlighted in Sec. 3 [0].
> 
>>   Is there some hope
>> that an modified formal proof can be developed?
> There certainly is.
>>   Substantial
>> contributions to the latter effort seems appropriate here.
> Any contribution to new proof is very welcome.
> 
> 
> 
> 
>> I did not see any rebuttal of the salient point that any such gap would apply to X25519MLKEM768 too.
> Addressed in [1].
> 
> 
> 
> 
>> This is a fatal problem with your formal analysis  - so, the formal analysis here is what requires fixing.
> Thank you for yet another attestation to my point that the existing formal analysis needs to be fixed.
> 
> Best regards,
> 
> -Usama
> 
> [0] file:///home/usama/gitRepos/risks-of-mlkem/draft-usama-tls-risks-of-mlkem.html#section-3
> 
> [1] https://mailarchive.ietf.org/arch/msg/tls/NTGubqR_wSygwxX4_6_yCAhiw4s/
> 
> 
> 
> _______________________________________________
> TLS mailing list -- [e-mail] <mailto:[e-mail]>
> To unsubscribe send an email to [e-mail] <mailto:[e-mail]>