Re: [TLS] Proposal: a TLS formal analysis triage panel

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 <durumcrustulum@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 <joe@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
>