[Cfrg] Talk at Real-World Crypto (was Re: Requesting removal of CFRG co-chair)

[Douglas Stebila <[e-mail]>]

On Jan 5, 2014, at 8:05 PM, David McGrew <[e-mail]> wrote:

> (An aside: I'd like to hear or read about Provable security of advanced properties of TLS and SSH, which I would guess is similar http://eprint.iacr.org/2013/813.pdf)

I'll post a link to the slides on the mailing list after the talk.

But as a preview: I'll talk about two recent related papers, one of which is the one you identified on multi-ciphersuite security and SSH (http://eprint.iacr.org/2013/813), and the other of which is on TLS renegotiation (http://eprint.iacr.org/2012/630).

Starting in 2012, there's been a series of papers aiming to prove the security of various TLS ciphersuites without alteration.  The original paper by Jager et al. at CRYPTO 2012 defined an appropriate security model (called Authenticated and Confidential Channel Establishment (ACCE)) and proved that signed-Diffie-Hellman ciphersuites are secure ACCE protocols, assuming that all of the individual building blocks are suitably secure.  Since then, there have been more papers aiming to analyze the other categories of ciphersuites, including the Krawczyk et al. paper at CRYTPO 2013 that Hoeteck Wee will present at Real World Crypto and Kohlar et al.'s 2013 eprint, both of which analyze RSA key transport and static DH; and there will be a paper at PKC 2014 on pre-shared key ciphersuites.

So from that line of work, we are learning that most TLS ciphersuites combine their primitives in acceptable ways.

My talk will discuss what happens when we look beyond individual ciphersuites in isolation.  For example, we know from the renegotiation attack of Ray and Dispensa in 2009 that some TLS-reliant applications are vulnerable to injection attacks due to how TLS originally did renegotiation.  Similarly, there was a paper by Mavrogiannopolous et al. at ACM CCS 2012 that did a cross-ciphersuite attack on TLS, showing how signed ECDH parameters could be reinterpreted as valid signed DH parameters.  Both of these attacks work despite the above proofs of ACCE security of the corresponding TLS ciphersuites, because the ACCE security model focuses on the ciphersuites used in isolation.

In the first part of the talk, I'll talk about our work on TLS renegotiation (http://eprint.iacr.org/2012/630).  Starting from the perspective of the formal ACCE security model, we wanted to understand why the model didn't catch the renegotiation attack.  We then extended the model to cover renegotiation, and proved that the SCSV/RIE (Signalling Ciphersuite Value / Renegotiation Indication Extension) fixes that were standardized do provide security in our renegotiation model.  (We have an even stronger model of renegotiation security that the SCSV/RIE fixes don't satisfy, but this model is only relevant if you want to detect injection attacks when renegotiating even if the current session key has been compromised, which is admittedly a corner case).

In the second part of the talk, I'll talk about our work on multi-ciphersuite security (http://eprint.iacr.org/2013/813).  We know from the ACCE line of work that various TLS ciphersuites are individually secure.  But we also know from the Mavrogiannopolous attack that there are attacks when multiple ciphersuites use the same long-term authentication keys, as is very common in practice.  Therefore ACCE security of individual ciphersuites doesn't generically imply simultaneous security of many ciphersuites re-using long-term authentication keys; under what conditions can we get multi-ciphersuite security?  We construct a composition framework for ACCE-like ciphersuites and identify conditions under which they are secure even with long-term key re-use.  Intuitively, if the thing that is signed uniquely identifies the ciphersuite that it's intended for, then it is safe to re-use that long-term key.  This isn't surprising; protocol designers have known this for a while.  But we can formalize this and use it to prove a composition theorem.  Since multi-ciphersuite security of signed-DH ciphersuites in TLS is ruled out by the Mavrogiannopolous attack, we instead look at SSH.  It turns out that the thing that is signed in SSH does indeed uniquely identify the ciphersuite it's for, and we can apply the composition theorem.  As part of this, we give the first proof of ACCE security of individual SSH ciphersuites (again under the assumption that the cryptographic primitives are secure), and then the composition theorem says that these ciphersuites are simultaneously secure, even when long-term keys are re-used across ciphersuites.

Douglas