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

[Nadim Kobeissi <[e-mail]>]

Hi Usama,

I want to separate the two halves of your reply, because I agree with you on one and respectfully disagree on the other.

On the technical points, I think we've largely converged. You're right that none of the three papers is a symbolic or automated proof of pure ML-KEM. The two pure-ML-KEM results are pen-and-paper computational proofs, not automated. You are also correct in that symbolic and computational analyses complement rather than substitute for each other. I also agree that an automated, maintainable, extensible ProVerif model has value on its own even if the WG decides the computational results are sufficient. That methodological case stands independently of the procedural argument about your draft.

On your specific question: is there a substantive change from draft-ietf-tls-hybrid-design-09 to -16 that would invalidate the Blanchet-Jacomme CryptoVerif proof? I went and checked both versions against the paper. Short answer: no. With respect to the key-schedule integration, the proof carries over:

- BJ model the hybrid integration as a single change to the Handshake-Secret derivation: HS = HKDF-extract(DHE || ss, Derive(ES, label1)), where ss is the KEM shared secret, implemented as a 204-line CryptoVerif file producing DHE || ss. Theorem 3 then assumes only IND-CCA2 of the KEM, plus PQ-PRF for HMAC, PQ-CR for the hash, and classical EUF-CMA for signatures.

- The integration is unchanged from -09 to -16. Section 3.3 and Figure 1 are identical in both versions: concatenated_shared_secret = ss_1 || ss_2, inserted in place of the (EC)DHE secret into the HKDF-Extract that derives the Handshake Secret. That is exactly the construction BJ proved.

- The one substantive delta is Kyber768 -> ML-KEM-768 (FIPS 203). That is a primitive swap. BJ treat the KEM as a black-box IND-CCA2 KEM, so the internal Kyber-vs-ML-KEM differences are invisible to the proof, and ML-KEM-768 satisfies the IND-CCA2 hypothesis Theorem 3 needs. Note that a ProVerif model would be even less precise about this, since primitives are largely black boxes in the symbolic model, and I am 100% certain that the differences between Kyber768 and ML-KEM-768 would be nigh-impossible to capture meaningfully in ProVerif.

- BJ actually anticipated this! Their "Lessons Learned" notes the proof's stability under protocol extension ("all the proof guidance of the previous version carried over to the hybridized version") and states the two conditions the integration must meet: the KEM ephemerals are included in the authenticated data, and the DH and KEM secrets are correctly combined with fixed lengths. Both still hold in -16: key shares remain in the authenticated ClientHello/ServerHello, and fixed-length shared secrets are still mandated.

On the conduct point, I'm not going to withdraw the ask. Usama, I hear your request to drop this, and I respect that you would rather it not overshadow your technical work. I am declining because the climate this sets is bigger than your draft and bigger than you.

You can waive a complaint on your own behalf. You cannot waive it for everyone else, and that is what this is about. My concern was never only that you were the target. It is that a sitting chair of this working group publicly endorsed a post telling a participant in a standards process (one named Muhammad-Usama!!!) to "go work at a Whole Foods or something.” How is that acceptable? What next, will a participant named Ali be publicly derided as needing to go drive an Uber instead after disagreeing with the chairs on signature schemes?

Deirdre liked that post first, followed by many veterans of this TLS WG. The post happened right as Bas’s reply was sent. Whatever its precise referent (and your generous reading of it is characteristic) the effect of a chair amplifying "say something unwelcome here and you should leave the field" is to signal to everyone watching that public ridicule is a sanctioned response from the people who run this group. That chills participation for people far less established and far less gracious than you, whether or not you personally feel chilled.

I also don't accept the "social media is out of scope" framing here. The aim is not to police what anyone likes or posts in general; that is genuinely their business. The point is narrower: chairs are appointed by and accountable to the AD, and a chair's public conduct that signals how dissent will be met bears directly on their ability to chair neutrally and on the health of this WG.

The applicable conduct guideline is RFC 7154 (BCP 54), Guideline 2: "We dispute ideas by using reasoned argument rather than through intimidation or personal attack ... so the rest of the participants who are sitting on the sidelines watching the discussion can form an opinion." A post telling a participant to "go work at a Whole Foods or something" is a personal attack designed to publicly ridicule and discredit specifically targeted individuals, not reasoned argument, and a chair publicly endorsing it is precisely what reaches the people on the sidelines. Guideline 1 asks participants to "extend respect and courtesy to their colleagues at all times ... especially when it is difficult to agree with them."

The relevant standard for the harm is RFC 7776 (BCP 25), Section 2: conduct whose "purpose or effect" is "creating an environment within the IETF that would be intimidating, hostile, or offensive." Note "purpose or effect" -- intent is not the test. To be precise: I am not asserting this clears the formal harassment bar in RFC 7776 (that process is confidential and runs through the Ombudsteam); I am citing the standard, and raising the guidelines matter with the AD, which RFC 7154 Appendix A explicitly contemplates ("report ... to the IETF Chair or the IESG").

On scope: WG chairs are appointed by the AD (RFC 2418), so a chair's public conduct that signals how dissent will be met is squarely the AD's concern, regardless of platform. This is not about policing what anyone likes or posts in general -- that is their business. It is narrowly about chair conduct and the neutrality the role requires.

So I'll restate the ask, decoupled from your draft and from you personally. Deb, one of your chairs is in flagrant violation of RFC 7776 and RFC 7154, and this is creating a chilling effect on discussions in this list. Kindly:

1. Look into the matter.
2. Ask Deirdre to remove the like and to post a brief acknowledgment to this list.
3. Confirm that endorsement of personal attacks on contributors, including via likes on public platforms, is not consistent with the conduct expected of a WG chair.

If we can’t even do that, then this WG is far, far gone.

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

> On 28 May 2026, at 6:24 AM, Muhammad Usama Sardar <[e-mail]> wrote:
> 
> Hi Nadim,
> Thank you for your valuable input. TL;DR is that none of the three papers is symbolic (vs. computational) proof for standalone ML-KEM for TLS. The two papers for standalone ML-KEM are computational proofs. Both symbolic and computational proofs are complementary and not a substitute of each other.
> 
> Social media posts are distraction and out of scope of IETF. So let's please close that topic.
> 
> 
>> 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.
> From my perspective, the key point is that both are computational-level proofs using pen-and-paper. None of them is maintainable and easily extensible if we were to use ML-KEM as a default in the future. 
> 
> More importantly, none of these is symbolic proof. ProVerif can be used for symbolic proof. It also provides an automated way to update the proofs for extensions in the future.
> 
> In any case, it is up to the WG if computational proofs are deemed sufficient.
> 
> Even if they are sufficient, I believe it remains valuable to complement those results with an automated proof in ProVerif.
> 
>> 
>> 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.
> Thanks, that is very helpful. By any chance, could you possibly share your opinion whether there is any substantive change from -09 to -16 that might invalidate that proof in CryptoVerif? If there is no such substantive change, that should already address the concern of folks.
>> 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).
> As a summary, there is no computerized proof for standalone ML-KEM in TLS in the three papers shared, whereas there is computerized (computational) proof for draft-ietf-tls-hybrid-design-09 in CryptoVerif.
> 
> 
>> Secondly, none of these are ProVerif proofs, which I think is what Muhammad is pushing for.
> Exactly, and more broadly computerized proofs at symbolic level which can be updated for future extensions.
>> 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.
> ProVerif and Tamarin are both acceptable tools. This was already clarified by FATT a couple of years ago. In fact, I have exclusively used ProVerif for all the drafts so far. AFAIK, Hannes and Chris also use ProVerif.
> 
> 
>> 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.
> I would note that 'no analysis required' is a perfectly valid output of FATT review. Moreover, FATT output is subject to approval by the WG.
> 
> So FWIW, asking for FATT review is actually harmless.
> 
> 
>> [...] The referents are unambiguous: Muhammad, and Bas's earlier message on this thread. [...]
> First things first. Social media activity is outside the scope of the IETF. Please don't bring anything happening on the social media to the IETF lists. If someone has substantial technical feedback, he can join the list to post or submit to me by email and I would very much welcome that and try my best to address that.
> 
> About the text you quoted, TLS WG is not a "cryptography standards group." The closest I can think of for that post is CFRG. Moreover, to the best of my knowledge, Bas is at Cloudflare and thus not an "academic cryptographer." So I believe you are misunderstanding the social media post.
> 
> Even if you were right, I believe it's perfectly fine if someone somewhere in the world does not like my draft, my formal models, my research work and/or my personal opinions. Given how controversial this topic is, I am not at all surprised by this. Is there someone here who has said something on this topic which has not been refuted? If we were to take into account such social media posts, I believe the whole TLS WG would be at Whole Foods. 🙂
> 
> Since you have mentioned my co-author Bas, there is no conflict between the two of us. While we had differences of opinion, we happily worked together for draft-westerbaan-tls-keyshare and made the substantive change a success. I would take this opportunity to share that yesterday, he shared off-list the new plan for the draft and I supported him in that, and we will most likely work together to proceed that work in the new direction. On the specific issue of ML-KEM, I have added a section based on his concern [0]. If anything, the differences of opinions are because of:
> 
> different backgrounds: he is a cryptographer while I am not. I work at the abstraction of symbolic security analysis (ProVerif). Both are complementary.
> different roles: he is at a company which has a deadline of 2029 for PQ and I totally understand where he is coming from when he is pushing for certain things. I am at a university where my focus is to ensure that we do not miss security flaws in the rush for standardization of PQ.
> It is on record with one of the chairs that I have appreciated working with him. He has been very kind and patient to explain his perspective and cryptographic nits to me, and I am trying to understand his perspective, and we are converging. As you can very well understand, not everything needs to be added in the symbolic model in ProVerif, and reasonable choices have to be made to keep it complementary to computational proof.
> 
> I request that we close this social media topic and keep our focus on the technical matters on list. In particular, I would welcome feedback on [0]. Thank you!
> 
> 
> 
> 
> 
>> Concretely, I would ask the responsible AD to: [...]
> 
> I would like to request to withdraw your ask to the AD. Whatever chair or other WG participants have liked or commented on social media is their personal thing, which has nothing to do with TLS WG. Also, WG participants are still giving their feedback on my draft and I am addressing their feedback. While the discussion is ongoing, I don't see a reason for an escalation to AD.
> 
> 
> 
> 
> Best regards,
> 
> -Usama
> 
> [0] https://muhammad-usama-sardar.github.io/risks-of-mlkem/draft-usama-tls-risks-of-mlkem.html#name-hybrid-ml-kem
> 
> 
> 
> _______________________________________________
> TLS mailing list -- [e-mail]
> To unsubscribe send an email to [e-mail]