An Analysis of TLS 1.3 and its use in Composite Protocols

The TLS protocol is one of the most important protocols today. This thesis is a study of TLS 1.3 and its use in composite protocols. The TLS protocol is intended to enable secure end-to-end communication over insecure networks, including the Internet. Unfortunately, this goal has been thwarted a number of times throughout the protocol's tumultuous lifetime, resulting in the need for a new version of the protocol, namely TLS 1.3. Over the past four years, in an unprecedented joint design effort with the academic community, the TLS Working Group has been working tirelessly to enhance the security of TLS.

We provide a comprehensive, faithful, and modular symbolic model of TLS 1.3, and use the Tamarin prover to verify the claimed TLS 1.3 requirements. Our analysis reveals a previously unreported unexpected behaviour, which inhibits strong authentication guarantees in some circumstances. In particular, participants cannot always derive their authentication status. We also provide a symbolic model of Exported Authenticators, a protocol that is layered on top of TLS to create a composite protocol, using the Tamarin prover to verify the claimed requirements. Our analysis requires us to define new authentication properties that allow us to capture the guarantees claimed by EAs. The results of our analysis show the same issue appears in EAs. We thus propose Layered EAs, an extension to EAs that allows participants to derive their authentication status. We provide a symbolic model of LEAs, and use the Tamarin prover to provide a partial proof of the claimed requirements.
We also propose a protocol composition that layers TLS 1.3 on top of a multi-party authentication protocol. This allows us to construct a TLS channel where the key is agreed between multiple parties, whilst preserving authentication and integrity. We compare and contrast this composition with three controversial proposals designed to achieve similar confidentiality guarantees.