Multi-Stage Key Exchange and the Case of Google's QUIC Protocol

The traditional approach to build a secure connection is to run a key exchange protocol and, once the key has been established, to use this key afterwards in a secure channel protocol. The security of key exchange and channel protocols, and to some extent also of the composition of both, has been scrutinized extensively in the literature. However, this approach usually falls short of capturing some key exchange protocols in which, due to practical motivation, the originally separated phases become intertwined and keys are established continuously. Two prominent examples of such protocols are TLS (with resumption), and Google's recently proposed low-latency protocol QUIC. In this work we revisit the previous security of model of Brzuska et al. (CCS'11) and expand it into a multi-stage key exchange model in the style of Bellare and Rogaway. In our model, parties can establish multiple keys in different stages and use these keys between stages, even to establish the next key. The advantage of using the formalization of Brzuska et al. is that it has been designed with the aim to provide compositional guarantees. Hence, we can, too, give sufficient conditions under which multi-stage key exchange protocols compose securely with any symmetric-key application protocol, like a secure channel protocol. We then exercise our model for the case of the QUIC protocol. Basically, we show that QUIC is an adequately secure multi-stage key exchange protocol and meets the suggested security properties of the designers. We continue by proposing some slight changes to QUIC to make it more amenable to our composition result and to allow reasoning about its security as a combined connection establishment protocol when composed with a secure channel protocol.