Re: [TLS] Choice of Additional Data Computation

[Hanno Becker <[e-mail]>]

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. 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 - <[e-mail]>
Sent: Saturday, April 25, 2020 6:58 PM
To: Hanno Becker <[e-mail]>
Cc: Eric Rescorla <[e-mail]>; Hannes Tschofenig <[e-mail]>; [e-mail] <[e-mail]>
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.