Formal Analysis of Security Protocols: Protocol Composition Logic

Full textClick to download.
CitationPhD Thesis, Stanford University, 2006
AuthorAnte Derek


We develop Protocol Composition Logic (PCL) - a Floyd-Hoare style logic for axiomatic proofs of protocol properties that is sound with respect to the standard symbolic model of protocol execution and attack. PCL can express temporal ordering of actions and knowledge, naturally capturing security properties such as authentication and secrecy. The induction rule for proving invariants and the composition theorems allow us to prove properties of compound protocols by combining independent proofs of their components.

In order to bridge the gap between the symbolic and computational models of security, we develop Computational PCL (CLCP) - a cryptographically sound formal logic for proving protocol security properties without explicitly reasoning about probability, asymptotic complexity, or the actions of a malicious attacker. The approach rests on a new probabilistic, polynomial-time semantics for a subset of PCL. Using CPCL we formulate a specification of secure key exchange that is closed under general composition with steps that use the key and present sound formal proof rules based on this game-based condition.

Back to publications
Back to previous page