[TLS] Kicking off the TLS 1.3 formal analysis triage panel

[Deirdre Connolly <[e-mail]>]

Hello everyone! We're kicking off our TLS 1.3 formal analysis triage panel.

We have these volunteers participating:

- Douglas Stebila
- Dennis Jackson
- Franziskus Kiefer
- Cas Cremers
- Karthikeyan Bhargavan
- Vincent Cheval

Some of them are on this list, some are not, major welcomes and thank yous
all around!

I will link to my write up to the working group
<https://mailarchive.ietf.org/arch/msg/tls/RupKEHeJdAzxpNEZnRgerk4en1c/>and
the recording of the most recent meeting
<https://youtu.be/Oo1UzQtfRYw?feature=shared&t=1485> for more context if
you want it.

The goal of the triage panel is to maintain the high degree of
cryptographic assurance in TLS 1.3 as it evolves as a living protocol. To
paraphrase a recent analysis of Encrypted Client Hello, one can see three
prongs motivating formal analysis of changes or extensions to TLS 1.3:

- Preservation of existing security properties: the authentication,
integrity, and confidentiality properties that have already been proven are
preserved
- New, stronger security properties: such as improved privacy demonstrated
by ECH, prove that extensions satisfies new goals
- Downgrade resilience: prove that active attackers cannot downgrade the
changed/updated/extended protocol to bypass/remove the new guarantees

These are especially salient for new features like Encrypted Client Hello,
but I would say the top bullet is the front of mind for most proposed
documents coming through TLSWG: people want to use TLS 1.3 in new settings,
in updated contexts, and want to tweak it a bit for their use case, and we
want to make sure these changes do not degrade the already proven security
properties of TLS 1.3.

Here's how I envision this going: every few weeks or so, more likely than
not spurred by a document introduced at a (March, July, November) IETF
meeting, we chairs ping the triage panel directly with document drafts that
we'd like a first pass sniff test on whether these proposals:

- imply a change to previous security analysis assumptions (via pen and
paper, formal methods tools, computer-aided provers, any/all of the above)
- whether such a change behooves updated analysis
- if updated analysis is recommended, of what type, what scope, and
estimated time to complete, given such and such a person or team

We (the chairs) will collect responses, collate them, and bring them to the
working group as part of an adoption call or other working group
discussions about a document. If this process did not occur (say something
was adopted long ago and has been dormant but now is being revived etc) we
may come back and run a similar procedure again. If the working group
agrees on requiring formal analysis for a document before it goes through a
last call, we will ask the triage panel for recommendations or advice on
trying to match the project with a group or a researcher who can work with
the document authors on delivering the analysis.

The first thing on deck is 8773bis
<https://datatracker.ietf.org/doc/draft-ietf-tls-8773bis/>, with more to
come. Hopefully this is useful.

Yay!

Deirdre, for the chairs