Aha - just saw your conversation with Thom. Seems like we all agree :) Sorry for the spam.
Best, Felix Am Fr., 18. Juli 2025 um 11:35 Uhr schrieb Felix Linker < [email protected]>: > 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]
