[TLS] Proposal: a TLS formal analysis triage panel

[Deirdre Connolly <[e-mail]>]

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 <[e-mail]>
Date: Tue, Jan 23, 2024 at 10:51 AM
Subject: [TLS] Completion of Update Call for RFC 8773bis
To: <[e-mail]> <[e-mail]>


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