> it's unclear to me whether this review would be a hard requirement to pass WGLC. Let's say a document makes it to that stage, and it is sent to the triage panel, but the panel never produces a formal analysis of it. (This could happen for example if the researchers don't find the extension at hand interesting enough, they're volunteering to help so I wouldn't blame them for picking what they want to work on.) In that hypothetical scenario, does the document proceed without formal analysis, or is it blocked?
Indeed; the interaction with the panel would be in two phases: any changes that are being proposed by/to the WG would have a preliminary triage of whether such changes _should_ have formal analysis, and of what scope/type. This would probably be nicely triggered by an adoption call. Ideally we'd have a sense from the panel of whether the proposed changes would entail a significant amount of formal analysis work from the get-go, or not. This preliminary triage can help inform the adoption call discussion. If the proposal is adopted, and the working group has received a formal analysis triage from the panel, and accepts the general scope of work to be a requirement / blocker before moving to WGLC, then it is. We then work with the panel to select the researchers/whomever to conduct the analysis, which may entail rounds of back and forth if the document changes over time. There may be changes that, on triage from the panel, are 'easy' and may not require updated analysis at all, or very little. The WG may agree to adopt the document and agree to proceed to WGLC _without_ formal analysis, with the implicit understanding that the adopted document and the one approaching WGLC will not have significantly diverged from each other. If we are worried about this, we can implement a sort of 'last chance' review with the panel to make sure we aren't missing something on such a document before actually triggering the WGLC. This is sort of what I had in mind, but am of course welcome to suggestions or changes. 😁 On Tue, Mar 5, 2024 at 9:12 PM David Schinazi <dschinazi.i...@gmail.com> wrote: > Hi Deirdre, > > Thanks for this, I think this is a great plan. From the perspective of > standards work, more formal analysis is always better, and this seems like > a great way to motivate such work. > > That said, it's unclear to me whether this review would be a hard > requirement to pass WGLC. Let's say a document makes it to that stage, and > it is sent to the triage panel, but the panel never produces a formal > analysis of it. (This could happen for example if the researchers don't > find the extension at hand interesting enough, they're volunteering to help > so I wouldn't blame them for picking what they want to work on.) In that > hypothetical scenario, does the document proceed without formal analysis, > or is it blocked? > > Thanks, > David > > On Tue, Mar 5, 2024 at 5:38 PM Deirdre Connolly <durumcrustu...@gmail.com> > wrote: > >> A few weeks ago, we ran a WGLC on 8773bis, but it basically came up >> blocked because of a lack of formal analysis of the proposed changes. The >> working group seems to be in general agreement that any changes to TLS 1.3 >> should not degrade or violate the existing formal analyses and proven >> security properties of the protocol whenever possible. Since we are no >> longer in active development of a new version of TLS, we don't necessarily >> have the same eyes of researchers and experts in formal analysis looking at >> new changes, so we have to adapt. >> >> I have mentioned these issues to several experts who have analyzed TLS >> (in total or part) in the past and have gotten tentative buy-in from more >> than one for something like a 'formal analysis triage panel': a rotating >> group of researchers, formal analysis experts, etc, who have volunteered to >> give 1) a preliminary triage of proposed changes to TLS 1.3¹ and _whether_ >> they could do with an updated or new formal analysis, and 2) an estimate of >> the scope of work such an analysis would entail. Such details would be >> brought back to the working group for discussion about whether the proposed >> changes merit the recommended analysis or not (e.g., a small, nice-to-have >> change may actually entail a fundamentally new security model change, >> whereas a large change may not deviate significantly from prior analysis >> and be 'cheap' to do). If the working group agrees to proceed, the formal >> analysis triage panel consults on farming out the meat of the analysis work >> (either to their teams or to students they supervise, etc.).\ Group >> membership can be refreshed on a regular schedule or on an as-needed basis. >> Hopefully the lure of 'free' research questions will be enticing. >> >> The goal is to maintain the high degree of cryptographic assurance in TLS >> 1.3 as it evolves as one of the world's most-used cryptographic protocols. >> >> I would like to hear thoughts on this idea from the group and if we would >> like to put it on the agenda for 119. >> >> Cheers, >> Deirdre >> >> ¹ 1.3 has the most robust analysis; we'll see about other versions >> >> ---------- Forwarded message --------- >> From: Joseph Salowey <j...@salowey.net> >> Date: Tue, Jan 23, 2024 at 10:51 AM >> Subject: [TLS] Completion of Update Call for RFC 8773bis >> To: <tls@ietf.org> <tls@ietf.org> >> >> >> The working group last call for RFC8773bis has completed >> (draft-ietf-tls-8773bis). There was general support for moving the document >> forward and upgrading its status. However, several working group >> participants raised the concern that formal analysis has not been conducted >> on this modification to the TLS protocol. We should at least have consensus >> on whether this document has the required analysis before upgrading it, but >> we also need a more general statement on this requirement since the TLS >> working group currently does not have a policy for what does and does not >> need formal analysis or what constitutes proper formal analysis. >> >> The chairs are working on a proposal for handling situations like this >> that we plan to post to the list in a week or so. >> >> Thanks, >> >> Joe, Deirdre, and Sean >> _______________________________________________ >> TLS mailing list >> TLS@ietf.org >> https://www.ietf.org/mailman/listinfo/tls >> >
_______________________________________________ TLS mailing list TLS@ietf.org https://www.ietf.org/mailman/listinfo/tls
