|Full text||Click to download.|
|Citation||PhD Thesis, Stanford University, 2005
This dissertation addresses two central problems associated with the design and
analysis of network protocols that use cryptographic primitives. The first
pertains to the secure composition of protocols, where the goal is to develop
proving properties of complex protocols by combining independent proofs of their
order to address this problem, we have developed a framework consisting of two
systems: Protocol Derivation System (PDS) and Protocol Composition Logic (PCL).
supports syntactic derivations of complex protocols, starting from basic
combining or extending them using a sequence of composition, refinement, and
transformation operations. PCL is a Floyd-Hoare style logic that supports
proofs of protocol properties. The eventual goal is to develop proof methods for
every derivation operation in PDS, thereby enabling the parallel development of
and their security proofs. In this dissertation, we present proof methods for
about protocol composition and a class of protocol refinements. The composition
are formulated and proved by adapting ideas from the assume-guarantee paradigm
reasoning about distributed systems. PDS and PCL have been successfully applied
number of industrial network security protocols, in several instances
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. 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 simulation-based 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.
Back to publications
Back to previous page