Is anyone from AWS active on the WG? When I left AWS a few years back, they had a very active group entirely dedicated to this kind of work, and any version of TLS is obviously relevant to AWS. Might be worth reaching out to them.
On Jun 1, 2024 at 1:32:20 PM, Eric Rescorla <e...@rtfm.com> wrote: > Thanks for posting this. > > It's great to see the triage panel coming together. This is very > thorough and helpful. > > My take-home from this report is that the security properties of > 8773-bis are not immediately obvious and therefore that prior to > advancing it we should actually have some sort of more formal analysis > using a tool like Tamarin/Proverif, etc. > > > I did want to address one point from Russ's response: > > > Who will perform this analysis? I asked a researcher to perform > > such an analysis, and the response was that it is too simple to get > > a paper. Now waht? > > Fundamentally, the IETF is a volunteer organization and it's up to > the WG members who are interested in a document to bring it any time > we have a requirement for a document to advance, the authors and the > WG need to find a way to fulfill it. This is true both for subjective > requirements (i.e., document has to be of high quality) and objective > ones. For example, RFC 6410 requires > > There are at least two independent interoperating implementations > with widespread deployment and successful operational experience. > > The IETF doesn't have a mechanism for producing these implementations; > that's the responsibility of the WG and the community at large, and > if there is insufficient interest to produced these implementations, > then the specification doesn't advance. I would note that the > TLS WG has already held some documents from advancing to PS > until there was sufficient implementation experience, so it's not > just about 6410. > > Similarly here, if the WG feels that a change is sufficiently large to > require formal analysis then the WG -- and more specifically those who > want the work to move forward -- need to figure out how to get that > analysis done, though of course the triage panel or the broader > community might help facilitate if there is enough demand or interest > in the work. > > > > Some more detailed thoughts on the panel review below. > > I did have one question about the format of the report. I see a > lot of "I statements". I assume these are (potentially) different > people's comments aggregated together, not all the same person? > I know it's more work but it might be more helpful if future reports > were structured in a slightly more narrative fashion. > > > 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 this is the heart of the question: should I be inferring > anything about the counterparty's identity based on them knowing > the PSK and if so, what? > > > > 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. > > My sense is that because the resumed keys are all derived from the > original PSK, that they would also be CRQC-resistant. > > > With that said, I don't understand how resumption is supposed to work > in practice S 5.1 says. > > > The "pre_shared_key" extension is defined in Section 4.2.11 of > > [RFC8446]. The syntax is repeated below for convenience. All of the > > listed PSKs MUST be external PSKs. If a resumption PSK is listed along > > with the "tls_cert_with_extern_psk" extension, the server MUST abort > > the handshake with an "illegal_parameter" alert. > > One of the basic assumptions of TLS 1.3 is that the server can choose > whether to resume or not and the handshake completes either way. > However, this restriction makes that impossible because the client > must offer *either* the external or resumption PSK. If it offers > the external PSK resumption is not possible and if it offers the > resumption PSK and the server is not willing to resume then > the external PSK is not used. > > -Ekr > > > > > > > On Mon, May 20, 2024 at 3:06 PM Deirdre Connolly <durumcrustu...@gmail.com> > wrote: > >> 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 >> > _______________________________________________ > TLS mailing list -- tls@ietf.org > To unsubscribe send an email to tls-le...@ietf.org >
_______________________________________________ TLS mailing list -- tls@ietf.org To unsubscribe send an email to tls-le...@ietf.org
