Only on the point of conduct: Working group chairs are not required to sacrifice their personal lives or personal opinions to serve. There is no requirement for separate email addresses. What they and others do in their personal time, outside the boundaries of the IETF (mail lists, meetings) is their own business and is not subject to the Code of Conduct (RFC 7154).
Any further discussion on this topic should be moved to a separate message chain, so as to not disrupt actual working group business on this one. Deb Cooley Sec AD On Thu, May 28, 2026 at 5:36 AM Nadim Kobeissi <[email protected]> wrote: > 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: > > 1. different backgrounds: he is a cryptographer while I am not. I work > at the abstraction of symbolic security analysis (ProVerif). Both are > complementary. > 2. 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] >
_______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
