(De-)Constructing TLS.

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