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 <[email protected]> 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 
>> <[email protected]> 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 -- [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]

Reply via email to