Finite-state analysis of SSL 3.0
John C. Mitchell, Vitaly Shmatikov, Ulrich Stern · 1998
The Secure Sockets Layer (SSL) protocol is analyzed using a finite-state enumeration tool called Murphi. The analysis is presented using a sequence of incremental approximations to the SSL 3.0 handshake protocol. Each simplified protocol is "model-checked" using Murphi, with the next protocol in the sequence obtained by correcting errors that Murphi finds automatically. This process identifies the main shortcomings in SSL 2.0 that led to the design of SSL 3.0, as well as a few anomalies in the protocol that is used to resume a session in SSL 3.0. In addition to some insight into SSL, this study demonstrates the feasibility of using formal methods to analyze commercial protocols.