An Analysis of TLS 1.3 and its use in Composite Protocols. / Hoyland, Jonathan.

2018. 273 p.

Research output: ThesisDoctoral Thesis

Unpublished

Standard

An Analysis of TLS 1.3 and its use in Composite Protocols. / Hoyland, Jonathan.

2018. 273 p.

Research output: ThesisDoctoral Thesis

Harvard

Hoyland, J 2018, 'An Analysis of TLS 1.3 and its use in Composite Protocols', Ph.D., Royal Holloway, University of London.

APA

Vancouver

Author

BibTeX

@phdthesis{0f7684c239dd4e1ca6638f2a1f9cd88f,
title = "An Analysis of TLS 1.3 and its use in Composite Protocols",
abstract = "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.",
keywords = "Formal Analysis, TLS 1.3, TLS, Protocol analysis, Composite Protocols, Computer Security",
author = "Jonathan Hoyland",
year = "2018",
language = "English",
school = "Royal Holloway, University of London",

}

RIS

TY - THES

T1 - An Analysis of TLS 1.3 and its use in Composite Protocols

AU - Hoyland, Jonathan

PY - 2018

Y1 - 2018

N2 - 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.

AB - 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.

KW - Formal Analysis

KW - TLS 1.3

KW - TLS

KW - Protocol analysis

KW - Composite Protocols

KW - Computer Security

M3 - Doctoral Thesis

ER -