Hi Usama, Building on Felix’ points:
Though I think that you raise some decent points about certain types of content that document authors / the TLS community should include in drafts (I have certainly complained about unclear threat models and security goals in drafts) I don’t think that a separate “FATT Considerations” is the right way to approach this. Instead, many of these points should just be part of the main body and/or security considerations sections of relevant drafts. I think putting them in a “FATT” section both makes them an afterthought, and I think that such content is actually very relevant to a general audience, not just the FATT, as e.g. security goals are very relevant to anyone who might want to implement a certain extension (as I consider security goals as essentially another type of functionality that an extension may provide). If we want to develop more guidance for document authors such that “have you thought about writing this down” covers these things, we could maybe consider developing something like https://datatracker.ietf.org/doc/draft-irtf-cfrg-cryptography-specification/ for TLS (or, less formally, put some suggestions on the IETF wiki). Thanks for raising the point though! Cheers, Thom (speaking for myself) > Op 10 jul 2025, om 11:33 heeft Felix Linker <[email protected]> het > volgende geschreven: > > Hi Usama, > > I have some thoughts on what you propose. I think it's a laudable goal to > have more drafts be formally verified, but I wonder whether formalizing the > process more will get the job done. > > I see some problems with what you propose. First of all: Your request for a > protocol diagram puts the cart before the horse. You write: "a protocol > diagram specifies the proposed cryptographically-relevant changes compared to > the standard TLS protocol." We, as formal analysis experts, should decide > which parts of the protocol are relevant to model and which we can omit. If > you would ask an author, they would say that all changes are relevant to be > analyzed (and they would be correct to ask us for that). The same goes for > the threat model although you're less explicit here what you ask from the > authors. > > I see our role as formal verification experts more broadly. We are not simply > the grunts that carry out the proof. We can inform the design process of > protocols and help designers explicate their threat model and desired > security properties. Formal analysis is an iterative process that informs > both properties and the threat model. Sometimes, a designer will tell you > that they wanted to achieve property X. You tell them, you cannot prove X, > but you can prove X' and then the designer will tell you that this is > actually what they meant. > > Now some editorial nits: I personally don't like the term "Dolev-Yao > adversary" as it's gatekeeping. People who don't know it certainly have to > google it. Why not call it "active network adversary?" Means the same but the > term is self-describing. > > In the threat model section, you write: "In addition, it could specify any > keys (e.g., long-term keys or session keys) which are assumed to be > compromised (i.e., available to the adversary)." No protocol has (or at least > should have) such keys. I guess you mean: "which may be compromised by the > adversary." > > Cheers, > Felix > > > Am Mo., 7. Juli 2025 um 20:24 Uhr schrieb Muhammad Usama Sardar > <[email protected] > <mailto:[email protected]>>: >> Hello TLS and UFMRG, >> >> I have proposed some extensions to the FATT process to make it sustainable >> and faster for all stakeholders. For authors, this would mean adding a new >> "Formal Analysis Considerations" section with a threat model, informal >> security goals, and a protocol diagram. >> >> For TLS WG, I propose not to consider drafts for adoption until this section >> is provided. Of course, it applies only to drafts proposing non-trivial >> changes to the TLS protocol. >> >> I view the proposed division of responsibilities as a good way forward until >> UFMRG focuses its activities on what it was originally created for -- >> "Usability". >> >> I welcome any feedback/comments/thoughts. >> >> Thank you, >> >> Usama >> >> >> -------- Forwarded Message -------- >> Subject: New Version Notification for >> draft-usama-tls-fatt-extension-00.txt >> Date: Mon, 7 Jul 2025 10:36:05 -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-fatt-extension-00.txt has >> been >> successfully submitted by Muhammad Sardar and posted to the >> IETF repository. >> >> Name: draft-usama-tls-fatt-extension >> Revision: 00 >> Title: Extensions to TLS FATT Process >> Date: 2025-07-07 >> Group: Individual Submission >> Pages: 6 >> URL: https://www.ietf.org/archive/id/draft-usama-tls-fatt-extension-00.txt >> Status: https://datatracker.ietf.org/doc/draft-usama-tls-fatt-extension/ >> HTML: https://www.ietf.org/archive/id/draft-usama-tls-fatt-extension-00.html >> HTMLized: >> https://datatracker.ietf.org/doc/html/draft-usama-tls-fatt-extension >> >> >> Abstract: >> >> This document proposes a new "Formal Analysis Considerations" section >> where the authors provide a threat model, informal security goals, >> and a protocol diagram. This document applies only to non-trivial >> extensions of TLS, which require formal analysis. >> >> >> >> The IETF Secretariat >> >> >> -- >> Ufmrg mailing list -- [email protected] <mailto:[email protected]> >> To unsubscribe send an email to [email protected] >> <mailto:[email protected]> > -- > Ufmrg 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]
