WWW.ABSTRACT.XLIBX.INFO
FREE ELECTRONIC LIBRARY - Abstract, dissertation, book
 
<< HOME
CONTACTS



Pages:   || 2 | 3 | 4 | 5 |   ...   | 17 |

«A DISSERTATION SUBMITTED TO THE DEPARTMENT OF COMPUTER SCIENCE AND THE COMMITTEE ON GRADUATE STUDIES OF STANFORD UNIVERSITY IN PARTIAL FULFILLMENT OF ...»

-- [ Page 1 ] --

SECURITY ANALYSIS OF NETWORK PROTOCOLS:

COMPOSITIONAL REASONING AND

COMPLEXITY-THEORETIC FOUNDATIONS

A DISSERTATION

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 PHILOSOPHY

Anupam 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 first 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, refinement, 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 refinements. 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 defining 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 final 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 definitions 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.

viAcknowledgements

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 [53], TLS [44], Kerberos [106], and the IPSec [73] and IEEE 802.11i [1] 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 confidentiality 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 difficult problem. In several instances, serious security vulnerabilities were uncovered in protocols many years after they were first 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 traffic 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. INTRODUCTION

Specifically, 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 [91] for a more comprehensive survey.) There are several points of difference among these approaches. While most model-checking tools can only analyze a finite 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 [24], 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 defined 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 [105], Dolev-Yao [47], 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

Abstract

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 identified (cf. [91]). One significant problem has to do with secure composition of protocols.

Many modern protocols like IKEv2 [71], IEEE 802.11i [1], and Kerberos [106] 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 difficult 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 fidelity 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 difficult problem since the security definitions of cryptographic primitives and protocols involve complex probability spaces and quantification 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, refinement, 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 refinements. The composition theorems are

CHAPTER 1. INTRODUCTION



Pages:   || 2 | 3 | 4 | 5 |   ...   | 17 |


Similar works:

«THE CURSE ON THE SERPENT (GENESIS 3:15) IN BIBLICAL THEOLOGY AND HERMENEUTICS by John L. Ronning A Dissertation Submitted to the Faculty of WESTMINSTER THEOLOGICAL SEMINARY in Partial Fulfillment of the Requirements for the Degree DOCTOR OF PHILOSOPHY Dedication For Linda, with deep appreciation ABSTRACT Gen 3:15, the second half of the curse on the serpent, pronounced in the Garden of Eden, has been interpreted in a number of quite different ways, and the predominant position and interests of...»

«Divine Exposures: Religion and Imposture in Colonial India by Joshua Barton Scott Department of Religion Duke University Date:_Approved: _ Dr. Bruce Lawrence, Supervisor _ Dr. Leela Prasad _ Dr. Richard Jaffe _ Dr. David Gilmartin _ Dr. Srinivas Aravamudan Dissertation submitted in partial fulfillment of the requirements for the degree of Doctor of Philosophy in the Department of Religion in the Graduate School of Duke University i v ABSTRACT Divine Exposures: Religion and Imposture in Colonial...»

«DIPLOMARBEIT Titel der Diplomarbeit „Nacido en Cuba. Made in the U.S.A.”: Exil und Identität in kubanoamerikanischer Prosa nach 1990 Verfasser Hermann Christian Sileitsch Angestrebter akademischer Grad Magister der Philosophie (Mag. phil.) Wien, 30. Oktober 2008 Studienkennzahl lt. Studienblatt: A 393 Studienrichtung lt. Studienblatt: Vergleichende Literaturwissenschaft Betreuer: Ao. Prof. Dr. Norbert Bachleitner -2Inhaltsverzeichnis Einleitung 1. Grundlegendes zu einer Theorie der...»

«    The challenge of web design guidelines:  Investigating issues of awareness,  interpretation, and efficacy      by Stephen James Szigeti   A thesis submitted in conformity with the requirements for the degree of Doctor of Philosophy Faculty of Information University of Toronto © Copyright by Stephen James Szigeti 2012 The challenge of web design guidelines:  Investigating issues of awareness, interpretation, and efficacy    Stephen James Szigeti Doctor of...»

«carl spaeter gmbh carl spaeter gmbh Spaeter Gruppe: Ausbildung duales Studium Carl Spaeter GmbH Personalabteilung Philosophenweg 17 47051 Duisburg Branche: Handel und Distribution Mitarbeiter: bundesweit ca. 1.700 Mitarbeiter Spaeter Duisburg: Willkommen SPAETER Duisburg. Wir handeln für Ihren Erfolg. SPAETER Duisburg und Hebels Stahlservice präsentieren sich vom 15. bis zum 18. März gemeinsam auf der Spaeter Bietigheim: Unternehmen CARL SPAETER GmbH CARL SPAETER GmbH. Höpfigheimer Straße...»

«DIPLOMARBEIT „Die Israelitische Kultusgemeinde Horn“ Eva Zeindl angestrebter akademischer Grad Magistra der Philosophie (Mag.phil.) Wien, 2008 Studienkennzahl lt. A 312 295 Studienblatt: Betreuerin / Betreuer: emer. o. Univ.-Prof. Dr. Gerald Stourzh Inhalt 1. Die jüdische Bevölkerung in Niederösterreich 1.1. Die gesetzliche Rahmenbedingungen 1.2. Israelitische Kultusgemeinden 2. Die jüdische Bevölkerung im politischen Bezirk Horn. 11 2.1. Demographische Entwicklung zwischen den Jahren...»

«ABSTRACT Title of dissertation: AN INVESTIGATION OF INHIBITORY CONTROL IN BILINGUAL APHASIA Monica Sampson, Doctor of Philosophy, 2015 Dissertation directed by: Yasmeen Faroqi-Shah, Ph.D. Department of Hearing and Speech Sciences Speaking involves selecting words and syntactic structures from among numerous competing options. It has been suggested that constant practice in using inhibitory control (IC) to limit within and cross-language competition may be associated with better lexicalsemantic...»

«Updated August 2013 Curriculum Vita John T. Bowen, Jr. Department of Geography Office Address & Phone Central Washington University 400 E. University Way, Ellensburg, WA 98926 tel: (509)-963-1130; fax: (509)-963-1047 e-mail: bowenjo@cwu.edu website: www.cwu.edu/~bowenjo Doctor of Philosophy (Geography), University of Kentucky, 1993 Master of Arts (Geography), University of Kentucky, 1991 Degrees Bachelor of Arts (Geography), Dartmouth College, 1988 Employment 1 Position Associate Professor &...»

«ON AN EXCHANGE OF CORRESPONDENCE BETWEEN RAYA DUNAYEVSKAYA AND NON-MARXIST HEGELIAN SCHOLARS January 7, 1987 Dear Colleagues, Because differences in Hegel's Science of Logic and the Encyclopedia versiot.e impinge on my changed perception of Lenin's philosophic ambivalence, I feel that I should give you a sense of the scholars' critique on the Idea of Cogaition.* First, the critics deny that there is a conflict between the Smaller Logic (Paragraph 235) and the Science of Logic, since the...»

«Theatre of Shame: The Impact of Paul’s Manual Labour on His Apostleship in Corinth by Catherine M. Jones A Thesis submitted to the Faculty of St. Michael’s College and the Biblical Department of the Toronto School of Theology. In partial fulfilment of the requirements for the degree of Doctor of Philosophy in Theology awarded by the University of St. Michael's College © Copyright by Catherine M. Jones (2013) Theatre of Shame: The Impact of Paul’s Manual Labour on His Apostleship in...»

«Essays in Heterogeneous Agent Macroeconomics A Dissertation Submitted to the Faculty of the Graduate School of the University of Minnesota by Andrew S. Glover In Partial Fulfilment of the Requirements for the Degree of Doctor of Philosophy Jos´-V´ e ıctor R´ ıos-Rull, Adviser August 2011 c Andrew S. Glover, 2011 Acknowledgements I would like to thank my adviser, Jos´-V´ e ıctor R´ ıos-Rull, for his guidance and encouragement. This dissertation would not exist without his assistance....»

«Diplomarbeit Weite und Wirklichkeit des Denkens – eine Debatte zwischen Anselm und Kant Verfasser Mag. Markus Bitterl Angestrebter akademischer Grad Magister der Philosophie (Mag.phil.) Wien, im April 2012 Studienkennzahl laut Studienbuchblatt: A 296 Studienrichtung laut Studienbuchblatt: Philosophie Betreuer: Univ.-Prof. Dr. Günther Pöltner Inhalt I. Einleitung 5 II. Vorfragen 7 Vorbemerkungen zum Umgang mit dem Text 7 Zur Frage der Einheit und Glaubensunabhängigkeit des Arguments 9...»





 
<<  HOME   |    CONTACTS
2016 www.abstract.xlibx.info - Free e-library - Abstract, dissertation, book

Materials of this site are available for review, all rights belong to their respective owners.
If you do not agree with the fact that your material is placed on this site, please, email us, we will within 1-2 business days delete him.