Naslov
Automated Analysis and Verification of TLS 1.3: 0-RTT, Resumption and Delayed Authentication

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

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

Skup
2016 IEEE Symposium on Security and Privacy (SP)

Mjesto i datum
San Jose (CA), Sjedinjene Američke Države, 23.05.2016. - 25.05.2016

Vrsta sudjelovanja
Predavanje

Vrsta recenzije
Međunarodna recenzija

Ključne riječi
security protocols ; verification ; TLS 1.3

Sažetak
After a development process of many months, the TLS 1.3 specification is nearly complete. To prevent past mistakes, this crucial security protocol must be thoroughly scrutinised prior to deployment. In this work we model and analyse the latest draft of the TLS 1.3 specification, namely revision 10, using the Tamarin prover, a tool for the automated analysis of security protocols. We specify and analyse the interaction of various handshake modes for an unbounded number of concurrent TLS connec- tions. We show that revision 10 meets the goals of authenticated key exchange in both the unilateral and mutual authentication cases. We extend our model to incorporate the desired delayed client authentication mechanism, a feature that is likely to be included in the next revision of the specification, and uncover a potential attack in which an adversary is able to successfully impersonate a client during a PSK-resumption handshake. This observation was reported to, and confirmed by, the IETF TLS Working Group. Our work not only provides the first supporting evidence for the security of several complex protocol mode interactions in TLS 1.3, but also shows the strict necessity of recent sugges- tions to include more information in the protocol’s signature contents.

Izvorni jezik
Engleski

Znanstvena područja
Matematika, Računarstvo

POVEZANOST RADA