Formally Verifying the State Machine of TLS 1.3 Handshake in OpenSSL

The TLS handshake state machine manages the handshake messages exchanged in a session based on the parameters negotiated between the client and the server. Although the TLS 1.3 standard has undergone multiple rounds of analysis and revisions before official release to ensure its security, the process from natural language descriptions to implementations still relies on human expertise and is error-prone. In this paper, we propose a systematic method to conduct equivalence verification between the implementation of the TLS state machine and the standard. We also conduct formal verification of OpenSSL, the extensively utilized open-source TLS implementation for secure communications. Using Cryptol, we model the handshake state machine both from the standards and OpenSSL's implementation to perform its formal verification. Our automatic tool E-Verify performs equivalence verification by comparing the state transition sequences produced by the RFC model and OpenSSL model with all combinations of negotiation parameters. Guided by the verification results, we identify 640 mismatches out of a total of 1,536 scenarios and pinpoint the corresponding negotiation parameter combinations.