[TLS] Re: WG Last Call: draft-ietf-tls-mlkem-08 (Ends 2026-07-08)

[Nadim Kobeissi <[e-mail]>]

Hi Sean,

I apologize, I only saw your emails after I sent my most recent one. I wrote it on my phone while walking my dog and this didn’t read the thread in its entirety until after I had sent it. I did not mean to ignore your recommendations.

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

> On 28 Jun 2026, at 9:46 PM, Sean Turner <[e-mail]> wrote:
> 
> AGAIN!!!!
> 
> Let’s stick to the consensus call, "I support" or do "I do not support" as was requested in the email that began this thread.
> 
> I will, again, repeat the reminder, about conduct:
> 
> Conduct Reminder: Given the heated nature of previous discussions on this topic, participants are strongly reminded to adhere to the IETF Code of Conduct (BCP 54) and the TLS WG's Mail List Procedures. Keep feedback professional, technical, and focused on the document's text.
> 
> For the TLS Chairs,
> spt
> 
>> On Jun 28, 2026, at 15:42, Muhammad Usama Sardar <[e-mail]> wrote:
>> 
>> Hi D. J. Bernstein,
>> 
>> I'd be happy if you could show me a concrete attack on the integration of ML-KEM in TLS that I can double-check in ProVerif, rather than referring to older attacks or complaining about absence of details in ProVerif. I'll try my best to put in all the details in ProVerif that you want. Please keep your email response focused on exactly that rather than what chairs or others did. Thank you!
>> 
>> If you don't show me a concrete attack, I'll not respond because there is no actionable gap for us to model since the combination of symbolic and computational proof provides sufficient coverage.
>> 
>> 
>> 
>> 
>> On 28.06.26 19:46, D. J. Bernstein wrote:
>>> Muhammad Usama Sardar writes:
>>>> D. J. Bernstein wrote:
>>>>> The TLS WG chairs write:
>>>>>> Significant developments have occurred both within this document and
>>>>>> in the broader TLS ecosystem to address the concerns raised in the
>>>>>> last WGLC.
>>>>> False.
>>>> If you believe Nadim's formal analysis in ProVerif is not a significant
>>>> development
>>> My comments have nothing to do with the judgment call of what qualifies
>>> as "significant".
>> Then, I kindly ask you not to use the words like "sideshow" for someone's substantial technical concern. As John says, key reuse is a fundamental security concern.
>>>> John is surely not the only one. Key reuse was one of my *major*
>>>> concerns.
>>> Sorry if I missed some previous text (but then why don't you provide a
>>> quote?).
>> Because I thought WG participants might trust me that I am not lying. 
>> 
>> Anyway, here you go from Thu, 27 Nov 2025 11:18:11 -0800 (PST) according to archives [0]:
>> 
>> I have no opinion from PQ perspective but from 
>> traditional crypto perspective, I agree with your concern on key reuse. 
>> Intuitively, I would assume the same problems would hold in pure PQ but 
>> there may be subtleties.
>> 
>> Anything else I can do for you to assure you that John was not the only one objecting about key reuse? or to assure you that key reuse was a technical concern that I have had for quite a long time?
>> 
>> Back then, I was -- unfortunately -- not able to formally prove it and hence, I did not emphasize it a lot. Nevertheless, my belief was that it is a weakness that can be exploited together with other weaknesses. And I believe that is typically what happens in reality too. I think there is rarely a single weakness in real-world compromises. It's often a combination of weaknesses which lead to bigger vulnerabilities.
>> 
>>>> AFAIU, most of the 25 objecters
>>>> from the last WGLC now seem to be satisfied with the formal proof. I've seen
>>>> only 4-5 of those still objecting. All other objecters so far are new
>>> Your numbers are not backed by URLs or other evidence; I have no idea
>>> why you think excluding "new" objectors is justified;
>> I'm not excluding any one at all. I'm just saying that based on the information we had from last WGLC objectors, we tried to get confirmation on all sides as far as we could: both symbolic and computational proofs.
>> 
>> We requested feedback on formal analysis or what else we can do to satisfy the needs of other objectors. Nobody showed up. And hence, WGLC is well-justified to understand what technical work needs to be done -- or alternatively whether spending any further WG energy on this draft is worth it.
>> 
>> Best,
>> 
>> -Usama
>> 
>> [0] https://mailarchive.ietf.org/arch/msg/tls/cGVWArNZO-N_r-5u5K8lBoVUitY/
>> 
>> _______________________________________________
>> TLS mailing list -- [e-mail]
>> To unsubscribe send an email to [e-mail]
> 
> _______________________________________________
> TLS mailing list -- [e-mail]
> To unsubscribe send an email to [e-mail]