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

Explore a comprehensive analysis of TLS 1.3 security features in this 19-minute IEEE conference talk. Delve into the automated verification of key aspects such as 0-RTT, resumption, and delayed authentication using the Tamarin prover. Learn about the modeling and analysis of revision 10 of the TLS 1.3 specification, including the interaction of various handshake modes for concurrent TLS sessions. Discover the findings on authenticated key exchange in both unilateral and mutual authentication scenarios. Examine the potential attack uncovered in the delayed client authentication mechanism and its implications for PSK-resumption handshakes. Gain insights into the importance of recent suggestions for enhancing protocol signature contents and the overall security of TLS 1.3.