Multiple Handshakes Security of TLS 1.3 Candidates

The Transport Layer Security (TLS) protocol is by far the most widely deployed protocol for securing communications and the Internet Engineering Task Force (IETF) is currently developing TLS 1.3 as the next-generation TLS protocol. The TLS standard features multiple modes of handshake protocols and supports many combinational running of successive TLS handshakes over multiple connections. Although each handshake mode is now well-understood in isolation, their composition in TLS 1.2 remains problematic, and yet it is critical to obtain practical security guarantees for TLS. In this paper, we present the first formal treatment of multiple handshakes protocols of TLS 1.3 candidates. First, we introduce a multi-level&stage security model, an adaptation of the BellareRogaway authenticated key exchange model, covering all kinds of compositional interactions between different TLS handshake modes and providing reasonably strong security guarantees. Next, we prove that candidate handshakes of TLS 1.3 draft meet our strong notion of multiple handshakes security. Our results confirm the soundness of TLS 1.3 security protection design. Such a multi-level&stage approach is convenient for analyzing the compositional design of the candidates with different session modes, as they establish dependencies of multiple sessions. We also identify the triple handshake attack of Bhargavan et al. on TLS 1.2 within our multiple handshakes security model. We show generically that the proposed fixes (RFC 7627) for TLS 1.2 offer good protection against multiple handshakes attacks.