Secrecy Analysis in Protocol Composition Logic

We present formal proof rules for inductive reasoning about the way that data transmitted on the network remains secret from a malicious attacker. Extending a compositional protocol logic with an induction rule for secrecy, we prove soundness for a conventional symbolic protocol execution model, adapt and extend previous composition theorems, and illustrate the logic by proving properties of two key agreement protocols. The first example is a variant of the Needham-Schroeder protocol that illustrates the ability to reason about temporary secrets. The second example is Kerberos V5. The modular nature of the secrecy and authentication proofs for Kerberos make it possible to reuse proofs about the basic version of the protocol for the PKINIT version that uses public-key infrastructure instead of shared secret keys in the initial steps. Keywords. Security protocol analysis, Logic, Secrecy

• Type: Conference
• Year: 2006
• Where: ASIAN
• Authors: Arnab Roy, Anupam Datta, Ante Derek, John C. Mitchell, Jean-Pierre Seifert
• Keywords: Algorithms, ASIAN 2006, Compositional Protocol Logic, Formal Proof Rules, Symbolic Protocol Execution