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:
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.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 developmentMy comments have nothing to do with the judgment call of what qualifies as "significant".
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 newYour 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/
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
