My understanding of the discussion differs: - This concerns KEMs in general and is independent of draft-ietf-tls-mlkem, ML-KEM, and PQ. - The draft should therefore have been renamed. In fact, I do not think this work should be a draft. An academic paper, together with discussion on the TLS WG mailing list, seems more appropriate. - A proof in the symbolic model would be valuable, but not required, as there are already other proofs supporting the security of KEM use in TLS 1.3.
My suggestion is that you, Nadim, and Nathanael collaborate on a formal ProVerif analysis of TLS 1.3 with KEMs exhibiting different security properties and report the results to the TLS WG once the work is complete. I don’t think a formal FATT process should be started. I want X25519MLKEM758 published as soon as possible. Cheers, John Preuß Mattsson From: Muhammad Usama Sardar <[email protected]> Date: Friday, 29 May 2026 at 12:38 To: [email protected] <[email protected]> Subject: [TLS] Fwd: New Version Notification for draft-usama-tls-risks-of-mlkem-01.txt Dear Joe and Sean, I believe I have collected sufficient attestations from the WG that a new proof is required for draft-ietf-tls-mlkem. As I understand, apart from me, there are at least 2 other WG participants (Nadim [0] and Nathanael [1]) who are already doing or have volunteered to do independent formal analysis in ProVerif. I take that as a strong attestation that there is enough WG energy to do the work. So with these attestations, I would like to request the initiation of the FATT process for draft-ietf-tls-mlkem. I believe it would be good to have FATT's evaluation of the artifacts that would be eventually developed by these efforts. Thank you for your kind consideration. In addition, I believe all concerns have been addressed in this version. Summary of major changes is: * Added justification based on the FATT process: Section 4 * Reorganization, specially in motivation (Section 1.1) * Added some common arguments: Section 6 * Comparison with hybrid ML-KEM in Section 4.1 * Clarification of what "breaking" means in Section 3 For those who haven't had a chance to check the draft yet, more feedback on Sec. 3 and 4 is very welcome. For discussion of details of modeling, please contact me off-list. Best regards, -Usama [0] https://mailarchive.ietf.org/arch/msg/tls/pZe6luYQeT4GhbOc1FE1xi-Lmzc/ [1] https://mailarchive.ietf.org/arch/msg/tls/S5QioGFa3T3AFWIAjsNg8BFy5Co/ -------- Forwarded Message -------- Subject: New Version Notification for draft-usama-tls-risks-of-mlkem-01.txt Date: Fri, 29 May 2026 03:02:54 -0700 From: [email protected]<mailto:[email protected]> To: Muhammad Sardar <[email protected]><mailto:[email protected]>, Muhammad Usama Sardar <[email protected]><mailto:[email protected]> A new version of Internet-Draft draft-usama-tls-risks-of-mlkem-01.txt has been successfully submitted by Muhammad Usama Sardar and posted to the IETF repository. Name: draft-usama-tls-risks-of-mlkem Revision: 01 Title: Potential Risks of Standalone ML-KEM in TLS 1.3 Date: 2026-05-29 Group: Individual Submission Pages: 16 URL: https://www.ietf.org/archive/id/draft-usama-tls-risks-of-mlkem-01.txt Status: https://datatracker.ietf.org/doc/draft-usama-tls-risks-of-mlkem/ HTML: https://www.ietf.org/archive/id/draft-usama-tls-risks-of-mlkem-01.html HTMLized: https://datatracker.ietf.org/doc/html/draft-usama-tls-risks-of-mlkem Diff: https://author-tools.ietf.org/iddiff?url2=draft-usama-tls-risks-of-mlkem-01 Abstract: We attest that standalone ML-KEM in TLS 1.3 breaks the existing formal proofs of TLS in state-of-the-art symbolic security analysis tool, ProVerif. In this draft, we show *exactly* where the ProVerif proofs break, namely transition from symmetric DHKE to asymmetric KEM. More specifically, the existing proofs of TLS in ProVerif are based on commutativity property, whereas commutativity does not apply to standalone ML-KEM in TLS. We also attest that from a formal analysis perspective, this is a much bigger change than RFC8773bis, which indeed went for FATT review (cf. [TLS-FATT]). We, therefore, formally request the chairs to initiate the FATT review of standalone ML-KEM in TLS. A few WG participants have already volunteered to do formal analysis in ProVerif. This draft also offers some preliminary discussion to help the developers and policy makers make informed choices. Finally, the draft also aims to reduce the endless repitition of arguments from both sides presented on several lists by documenting these arguments so they can simply be referred to. The IETF Secretariat
_______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
