You are looking at a specific version 20140108:174918 of this paper. See the latest version.

Paper 2014/020

(De-)Constructing TLS

Markulf Kohlweiss and Ueli Maurer and Cristina Onete and Bjoern Tackmann and Daniele Venturi

Abstract

One of the most important applications of cryptography is the establishment of secure communication channels between two entities (e.g. a client and a server), and the protocol most widely used for this purpose is TLS. A key goal of research in cryptography is to provide security proofs for cryptographic protocols. This task is particularly difficult if the considered protocol has not been designed with provable security in mind, as is the case for TLS. Results on provable security differ with respect to (1) the assumptions made and (2) the statement that is proved to follow from the assumptions. It is important that the proved statement is of a form that allows for both comparisons of protocol performance, and for direct use in the proof of a higher-level protocol. Security statements should thus be exact (as opposed to asymptotic), giving precise upper bounds for the security level guaranteed by a protocol. Furthermore, a key to analyzing and designing cryptographic protocols is a modularization in which the role of each cryptographic primitive (e.g. encryption) or mechanism (e.g. nonce exchange) is made explicit, and the security of its application is proved in isolation, once and for all. The constructive cryptography framework provides a sound instantiation of this approach. A modular step constructs a specific resource from certain (assumed) resources, and the overall protocol is the composition of several such construction steps. The security proof for the overall protocol follows directly from the composition theorem as well as the individual (reasonably simple) security proofs for the modules. Moreover, the actual security statement for the overall protocol is of a standardized form, in terms of a resource, which makes it straight-forward to use the protocol in a higher-level context, with the overall security proof again following from the composition theorem. In this paper, we provide such a constructive treatment of TLS. We provide a deconstruction of TLS into modular steps and a security proof for each step which, compared to previous work, results in the above mentioned advantages. For the key-exchange step in particular, we analyze the RSA-based and both Diffie-Hellman-based variants (with static and ephemeral server key) under a non-randomizability assumption for RSA-PKCS and the Gap Diffie-Hellman assumption, respectively; in all cases we make use of random oracles. In general, since the design of TLS is not modular, the constructive decomposition is less fine-grained than one might wish to have and than it is for a modular design. This paper therefore also suggests new insights into the intrinsic problems incurred by a non-modular protocol design such as that of TLS.

Metadata
Available format(s)
PDF
Category
Cryptographic protocols
Publication info
Preprint. MINOR revision.
Keywords
TLS
Contact author(s)
bjoernt @ inf ethz ch
History
2015-04-22: revised
2014-01-08: received
See all versions
Short URL
https://ia.cr/2014/020
License
Creative Commons Attribution
CC BY
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.