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
> <[email protected]> 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 -- [email protected]
> To unsubscribe send an email to [email protected]
_______________________________________________
TLS mailing list -- [email protected]
To unsubscribe send an email to [email protected]
