We're sorry but this page doesn't work properly without JavaScript enabled. Please enable it to continue.
Feedback

Design and verification of the TLS 1.3 handshake state machine in LibreSSL

Formal Metadata

Title
Design and verification of the TLS 1.3 handshake state machine in LibreSSL
Title of Series
Number of Parts
34
Author
License
CC Attribution 3.0 Unported:
You are free to use, adapt and copy, distribute and transmit the work or content in adapted or unchanged form for any legal purpose as long as the work is attributed to the author in the manner specified by the author or licensor.
Identifiers
Publisher
Release Date
Language

Content Metadata

Subject Area
Genre
Abstract
The TLS 1.3 handshake is the protocol used for negotiating a TLS 1.3 connection between a client and a server. During the handshake the configuration for the session is agreed upon, ephemeral secrets are exchanged and the server is authenticated. This protocol is encoded in a state machine. After a general discussion of TLS and in particular a comparison of TLS 1.2 and TLS 1.3, this talk will review the TLS 1.3 handshake state machine and discuss its implementation in LibreSSL. Benefits and drawbacks of both the handshake protocol and LibreSSL's implementation will be discussed. We will also elaborate on the way we verify and guarantee our implementation's correctness using regression testing and other methods.