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
_______________________________________________ TLS mailing list TLS@ietf.org https://www.ietf.org/mailman/listinfo/tls