Security Analysis of Network Protocols: Compositional Reasoning and Complexity-theoretic Foundations

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. 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