Sciweavers

Share
ASIAN
2006
Springer

Secrecy Analysis in Protocol Composition Logic

11 years 5 months ago
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
Arnab Roy, Anupam Datta, Ante Derek, John C. Mitch
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2006
Where ASIAN
Authors Arnab Roy, Anupam Datta, Ante Derek, John C. Mitchell, Jean-Pierre Seifert
Comments (0)
books