(De-)Constructing TLS

TLS is one of the most widely deployed cryptographic protocols on the Internet; it is used to protect the con dentiality and integrity of transmitted data in various client-server protocols. Its non-standard use of cryptographic primitives, however, makes it hard to formally assess its security. It is in fact dicult to use traditional (well-understood) securitybr /> notions for the key-exchange (here: handshake) and the encryption/authentication (here:br /> record layer ) parts of the protocol due to the fact that, on the one hand, traditional gamebasedbr /> notions do not easily support composition, and on the other hand, all TLS versionsbr /> up to and including 1.2 combine the two phases in a non-standard way.br /> In this paper, we provide a modular security analysis of the handshake in TLS version 1.2br /> and a slightly sanitized version of the handshake in the current draft of TLS version 1.3,br /> following the constructive cryptography approach of Maurer and Renner (ICS 2011). Webr /> provide a deconstruction of the handshake into modular sub-protocols and a security proofbr /> for each such sub-protocol. We also show how these results can be combined with analysesbr /> of the respective record layer protocols, and the overall result is that in all cases thebr /> protocol constructs (unilaterally) secure channels between the two parties from insecurebr /> channels and a public-key infrastructure. This approach ensures that (1) each sub-protocolbr /> is proven in isolation and independently of the other sub-protocols, (2) the overall securitybr /> statement proven can easily be used in higher-level protocols, and (3) TLS can be used inbr /> any composition with other secure protocols.br /> In more detail, for the key-exchange step of TLS 1.2, we analyze the RSA-based andbr /> both Die-Hellman-based variants (with static and ephemeral server key share) under abr /> non-randomizability assumption for RSA-PKCS and the Gap Die-Hellman assumption,br /> respectively; in all cases we make use of random oracles. For the respective step of TLS 1.3,br /> we prove security under the Decisional Die-Hellman assumption in the standard model. Inbr /> all statements, we require additional standard computational assumptions on other primitives.br /> In general, since the design of TLS is not modular, the constructive decomposition isbr /> less ne-grained than one might wish to have and than it is for a modular design. This paperbr /> therefore also suggests new insights into the intrinsic problems incurred by a non-modularbr /> protocol design such as that of TLS./p