Analysing TLS in the Strand Spaces Model

Abstract

In this paper, we analyse the Transport Layer Security (TLS) protocol within the strand spaces setting. In [BL03] Broadfoot and Lowe suggested an abstraction of TLS. The abstraction models the security services that appear to be provided by the protocol to the high-level security layers. The outcome of our analysis provides a formalisation of the security services provided by TLS and proves that, under reasonable assumptions, the abstract model suggested by Broadfoot and Lowe is correct. To that end, we reduce the complexity of the protocol using safe simplifying transformations. We extend the strand spaces model in order to include the cryptographic operations used in TLS and facilitate its analysis. Finally, we use the extended strand spaces model to fully analyse TLS with its two main components: the Handshake and Record Layer protocols.