Finite-State Analysis of SSL 3.0
John C. Mitchell, Vitaly Shmatikov, and Ulrich Stern, Stanford University
The Secure Sockets Layer (SSL) protocol is analyzed using a
finite-state enumeration tool called Mur
.
The analysis is presented using a sequence of incremental
approximations to the SSL 3.0 handshake protocol.
Each simplified protocol is ``model-checked'' using Mur ,
with the next protocol in the sequence obtained by correcting
errors that Mur 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.
author = {John C. Mitchell and Vitaly Shmatikov and Ulrich Stern},
title = {{Finite-State} Analysis of {SSL} 3.0},
booktitle = {7th USENIX Security Symposium (USENIX Security 98)},
year = {1998},
address = {San Antonio, TX},
url = {https://www.usenix.org/conference/7th-usenix-security-symposium/finite-state-analysis-ssl-30},
publisher = {USENIX Association},
month = jan
}