| Full text | Click to download. |
| Citation | PhD Thesis, Stanford University, 2006
|
| Author | Ante 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.