Hi Usama, > we add a statement on preference of hybrids and refer to the paper in the > security considerations of draft-ietf-tls-mlkem.
I agree that this is a good idea and would love to see it, ideally referencing my analysis. Nadim Kobeissi Symbolic Software • https://symbolic.software > On 4 Jun 2026, at 8:54 PM, Muhammad Usama Sardar > <[email protected]> wrote: > > > Hi Nadim, > > Awesome work. Thanks a lot. That resolves my concern. > > Before we put this discussion behind us, I would like to suggest that: > > we put artifacts in front of FATT for evaluation: It would be good to have > the artifacts evaluated once, so that we can keep using them in the future > for all PQ extensions. > we add a statement on preference of hybrids and refer to the paper in the > security considerations of draft-ietf-tls-mlkem. > 1 would be nice -- the earlier the better. But IMHO 2 is essential. > > One small note: I noticed that in your paper, you cite link to editor's copy > [0]. I have published -02 [1] -- in the state it was -- for you to have a > permanent citation, because the editor's copy will keep changing -- and has > already moved to the next steps -- and it might be confusing for the > reviewers/readers to find a mismatch in the paper and the reference. -02 is > just for you; others don't need to worry about it and there is nothing new to > read in it. > > > >> One implementation-facing angle that may be worth spelling out, even if it >> is outside what the symbolic model can prove, is which negative tests would >> best catch hybrid-specific integration mistakes. > I think this is very valuable and practically useful suggestion to craft > tests and folks are welcome to work on it. But I am more than happy with what > has been achieved. Thanks Nadim. >> Any kind of Undefined Behavior in implementation would compromise both. > I believe one can actually do formal verification on the real code to have > high assurance that there is no Undefined Behavior. >> I think some of the informal claims are stronger than what >> this paper proves. This does not matter for ML-KEM or ECC hybrids >> thereof — but could matter for another KEM. > Could you please explicitly share those differences? >> Note that once a CRQC emerges, which some people say may happen very soon, >> [...] > and some people have argued it may never occur [2] >> I think formal analysis in the not so distant future should focus on quantum >> attackers and treat ECC and RSA as not providing any security. > Once the WG agrees on setting them to 'N' or 'D' probably that will be the > appropriate time to update the formal models. >> Many TLS libraries enforce handshake timeouts, so unless the key exchange >> algorithm is completely broken, an attacker cannot practically keep a >> connection open long enough to forge the Finished message. > Is the handshake timeout typically pre-configured or dynamically selected? > Does anyone have datapoints on handshake timeout in common TLS libraries? > Actually, some people propose remote attestation within the handshake, which > requires significantly increasing the timeout. In particular, it adds the > time for generation and appraisal of Evidence within the handshake, which > gives the adversary plenty of time to do a lot of interesting things. > >> It is great that TLS WG have clarified that static keys MUST NOT be used for >> key exchange. This significantly lower the risk for these kind of attacks. > Agree. It would have been beneficial to do it long time ago, but better late > than never. > > > Best regards, > > -Usama > > > > [0] > https://muhammad-usama-sardar.github.io/risks-of-mlkem/draft-usama-tls-risks-of-mlkem.html > > [1] https://datatracker.ietf.org/doc/draft-usama-tls-risks-of-mlkem/02/ > > [2] > https://www.ietf.org/archive/id/draft-usama-tls-risks-of-mlkem-02.html#section-6.4 > > > >
_______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
