I support initiating the FATT process here, and I support the work Usama is doing to use symbolic models to better understand the protocol's security properties. Even where existing proofs give us confidence, having an explicit symbolic analysis of the standalone-KEM case is the kind of thing that's worth doing rather than assuming, and there are clearly participants willing to do it.
+1 from me. David On Sun, May 31, 2026 at 1:15 AM Nathanael Ritz <[email protected]> wrote: > Hi Usama, > > I have some feedback re: "Justification based on FATT Process" (sect. 4) > for the -01 draft [0]. > > In sect. 4-6.2.1 you highlight "3 public forks". E.g., > > - jupenur/formal-spec-id-crisis > - nathanaelritz/formal-spec-id-crisis [1] > - telephonicrobotics/formal-id-crisis-spec [2] > > I wanted to clarify that I control both repos, `telephonicrobotics` and > `nathanaelritz`. I.e., `telephonicrobotics` is my GH username and I use > `nathanaelritz` for my more front-stage work. Additionally, it appears both > links point directly to the original init commit #a25631b [3], [4] instead > of hyperlinking to the main branch for either repository -- although that > could just be a GH artifact. > > Truth be told, the cloned repo at > `telephonicrobotics/formal-id-crisis-spec` is more of an artifact than > anything actively developed. As it's presented, I'm afraid this may cause > some readers to accidentally perceive my substantive contributions to this > code base as larger than they currently are. > > Therefore, for the -02 revision of your draft, I propose dropping the > citation for `telephonicrobotics/formal-id-crisis-spec` altogether and > hyperlinking directly to the main branch of my main fork at > `nathanaelritz/formal-spec-id-crisis` [5] for maximum clarity. > > Thanks, > Nathanael > > [0] > https://www.ietf.org/archive/id/draft-usama-tls-risks-of-mlkem-01.html#name-justification-based-on-fatt > [1] > https://www.ietf.org/archive/id/draft-usama-tls-risks-of-mlkem-01.html#section-4-6.2.2.2.1 > [2] > https://www.ietf.org/archive/id/draft-usama-tls-risks-of-mlkem-01.html#section-4-6.2.2.3.1 > [3] > https://github.com/nathanaelritz/formal-spec-id-crisis/blob/a028cec823b7d9bf13dd5a1dd71ab14c75b1a83d/TLS-a/fix/tls-lib-simple.pvl#L38-L41 > [4] > https://github.com/telephonicrobotics/formal-id-crisis-spec/blob/c1953127ce004e51b888250591ec9971ad50e98c/TLS-a/fix/tls-lib-simple.pvl#L38-L41 > [5] https://github.com/nathanaelritz/formal-spec-id-crisis/tree/main > > > On Fri, 29 May 2026 at 04:38, Muhammad Usama Sardar < > [email protected]> wrote: > >> 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] >> To: Muhammad Sardar <[email protected]> >> <[email protected]>, Muhammad Usama Sardar >> <[email protected]> >> <[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] >> > _______________________________________________ > TLS mailing list -- [email protected] > To unsubscribe send an email to [email protected] >
_______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
