ODU CS 772 - Finite-State Analysis of SSL 3.0

Unformatted text preview:

Finite-State Analysis of SSL 3.0Abstract1 Introduction2 Outline of the methodology2.1 The Mur verification system2.2 The methodology2.3 The intruder modelNo cryptanalysis.No probabilities.No partial information.3 The SSL 3.0 handshake protocol 4 Modeling SSL 3.0 4.1 Notation4.2 Assumptions about cryptography 4.3 Protocol ABasic protocol (A)Attack on A4.4 Protocol BA + server authenticationAttack on B4.5 Protocol CB + client authenticationAttack on C 4.6 Protocol D C + post-handshake verification of plaintextAttack on D 4.7 Protocol ED + post-handshake verification of all messagesAttack on E4.8 Protocol F E + noncesAttack on F 4.9 Protocol Z (final)4.9.1 Protocol Z with resumption: cryptosuite attack 4.9.2 Protocol Z with resumption: version rollback attack 4.10 Protocol Z vs. SSL 3.0 5 Optimizing the intruder model6 ConclusionsAcknowledgmentsAppendix A: SSL 2.0New sessionResumed sessionResumed session with client authenticationAppendix B: master secret computation ReferencesAbout this document ...7th USENIX Security Symposium, 1998 [Technical Program] Pp. 201–216 of the ProceedingsFinite-State Analysis of SSL 3.0 John C. Mitchell, Vitaly Shmatikov, and Ulrich Stern Computer Science Department Stanford UniversityStanford, CA 94305 {jcm,shmat,uli}@cs.stanford.eduAbstractThe 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. 1 IntroductionIn previous work [9], a general-purpose finite-state analysis tool has been successfully applied to the verification of small security protocols such as the Needham-Schroeder public key protocol, Kerberos, and the TMN cellular telephone protocol. The tool, Mur [3, 10], was designed for hardware verificationand related analysis. In an effort to understand the difficulties involved in analyzing larger and more complex protocols, we use Mur to analyze the SSL 3.0 handshake protocol. This protocol is important, since it is the de facto standard for secure Internet communication, and a challenge, since it has more steps and greater complexity than the other security protocols analyzed using automated finite-state exploration. In addition to demonstrating that finite-state analysis is feasible for protocols of this complexity, our study also points to several anomalies in SSL 3.0. However, we have not demonstrated the possibility of compromising sensitive data in any implementation of the protocol. In the process of analyzing SSL 3.0, we have developed a ``rational reconstruction'' of the protocol. Morespecifically, after initially attempting to familiarize ourselves with the handshake protocol, we found that we could not easily identify the purpose of each part of certain messages. Therefore, we set out to use ouranalysis tool to identify, for each message field, an attack that could arise if that field were omitted from the protocol. Arranging the simplified protocols in the order of increasing complexity, we obtain anincremental presentation of SSL. Beginning with a simple, intuitive, and insecure exchange of the required data, we progressively introduce signatures, hashed data, and additional messages, culminating in a close approximation of the actual SSL 3.0 handshake protocol. In addition to allowing us to understand the protocol more fully in a relatively short period of time, this incremental reconstruction also provides some evidence for the ``completeness" of our analysis. Specifically, Mur exhaustively tests all possible interleavings of protocol and intruder actions, making sure that a set of correctness conditions is satisfied in all cases. It is easy for such analysis to be ``incomplete" by not checking all of the correctness conditions intended by the protocol designers or users. In developing our incremental reconstruction of SSL 3.0, we were forced to confirm the importance of each part of each message. In addition, since no formal or high-level description of SSL 3.0 was available, we believe that the description of SSL 3.0 that we extracted from the Internet Draft [6] may be of interest. Our analysis covers both the standard handshake protocol used to initiate a secure session and the shorter protocol used to resume a session [6, Section 5.5,]. Mur analysis uncovered a weak form of version rollback attack (see Section 4.9.2) that can cause a version 3.0 client and a version 3.0 server to commit to SSL 2.0 when the protocol is resumed. Another attack on the resumption protocol (described in Sections 4.8 and 4.9.1) is possible in SSL implementations that strictly follow the Internet draft [6] and allow the participants to send application data without waiting for an acknowledgment of their Finished messages. Finally, an attack on cryptographic preferences (see Section 4.6) succeeds if the participants support weak encryption algorithms which can be broken in real time. Apart from these three anomalies, we were not able to uncover any errors in our final protocol. Since SSL 3.0 was designed to be backward-compatible, we also implemented and checked a full model for SSL 2.0 as part of the SSL 3.0 project. In the process, Mur uncovered the major problems with SSL 2.0 that motivated the design of SSL 3.0. Our Mur analysis of SSL is based on the assumption that cryptographic functions cannot be broken. Forthis and other reasons (discussed below), we cannot claim that we found all attacks on SSL. But our analysis has been efficient in helping discover an important class of attacks. The two prior analyses of SSL 3.0 that we are aware of are an informal assessment carried out by Wagnerand Schneier [14] and a formal analysis by Dietrich using a form of belief logic [2]. (We read the Wagnerand Schneier study before carrying out our analysis, but did not become aware of the Dietrich study until after we had completed the bulk of our work.) Wagner and Schneier comment on the possibility of anomalies


View Full Document

ODU CS 772 - Finite-State Analysis of SSL 3.0

Download Finite-State Analysis of SSL 3.0
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Finite-State Analysis of SSL 3.0 and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Finite-State Analysis of SSL 3.0 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?