Check out the new USENIX Web site.

Home About USENIX Events Membership Publications Students
7th USENIX Security Symposium, San Antonio, Texas

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 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.
  • View the full text of this paper in HTML form and PDF form.

  • If you need the latest Adobe Acrobat Reader, you can download it from Adobe's site.

  • To become a USENIX Member, please see our Membership Information.

?Need help? Use our Contacts page.

Last changed: 12 April 2002 aw
Technical Program
Conference Index