Good with a discussion on formal analysis. >explicitly indicate on a very prominent place, preferably abstract, whether >the draft has gone through FATT review or not,
I think formal analysis should be treated like any other form of analysis and referenced where appropriate, for example in the Security Considerations section. While I think it is excellent that the IETF is using formal analysis as a tool, I am seeing a tendency toward placing too much faith in it. Like all security proofs, formal analysis is only as strong as its assumptions and model. The scope is typically limited, and the model does not necessarily capture real-world deployment complexity, implementation details, operational constraints, or misuse scenarios. The public formal verification effort around RFC 8446 was highly valuable and resulted in a number of publicly accessible papers and improved understanding of the protocol. However, my impression is that the experience with the current FATT process has been more mixed. Cheers, John From: Muhammad Usama Sardar <[email protected]> Date: Tuesday, 3 March 2026 at 09:56 To: Eric Rescorla <[email protected]> Cc: [email protected] <[email protected]> Subject: [TLS] Re: Fwd: New Version Notification for draft-usama-tls-fatt-extension-02.txt Hi Ekr, Thank you for your valuable feedback. I respect your opinion and I apologize the current draft could not live up to your expectations. I also do admit that a lot of it is about the disputes but from my perspective, it has already killed a lot of time, and I believe it needs an urgent fix. While I believe I do have some proposed solutions, such as: * explicitly indicate on a very prominent place, preferably abstract, whether the draft has gone through FATT review or not, * WG should be given the right to argue against the decision of the chairs regarding whether FATT analysis is required, * be more explicit on: * what is the scope of FATT, * what kind of drafts need FATT review and why, * surely not every draft needs to go to FATT but the controversial ones do need to go to FATT, regardless of the nature of the draft and whatever the chairs believe (I want to remind folks that 'nothing required' is a perfectly valid outcome of initial FATT review.) the draft is presenting factual evidences that the problem exists, since a few folks shared their opinions in meeting 123 that changes to FATT process are not required. Also, please note that I am not yet asking for adoption. I believe we first need to agree that reforms are actually required. The adoption-ready version will then replace these pain points by proposed solutions. I've opened an issue [0] for your feedback and will submit a version addressing the parts I understand when the submission reopens. Some thoughts and questions below: On 03.03.26 02:16, Eric Rescorla wrote: TBH, I don't find this draft that helpful. yeah, sorry as above. While there are some parts of it that seem like they might be unobjectionable, Could you share which ones? It would be good to agree on something at least :) way too much of it seems to be concerned with litigating various disputes about specific past events. I hear your concern about litigating past events but I don't want these to repeat again. My goal is to document the identified gaps with concrete (and not fictional ones) examples, discussing those and mutually finding the best way forward. That's not a good starting point for reform. Maybe. I am open to suggestions. Do you have an alternative proposal for a starting point? More generally, this draft seems to envision some defined role in the WG process for "Verifiers" other than through the FATT. I am not following what you mean by "other than through the FATT". Did you mean "other than the FATT"? Anyway, I appreciate your concern on roles. I did not intend to define a new formal role in the WG process. The definition of "Verifier" was just meant as a shorthand to avoid repeating the phrase "person (team) doing the formal analysis". It's nothing more than that and it has got nothing to do with the formal "roles". The capitalization was intended to distinguish it from the layman use of verifier. If some specific wording is leading to confusion, please point me to that and I'll fix that. The term "Verifier" was admittedly chosen because of lack of better term, and I am not attached to it. I just wanted to have a shorter term than 'formal analysis contributors'. How about 'Analyst'? I'd also welcome any alternatives or PR in the repo, which disambiguates this. For example: The FATT process restricts the Verifier from contacting the FATT directly. We argue that the Verifier should be allowed to contact the FATT (at least the FATT person for a specific draft) because of the following reasons: I don't think this is advisable. I am not completely sure what exactly is "this" referring to here: the first quoted sentence (The FATT process...) or the second one (We argue...)? or "defined role"? If the former, the key point was [1]. If the latter, then see above. >From my perspective, the purpose of having a separate FATT is to ensure that in cases where the WG deems some formal analysis is needed, we have a structure for getting that. That's exactly my point. It should be the WG and not chairs exclusively making unilateral decisions and not even considering worth it to inform WG about those decisions and the rationale behind those decisions. This seems quite far from transparent process, no? I believe the process would benefit from greater transparency so the WG can actually 'deem' when analysis is needed, as you suggested. Thanks and best regards, -Usama [0] https://github.com/muhammad-usama-sardar/tls-fatt-extension/issues/3 [1] https://www.ietf.org/archive/id/draft-usama-tls-fatt-extension-02.html#section-3.3-3
_______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
