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]>: > 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] > To: Muhammad Sardar <[email protected]> > <[email protected]>, Muhammad Usama Sardar > <[email protected]> > <[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] > To unsubscribe send an email to [email protected] >
_______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
