Hi Nadim, Awesome work. Thanks a lot. That resolves my concern.
Before we put this discussion behind us, I would like to suggest that: 1. 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. 2. 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.
I believe one can actually do formal verification on the real code to have high assurance that there is no Undefined Behavior.Any kind of Undefined Behavior in implementation would compromise both.
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
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
