Implementing and Proving the TLS 1.3 Record Layer

Explore a comprehensive analysis of the TLS 1.3 record layer implementation and security proofs in this IEEE Symposium on Security & Privacy conference talk. Delve into the core functionality of authenticated encryption in TLS, examining how streams of messages are fragmented, multiplexed, and encrypted with optional padding. Learn about the differences between TLS 1.3 and TLS 1.2, including the use of Authenticated Encryption with Associated Data (AEAD) and algorithms like AES-GCM and ChaCha20-Poly1305. Discover how new protocol features such as early application data and late handshake messages are handled. Gain insights into the verification process using F*, a dependency typed language, and understand how high-level security is reduced to cryptographic assumptions on ciphers. Follow the step-by-step reduction process, including functional correctness and injectivity properties of one-time MAC algorithms, security of generic AEAD construction, and extension to stream encryption and length-hiding multiplexed encryption. Examine the security model of the record layer against adversaries controlling TLS sub-protocols, and learn about concrete security bounds for various ciphersuites. Understand the implications of these findings on recommended data limits before re-keying. Explore the integration of this implementation into the miTLS library and its interoperability with popular web browsers.