On Sun, Apr 26, 2020 at 2:43 AM Hanno Becker <hanno.bec...@arm.com> wrote:
> Hi, > > Thanks Chris for your thoughts. > > Yes, it seems that specific formal analysis is needed, since we're > dealing with the new > situation that - in contrast to TLS 1.3 - shortened or omitted fields in > the DTLS 1.3 headers > (e.g. epoch, length, CID) introduce a notion of implicit context to a > record which wasn't > present before. This requires analysis of the desired properties of this > implicit context > and their implications on the protocol design. > > For example, such a property might informally be that a party able to > decrypt a record > must have correctly reconstructed the full implicit context of the > record, such as the full > epoch when it was shortened in the header, the CID when it was omitted, or > the length > when it was omitted. > The epoch, the sequence number, and the length are all bound to the AEAD computation: - The epoch determines the key - The sequence number determines the nonce [note that this is actually implicit in TLS 1.3] - The length determines the input to the AAD. And I am proposing removing implicit CIDs. -Ekr This seems most directly achieved by cryptographically binding this > context to the record through AAD, while protecting only the explicit > context makes reasoning > that the party has the correct context either less straightforward (see > the epoch example) or > impossible (current CID issue allowing to decrypt a record in a context > with different CID). > To me it therefore still appears preferable to use a pseudo-header as the > AAD. > > Hopefully some more people from the protocol verification community > will join in here and give their thoughts. > > Best, > Hanno > ------------------------------ > *From:* chris - <chrispat...@gmail.com> > *Sent:* Saturday, April 25, 2020 6:58 PM > *To:* Hanno Becker <hanno.bec...@arm.com> > *Cc:* Eric Rescorla <e...@rtfm.com>; Hannes Tschofenig < > hannes.tschofe...@arm.com>; tls@ietf.org <tls@ietf.org> > *Subject:* Re: [TLS] Choice of Additional Data Computation > > > > So far I fail to understand, on an intuitive level, why it easier to > analyze the protocol when the AAD can take multiple forms potentially > truncating or omitting the underlying data, but then I don't know the > details and you're the expert here. If you have time though to explain a > bit more where the flaw in my thinking below is, that would be great, > provided it's possible. > > > I don't know that there's a flaw in your thinking. At the moment, all that > I can speak to is how authenticating the header (or not) might impact > security of DTLS. We can't directly extrapolate from what we know about > TLS, because the security goal is not to the same. That said what I know > about TLS is the following: the contents of the record header doesn't > matter for security goal considered in [1], as long as (1) the header is > authenticated; and (2) it correctly encodes the length of the next > ciphertext. But since the security goal of DTLS is not the same, the > details of the spec that are (ir)relevant to security are likely to differ. > > > > For example, another thing which I would expect to be more complicated to > verify in full rigor is epoch authentication: If the epoch is reduced to > its two low order bits in the DTLS 1.3 header and thus (at the moment) also > in the AAD, arguing that decryption can only succeed for the correctly > expanded epoch involves knowing that all epochs having different keys. > That's of course true but this fact wouldn't be needed if the full numeric > epoch was always explicitly authenticated in the AAD. This isn't a real > issue in the end, but I would expect it to be a nuisance in a formal proof? > > In terms of what you mentioned regarding decoding details, it seems that > adding the underlying logical header to the AAD ensures more directly that > decryption can only succeed if header decoding (that is, filling in > implicit data or expanding truncated data) was done correctly, whereas it > is less clear with the truncated or omitted data in AAD, as in the epoch > example above. Is it possible to explain what the flaw is here intuitively? > > > I'm afraid I would need to absorb spec and think about its intended > security properties in order to answer these specific questions. I'm sorry > if this answer is unhelpful; Ekr asked that I chime due to my prior work on > TLS. But I don't think there's a simple answer here, and unfortunately I > don't have the time to think it through at the moment. > > For now, I'll just leave you with this. I'm a fan of the following design > principle: whenever there is a branch in your code that depends on a bit > read from the wire, that bit should be authenticated if possible. To your > example, if a decision you're about to make depends on you agreeing with > the peer on the current epoch, the principle says that the epoch had better > be authenticated. Whether it's necessary or appropriate to do so here (via > AEAD decryption) depends very much on the context, i.e., the protocol > details and the security goal. > > > Chris P. > > > IMPORTANT NOTICE: The contents of this email and any attachments are > confidential and may also be privileged. If you are not the intended > recipient, please notify the sender immediately and do not disclose the > contents to any other person, use it for any purpose, or store or copy the > information in any medium. Thank you. >
_______________________________________________ TLS mailing list TLS@ietf.org https://www.ietf.org/mailman/listinfo/tls
