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?
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.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."
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.
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
