«A DISSERTATION SUBMITTED TO THE DEPARTMENT OF COMPUTER SCIENCE AND THE COMMITTEE ON GRADUATE STUDIES OF STANFORD UNIVERSITY IN PARTIAL FULFILLMENT OF ...»
SECURITY ANALYSIS OF NETWORK PROTOCOLS:
COMPOSITIONAL REASONING AND
SUBMITTED TO THE DEPARTMENT OF COMPUTER SCIENCE
AND THE COMMITTEE ON GRADUATE STUDIES
OF STANFORD UNIVERSITY
IN PARTIAL FULFILLMENT OF THE REQUIREMENTS
FOR THE DEGREE OF
DOCTOR OF PHILOSOPHYAnupam Datta September 2005 c Copyright by Anupam Datta 2005 All Rights Reserved ii I certify that I have read this dissertation and that, in my opinion, it is fully adequate in scope and quality as a dissertation for the degree of Doctor of Philosophy.
John C. Mitchell (Principal Adviser) I certify that I have read this dissertation and that, in my opinion, it is fully adequate in scope and quality as a dissertation for the degree of Doctor of Philosophy.
Dan Boneh I certify that I have read this dissertation and that, in my opinion, it is fully adequate in scope and quality as a dissertation for the degree of Doctor of Philosophy.
David L. Dill Approved for the University Committee on Graduate Studies.
iii iv Abstract This dissertation addresses two central problems associated with the design and security analysis of network protocols that use cryptographic primitives. The ﬁrst problem pertains to the secure composition of protocols, where the goal is to develop methods for proving properties of complex protocols by combining independent proofs of their parts. In order
to address this problem, we have developed a framework consisting of two formal systems:
Protocol Derivation System (PDS) and Protocol Composition Logic (PCL). PDS supports syntactic derivations of complex protocols, starting from basic components, and combining or extending them using a sequence of composition, reﬁnement, and transformation operations. PCL is a Floyd-Hoare style logic that supports axiomatic proofs of protocol properties. The eventual goal is to develop proof methods for PCL for every derivation operation in PDS, thereby enabling the parallel development of protocols and their security proofs. In this dissertation, we present proof methods for reasoning about protocol composition and a class of protocol reﬁnements. The composition theorems are formulated and proved by adapting ideas from the assume-guarantee paradigm for reasoning about distributed systems. PDS and PCL have been successfully applied to a number of industrial network security protocols, in several instances identifying serious security vulnerabilities.
The second problem pertains to the computational soundness of symbolic protocol analysis. At a high-level, this means that a logical method for protocol analysis should have an associated soundness theorem, which guarantees that a completely symbolic analysis or proof has an interpretation in the standard complexity-theoretic model of modern cryptography. Our approach to this problem involves deﬁning complexity-theoretic semantics and proving a soundness theorem for a variant of PCL which we call Computational PCL.
v While the basic form of the logic remains unchanged, there are certain important differences involving the interpretation of implication in terms of conditional probability and the semantics of the predicates used to capture secrecy properties.
The ﬁnal result in the dissertation spans both the problems. An alternative way of specifying and reasoning about protocol composition is through equivalence or simulation between the real protocol and an ideal protocol, which is secure by construction. We prove that, under reasonable assumptions about the communication model, three simulationbased deﬁnitions for protocol security–universal composability, black-box simulatability, and process observational equivalence–express the same properties of a protocol. The proofs are axiomatic and are carried out using process calculus equational principles. Since these equational principles are rather general, the proofs carry over to a number of process calculi, in particular, the probabilistic poly-time process calculus, whose execution model is consistent with the complexity-theoretic model of cryptography. We also observe certain important differences between the composition paradigm of universal composability, and the assume-guarantee paradigm of PCL.
I would like to thank my advisor, John Mitchell, for valuable guidance. I have learnt a lot from him. I would also like to thank the faculty members on my reading and orals committees: Dan Boneh, David Dill, Rajeev Motwani, and Stanley Peters for providing feedback on the research results. Additional thanks to Dan and David for teaching an excellent set of courses which helped me greatly in my research. I would also like to express my gratitude towards Dusko Pavlovic and Andre Scedrov for providing direction and advice. Much of the work on the logic and derivation system presented in this dissertation was carried out in collaboration with Dusko.
I was fortunate to be part of a very active research group here at Stanford. I have worked closely with and learnt a lot from several students, postdocs and visitors in our group. Special thanks to Ante Derek and Ajith Ramanathan for the excellent brain-storming sessions and the fun times. Each chapter in this dissertation is joint work with at least one of them.
Thanks also to Andrei Aron, Dan Auerbach, Michael Backes, Adam Barth, Changhua He, Cary Kempston, Ralf K¨ sters, Mathieu Turuani, Arnab Roy, Vitaly Shmatikov, Mukund u Sundararajan, and Bogdan Warinschi for fruitful collaborations and interesting conversations.
I would also like to express my gratitude towards several faculty members at IIT Kharagpur who got me excited about research and who continue to provide encouragement. Finally, I would like to thank my friends for their company, and my (extended) family for unconditional support and understanding over the years.
4.1 Illustrating the Methodology......................... 59
4.2 Instantiations of the Challenge-Response template.............. 62
4.3 Protocol that is an instantiation of both CR and ENC templates....... 65
4.4 Instantiations of authenticated key-exchange templates........... 68
Introduction Protocols that enable secure communication over an untrusted network constitute an important part of the current computing infrastructure. Common examples of such protocols are SSL , TLS , Kerberos , and the IPSec  and IEEE 802.11i  protocol suites. SSL and TLS are used by internet browsers and web servers to allow secure transactions in applications like online banking. The IPSec protocol suite provides conﬁdentiality and integrity at the IP layer and is widely used to secure corporate VPNs. IEEE 802.11i provides data protection and integrity in wireless local area networks, while Kerberos is used for network authentication.
The design and security analysis of such network protocols presents a difﬁcult problem. In several instances, serious security vulnerabilities were uncovered in protocols many years after they were ﬁrst published or deployed [105, 59, 1, 16, 104, 68]. While some of these attacks rely on subtle properties of cryptographic primitives, a large fraction can be traced to intricacies in designing protocols that are robust in a concurrent execution setting.
To further elaborate this point, let us consider the concrete example of the SSL protocol.
In SSL, a client typically sets up a key with a web server. That key is then used to protect all data exchanged between them. A single client can simultaneously engage in sessions with multiple servers and a single server concurrently serves many clients. Let us consider a scenario in which all network trafﬁc is under the control of the adversary. In addition, the adversary may also control some of the clients and servers. The protocol should guarantee certain security properties for honest agents even in such an adversarial environment.
CHAPTER 1. INTRODUCTIONSpeciﬁcally, if an honest client executes an SSL session with an honest server, the attacker should not be able to recover the exchanged key. This is called the key secrecy property.
Furthermore, an attacker should not be able to fool an honest client into believing that she has completed a session with an honest server unless that is indeed the case. This property is called authentication. The security proof that SSL does indeed provide these guarantees, even when the cryptography is perfect, turns out to be far from trivial [108, 60]. The central problem is ensuring that the attacker cannot combine data acquired from a possibly unbounded number of concurrent sessions to subvert the protocol goals.
Over the last two decades, a variety of methods and tools have been developed for analyzing the security guarantees provided by network protocols. The main lines of work include specialized logics [24, 121, 55], process calculi [6, 3, 77, 116] and tools [89, 119], as well as theorem-proving [110, 109] and model-checking methods [79, 102, 117, 118] using general purpose tools. (The cited papers are representative but not exhaustive; see  for a more comprehensive survey.) There are several points of difference among these approaches. While most model-checking tools can only analyze a ﬁnite number of concurrent sessions of a protocol, some of the logics, process calculi, and theorem-proving techniques yield protocol security proofs without bounding the number of sessions. With the exception of the BAN family of logics , most approaches involve explicit reasoning about possible attacker actions. Finally, while security properties are interpreted over individual traces in the majority of these methods, in the process calculi-based techniques, security is deﬁned by an equivalence relation between a real protocol and an ideal protocol, which is secure by construction. Inspite of these differences, all of these approaches use the same symbolic model of protocol execution and attack. This model seems to have developed from positions taken by Needham-Schroeder , Dolev-Yao , and much subsequent work by others. In this model, the adversary is allowed to choose non-deterministically among the set of possible actions; messages are represented as
terms, not sequences of bits;
and encryption and other cryptographic primitives are modelled in an abstract black-box manner. This idealization has been a major enabling factor in the development of the above mentioned array of tools and techniques.
As this research area comes of age, several important open problems have been identiﬁed (cf. ). One signiﬁcant problem has to do with secure composition of protocols.
Many modern protocols like IKEv2 , IEEE 802.11i , and Kerberos  comprise of several different sub-protocols and modes of operation. The challenge is to develop proof methods that allow security proofs of such composite protocols to be built up by combining independent proofs of their parts. Composition is a difﬁcult problem in security since a component may reveal information that does not affect its own security but may degrade the security of some other component in the system. A second important problem pertains to the model of protocol execution and attack used while carrying out the security analysis task. As mentioned before, almost all extant approaches for symbolic protocol analysis use an idealized model where cryptography is assumed to be perfect. This idealization makes the protocol analysis problem more amenable to automation. However, the abstraction detracts from the ﬁdelity of the analysis since attacks arising from the interaction between the cryptosystem and the protocol lie outside the scope of this model. The goal then is to develop logical methods for protocol analysis with associated soundness theorems, which guarantee that a completely symbolic analysis or proof has an interpretation in the standard complexity-theoretic model of modern cryptography. At an informal level, this means that a machine-checkable or generated proof should carry the same meaning as a hand-proof done by a cryptographer. This turns out to be a difﬁcult problem since the security deﬁnitions of cryptographic primitives and protocols involve complex probability spaces and quantiﬁcation over all probabilistic polynomial time attackers. In this dissertation, we initiate a program and take several steps towards solving these two problems. In the following paragraphs, we summarize our main results and sketch several directions for future work.
We have developed a framework consisting of two formal systems: Protocol Derivation System (PDS) and Protocol Composition Logic (PCL). Within the protocol analysis spectrum, this work can be placed in the category of specialized logics. PDS supports syntactic derivations of complex protocols, starting from basic components, and combining or extending them using a sequence of composition, reﬁnement, and transformation operations. PCL is a Floyd-Hoare style logic [52, 64] that supports axiomatic proofs of protocol properties. The eventual goal is to develop proof methods for PCL for every derivation operation in PDS, thereby enabling the parallel development of protocols and their security proofs. In this dissertation, we present proof methods for reasoning about protocol composition and a class of protocol reﬁnements. The composition theorems are