Finite-State Analysis of SSL 3.0

Authors: 

John C. Mitchell, Vitaly Shmatikov, and Ulrich Stern, Stanford University

Abstract: 

The Secure Sockets Layer (SSL) protocol is analyzed using a finite-state enumeration tool called Murtex2html_wrap_inline1336 . The analysis is presented using a sequence of incremental approximations to the SSL 3.0 handshake protocol. Each simplified protocol is ``model-checked'' using Murtex2html_wrap_inline1336 , with the next protocol in the sequence obtained by correcting errors that Murtex2html_wrap_inline1336 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.

BibTeX
@inproceedings {261405,
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
}
Download

Links

Paper: 
http://usenix.org/publications/library/proceedings/sec98/full_papers/mitchell/mitchell.pdf
Paper (HTML): 
http://usenix.org/publications/library/proceedings/sec98/full_papers/mitchell/mitchell_html/mitchell.html