Naslov
A Comprehensive Symbolic Analysis of TLS 1.3

Autori
Cremers, Cas ; Horvat, Marko ; Hoyland, Jonathan ; Scott, Sam ; van der Merwe, Thyla

Vrsta, podvrsta i kategorija rada
Radovi u zbornicima skupova, cjeloviti rad (in extenso), znanstveni

Izvornik
CCS '17: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security / - New York (NY) : Association for Computing Machinery (ACM), 2017, 1773-1788

ISBN
978-1-4503-4946-8

Skup
2017 ACM SIGSAC Conference on Computer and Communications Security

Mjesto i datum
Dallas (TX), Sjedinjene Američke Države, 30.10.2017. - 03.11.2017

Vrsta sudjelovanja
Predavanje

Vrsta recenzije
Međunarodna recenzija

Ključne riječi
symbolic verification ; authenticated key exchange ; TLS 1.3

Sažetak
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 three 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 further this effort by constructing the most comprehensive, faithful, and modular symbolic model of the TLS 1.3 draft 21 release candidate, and use the Tamarin prover to verify the claimed TLS 1.3 security requirements, as laid out in draft 21 of the specification. In particular, our model covers all handshake modes of TLS 1.3. Our analysis reveals an unexpected behaviour, which we expect will inhibit strong authentication guarantees in some implementations of the protocol. In contrast to previous models, we providea novel way of making the relation between the TLS specification and our model explicit: we provide a fully annotated version of the specification that clarifies what protocol elements we modelled, and precisely how we modelled these elements. We anticipate this model artifact to be of great benefit to the academic community and the TLS Working Group alike.

Izvorni jezik
Engleski

Znanstvena područja
Matematika, Računarstvo

POVEZANOST RADA