Re: [TLS] Encrypt-then-MAC again (was Re: padding bug)

[Nikos Mavrogiannopoulos <[e-mail]>]

On Sat, 2013-11-30 at 17:29 +0000, Paterson, Kenny wrote:

> >Proven to be secure doesn't mean that attacks don't exist. The TLS
> >padding scheme was proven to be secure prior to be broken; ironically by
> >the same person who made the proof. Attacks work by playing outside the
> >requirements of the proof.
> 
> I assume here that you're referring to my "Tag size matters" paper with
> Ristenpart and Shrimpton, and then to the Lucky 13 paper here. OK, with
> some of my TLS credentials established for those who don't know me, here
> are the key points that I take away from the TLS proof (from that paper)
> versus the Lucky 13 attack:
> 
> The proof for MAC-then-Pad-then-Encrypt in TLS was extremely delicate and
> difficult to produce. Indeed, in generating it, we came up with another
> new attack on "TLS with short MACs" that excludes certain parameters from
> ever being secure. We then had to make an assumption for the proof to go
> through: that the decryption process does not leak the source of
> decryption failure (sanity check failure, bad pad, or bad MAC), or any of
> the timing involved in decryption.

Hello Kenny,
 Indeed, this is the paper I was referring to. Note however, that my
main point was not about any issue with the proof instead, but how
crypto proofs should be interpreted by non-hardcore-crypto experts. As
we are now, a proof in a cryptography field is not equivalent to a
proof, for example, in the language of mathematics, which is typically
accepted as a universal truth. 

> What the Lucky 13 attack showed is that achieving this "uniformity of
> errors" is very difficult for TLS's MAC-then-Pad-then-Encrypt construction.

Indeed, and the paper contributes a lot to our knowledge of the AtE
mode.

> And this is why MAC-then-Encrypt - and its real world variants - are being
> given such a hard time on this list by some, including me: our bitter
> experience is that implementing it securely is just much too hard. Witness
> Adam Langley's 500 line patch for OpenSSL and NSS to get this (finally)
> right. (Side note - Adam deserves credit for independently discovering the
> same attack vector that we used in Lucky 13.)
> To add a bit more detail: during the Lucky 13 disclosure process, I worked
> with many vendors to help them get their patches ready. Very few of them
> were actually able to completely eliminate timing side channels completely
> in their implementations, and all that I know of (except for Adam) settled
> for a "good enough" approach. Of course, that pragmatic approach is quite
> justifiable. But it may still leave open small windows of opportunity for
> future attack.

That's why I don't like this kind of fixes (having 500 or 1000 lines to
remove the CBC padding is unacceptable to me). Thus I find it natural
for an implementer to avoid such a fix, as he may accidentally introduce
more bugs than the one it solves.  This is the reason I would like to
see a proper fix in the protocol.

> Bottom line: none of the many issues that MAC-then-Pad-then-Encrypt has
> had in TLS should *ever* arise for Encrypt-then-MAC, unless the
> implementer was extremely ill-educated.

Indeed, but I believe the same point applies for AtE if AtE is seen as
Pad-then-MAC-then-Encrypt (thanks to your attacks and papers, this is
the only reasonable interpretation of AtE today).

> To me, the perceived dangers of exposing the MAC - dangers which neither I
> (nor any serious cryptographer I know) accept as being real - are far
> outweighed by the simplicity and robustness provided by an
> Encrypt-then-MAC approach.

I agree that if TLS would be redesigned today, that could be a very good
point. However, this is not the case. The issue at hand is a fix in the
CBC ciphersuites and I find it quite drastic change (*) to switch the
order of encryption and authentication in all ciphersuites just because
of an issue in the CBC ones. That's why I'd prefer a simple fix for the
issue at hand that is _known_ to be as secure as EtA for the ciphers we
use.

(*). drastic but acceptable for me though - see my previous posts.

> >Nevertheless, there is much more recent work on EtA vs AtE, that
> >actually proves AtE secure (not "generically" as you pose, you just need
> >a decent cipher). You may check "The order of encryption and
> >authentication for protecting communications (or: How secure is SSL?)".
> >There are even newer papers than that, it is just this that came to
> >mind.
> 
> This is too simplistic an interpretation of that paper by Hugo Krawczyk,
> I'm afraid. It's an excellent piece of work, and quite ahead of its time
> in trying to apply provable security techniques to a real protocol. But it
> has two major shortcomings if you try to apply it to CBC-mode encryption
> as used in TLS:
> 1. It does not consider TLS padding whatsoever - but instead assumes data
> is all block-aligned. As soon as you introduce padding in-between the MAC
> and the encryption, i.e. as in TLS's actual construction, you run into
> lots of trouble - Vaudenay, Bodo Moeller's observations, Lucky 13 and all.

This is true, but it is part of my argumentation as I consider AtE to be
pad-then-MAC-then-encrypt, can be seen as no padding whatsoever, the AtE
proof applies directly.

> 2. It assumes the MAC output size is the same as the block cipher's block
> size.

That I hadn't notice, and if it is not fixable, it is indeed a strong
counter-argument against pad-mac-then-encrypt.

> On the plus side, and perhaps this is what you were referring to, Hugo's
> analysis works just fine for stream-cipher based ciphersuites (as long as
> the stream cipher is good - so not RC4 then!). The Asiacrypt 2011 paper
> can be seen as extending his analysis to handle the actual construction
> used in TLS's CBC-mode ciphersuites, but with the important, necessary,
> and difficult-to-achieve proviso concerning uniformity of errors.

So as I understand your proof fixes the point (2), that you mentioned
above?

> But, at the risk of repeating myself, I very much prefer the simplicity
> and robustness of an Encrypt-then-MAC construction.
> Of course, this is just another opinion, like many others that have been
> expressed on this list recently, and I cannot hope it will be the last
> word on the subject. But I can hope that it's accepted as an opinion born
> from significant experience in analysing TLS security, from a variety of
> perspectives (theoretical, implementation, attacks).

I believe your opinion is greatly appreciated on this list (and of
course by me), so thanks for taking the time of expressing it. It is
nice to discuss with solid arguments.

best regards,
Nikos