Hi all,I maintain my 'no opinion' position. However, if the votes end up in tie, you can use me as a tie-breaker to be a few inches towards support from the middle ground. On request, Sophie kindly provided me substantial technical response off-list which helped clarify my misunderstanding for ML-KEM. This attestation holds unless someone shows a concrete attack/vulnerability in ML-KEM in the context of TLS.
=== Dear Tanja,I sincerely apologize to have misunderstood your concerns. I wanted to say that in my understanding, we /tried/ to address some of your concerns. I am sorry to know that none of your concerns were addressed in your opinion.
I am (intentionally) responding to only a few (and not all) of your items where I have clarifying questions.
On 07.07.26 19:00, Tanja Lange wrote:
I apologize for that. I haven't changed my email setting for quite a long time and you are the first one who has mentioned this to me. I couldn't figure it out. Anyway, I have reported it to my admin. If someone else sees such a problem in my emails, please write to me off-list with some info, such as which email program you use. Thank you!Dear Muhammad, Please see inline (though something in your email setting is messing up the formatting by just indenting; extra > added for making this readable again).
Could you please clarify the difference? I typically use them interchangeably to meanviolation of a specific security (or privacy) property.On Tue, Jul 07, 2026 at 04:19:23AM +0200, Muhammad Usama Sardar wrote:The draft now responsibly includes promotion of hybrids. Can you show me a concrete attack resulting from risky behavior?Well, it would have to be a vulnerability rather than an attack, but I assume that's what you mean.
Below you mention Nadim's proof. What that shows is that if you give away the secret key of one of the components of ECC+PQC then the combined system is still secure. If you only have PQC and give away the secret key for that, it is completely insecure. So, I assume that your question is how it could be that we give away the secret key for ML-KEM. a) If cryptanalysis of ML-KEM succeeds (completely, as in SIKE, or weakening it enough as RC4 or RSA-768) the only protection is gone, which makes the outcome _worse_ than the current situation of pure ECC and worse than for ECC+ML-KEM. Neither of those will help long-term, but at least the data is not exposed yet. b) If there are implementation errors in ML-KEM that remove or weaken the security the only protection is gone. Same as a)
Agree with both. Respectfully, I just haven't seen anyone showing any of the 'if' condition to hold right now. Somebody showed an old CVE in the thread but as I understand, prohibition of key reuse avoids that.
I am not a cryptographer, so I need your help in showing the vulnerabilities. Would you mind sharing which specific implementation you think has errors?
As much as I like PQC and push for its adoption asap because we're too late (not my fault), I also warn about stability and code quality and we must acknowledge that. I love formally verified software like everybody else and it's the best we can do,The WG spent quite some time in planning, discussing and executing the formal analysis to the extent that nobody was complaining about formal analysis. Thanks to Nadim, it was finally formally verified in ProVerif and checked by at least one FATT member. So we have done "the best" we could do, as you seem to be saying. Computational proofs already exist and the WG seemed to believe that to be sufficient.This might be one part of the misunderstanding. There are (at least) 3 layers where formal verification is needed * protocol level, * proof of primitives level, * implementation level. A proof in ProVerif fits in the first category. I wrote "formally verified software" which is the third kind and not addressed in the RFC and it concerns the software ecosystem.
In general, I agree but I don't think the three layers are disjoint. Do you agree? For example, in our recent (unrelated to ML-KEM) work, we used ProVerif to verify implementation-level verification of real-world code. Nothing stopped us from making the formal model in ProVerif for the implementation.
Anyway, IIRC Yaakov mentioned the limitations of formal verification during this WGLC and I agree with him.
Best regards, -Usama
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
