Hi Usama, all, Thanks. I agree this should not make the draft depend on a full new test suite before progressing. The useful near-term thing may just be to collect a small set of negative cases that implementers can run against the existing artifacts.
The cases I would start with are roughly: - negotiated hybrid group differs from the group encoded/bound in either component; - one component is omitted, malformed, or fails decapsulation/validation; - KEM and ECDHE values are individually valid but assembled from different handshakes/transcripts; - a peer attempts to continue as standalone ML-KEM or standalone ECDHE after a hybrid group was negotiated; - application traffic secrets are derived only after both components have been accepted under the negotiated hybrid group. That is not a formal proof obligation, but it would make the intended “both components are bound and accepted” property easier to check in implementations. If there is a preferred place for such cases – draft text, a GitHub issue, or a separate test-artifact note – I can help shape it there. Best, Songbo Bu On Thu, 4 Jun 2026 21:48:32 +0200, 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]
