David Stainton <[email protected]> writes: > 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 The entire idea behind https://github.com/tlswg/tls-fatt seems like a good thing, and I wonder what would warrant side-step it. /Simon > +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] >
signature.asc
Description: PGP signature
_______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
