Hello! We're back with some feedback from our triage panel on 8773bis. <https://datatracker.ietf.org/doc/draft-ietf-tls-8773bis/> We had participation from all members of the panel this time around (🎉).
Some high-level takeaways: - agreement that more clarity in the document about the intended security goals is needed - support for a proper security analysis to shore up the security arguments: for authentication properties, a Tamarin analysis may do ------------------------------------------------------- Here is a summary across all participants: *On changes made by the 8773bis draft to TLS 1.3 and on the draft itself:* The draft adds an extension to negotiate a handshake using both a PSK and certificates for authentication. The draft makes specific claims around PQ confidentiality if the PSK is secret and forward secrecy when the PSK is destroyed. The claims the draft makes around authentication based on the PSK aren't clear to me on the first reading and would likely need some refinement prior to analysis. I think the draft could be a little more precise in what it's trying to achieve, which would also help the security arguments. I agree that the draft could be clearer on what the security goals it's trying to achieve are. The language in Section 7 about the assumptions on the PRF is not quite right: > This extension provides the desired protection for the session secrets, as long as HMAC with the selected hash function is a pseudorandom function (PRF) [GGM1986]. It should actually be assuming the dual PRF security of HMAC, since the TLS key schedule uses the PSK and other chaining inputs sometimes in the first input of HMAC, sometimes in the second. the informal security arguments in some related documents (eg https://datatracker.ietf.org/doc/html/rfc9257, https://www.rfc-editor.org/rfc/rfc9258.html ) seem much better worked out. More clarity about the exact claimed additional security is required. I found the RFC unclear on how the extension should be used in subsequent sessions. They wrote: "Since the "tls_cert_with_extern_psk" extension is intended to be used only with initial handshakes,…”. So let’s say you use the extension in a first session with an external PSK + cert. Must the PSK generated from that session ticket be used in subsequent sessions with their extension , i.e. cert + psk, or can it go back to “normal mode”, i.e. psk only without cert? I’m not sure how this behaves specially w.r.t. to their goal of being safe against CRQC. *Does the draft invalidate the previous security analyses?* Yes. Although the draft has an informal sketch that it doesn't make the key derivation in a particular handshake 'worse', this doesn't immediately rule out any awkward cross-handshake interactions. This is a reasonable extension to TLS 1.3 and can be done in a way that does not affect the existing security guarantees of the protocol. I am curious whether using such a PSK breaks the privacy guarantees of ECH, and whether those two extensions are compatible. The extension's "security argument" in the extension's text is invalid: it is not obvious that this extension only improves security. I don't immediately see how it would degrade base TLS security, though a proper analysis would make me more confident; I'd be wondering how the "context" of this particular mode is clearly separate from (preventing message confusion), and carried through (transcript/state towards e.g. resumption/post-handshake authentication), w.r.t. other modes. It could well be that in the presence of an active attacker, the new mode doesn't offer *additional* security because of its interaction with similar modes. In such a case, the extension would offer little benefit. *Does the change merit an updated analysis?* I think so. Although I like to think the TLS1.3 key derivation is pretty robust, it's hard to think through the various types of handshake and how they could be composed by an attacker - especially when the PSK might be used in multiple modes by multiple parties. The main question to ask, other than whether this extension breaks prior analyses, is what are the new guarantees it provides: that will indeed require new analysis. I see much more need for analysis when it comes to the authentication properties of the PSK (psk/cert combination), whereas the secrecy (assuming authentication is a non-goal) is much more straightforward. I agree with the above. I'd delineate between confidentiality and authentication, and then be clear about to what extent hybrid security is being expected: - For confidentiality: I guess hybrid confidentiality is desired, meaning that session keys are secure if either the external PSK is unbroken, or ECDH is unbroken (and if the ephemeral key exchange is actually hybrid traditional+PQ, then it's actually a 3-way hybrid) - For authentication: Is there a desire for a hybrid authentication property based on the external PSK? Or is one only relying on the public key certificate for authentication? As for the confidentiality analysis: the fixed key schedule already provides locations for putting all the relevant inputs in and that's part of the existing analyses of TLS, so I don't think you'd get any surprises there. The current security argument is insufficient and there should be a meaningful security analysis. *If so, what type / scope / effort is required?* Symbolic analysis (Tamarin, ProVerif) would be suitable for identifying / eliminating cross-protocol attacks. Extending the existing models seems feasible. For the authentication analysis, I think here a Tamarin-like analysis might be useful for checking undesirable interactions; for example, could anything go wrong if a single PSK is used both as a traditional PSK but also as an external PSK? ------------------------------------------------------- I want to express major thanks to our triage panel for their participation and expertise here! Now it's up to WG to discuss what to do with this analysis. 😁 Cheers, Deirdre, for the chairs On Thu, Apr 18, 2024 at 11:36 AM Deirdre Connolly <durumcrustu...@gmail.com> wrote: > 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 To unsubscribe send an email to tls-le...@ietf.org
