Full text  Click to download. 
Citation  PhD Thesis, Stanford University, 2005

Author  Anupam Datta

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 FloydHoare 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 assumeguarantee 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 highlevel, 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 complexitytheoretic model of modern
cryptography.
Our approach to this problem involves defining complexitytheoretic 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
simulationbased
definitions for protocol securityuniversal composability, blackbox
simulatability, and
process observational equivalenceexpress 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 polytime process calculus, whose
execution model
is consistent with the complexitytheoretic model of cryptography. We also
observe certain
important differences between the composition paradigm of universal
composability, and the
assumeguarantee paradigm of PCL.