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

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:
> 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).
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!
> 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.
Could you please clarify the difference? I typically use them 
interchangeably to meanviolation of a specific security (or privacy) 
property.
> 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

_______________________________________________
TLS mailing list -- [email protected]
To unsubscribe send an email to [email protected]