Hi Usama, Thank you for your explanation. What you write makes sense!
Taking your response into account, I think my issue is mostly that you suggest adding a "formal analysis considerations" section with protocol model, properties, threat model, etc. This section seems like it would shift the responsibility from those conducting the formal analysis to those designing the protocol. It's great to have a draft that is easy to analyze, but ultimately, formal analysis people should do the scoping of what is and what is not relevant (and this is not too much work). Having a protocol model, security properties, and a threat model is valuable for everyone. Why not simply require that this is present in the draft? Security considerations seem like a great place to specify properties and threat model. The protocol model can go wherever it fits. Intro is also a great place. Best, Felix Am Do., 10. Juli 2025 um 12:57 Uhr schrieb Muhammad Usama Sardar < [email protected]>: > Hi Felix, > > Thank you for your feedback. I am a bit surprised because what I am asking > for is not much different from RFC 4101 (as pointed out in the draft). > On 10.07.25 11:33, Felix Linker wrote: > > 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. > > Maybe. I believe having it as part of the process is helpful but I am open > to discussion on why you think otherwise. At least the points you > highlighted below are not convincing to me. > > 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). > > I believe you are making a gross exaggeration here. I do have some > counterexamples to your point on "they would say ...". Before publishing > this draft, I have had some discussions with some authors on this point and > nobody has so far said "all of my draft is about cryptographically-relevant > changes" or that "all changes are relevant to be analyzed". The authors I > talked to include just around two years of work on protocol design up to > two decades of work on protocol design in the IETF. They include authors > with no RFC all the way up to almost 100 RFCs. > Also, please note that a protocol diagram is meant to be just a starting > point. This is not meant to say that the verifier should not look at other > parts of the draft. This also does not exclude the option for the verifier > to decide by himself which parts should be modeled. > > The same goes for the threat model although you're less explicit here what > you ask from the authors. > > Could you please be more explicit on "the same" and what exactly is your > point here? > > 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. > > In my view, this is indeed covered in section 4, e.g., "the verifier may > propose updates to the Formal Analysis Considerations section, ...". Could > you be more explicit on what you find missing/limiting in Sec. 4 in your > view? > > > 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. > > I think "Dolev-Yao adversary" is well known. I can add a reference. I am > also fine with "active network adversary" if people find that easier. > > 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." > > Some protocols are designed based on the hypothesis that certain keys are > compromised and provide protection for that. I will add an example of a > draft to clarify this. > >
_______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
