Sciweavers

Share
CSFW
2006
IEEE

Computationally Sound Compositional Logic for Key Exchange Protocols

9 years 10 months ago
Computationally Sound Compositional Logic for Key Exchange Protocols
We develop a compositional method for proving cryptographically sound security properties of key exchange protocols, based on a symbolic logic that is interpreted over conventional runs of a protocol against a probabilistic polynomial-time attacker. Since reasoning about an unbounded number of runs of a protocol involves inductionlike arguments about properties preserved by each run, we formulate a speciļ¬cation of secure key exchange that is closed under general composition with steps that use the key. We present formal proof rules based on this gamebased condition, and prove that the proof rules are sound over a computational semantics. The proof system is used to establish security of a standard protocol in the computational model.
Anupam Datta, Ante Derek, John C. Mitchell, Bogdan
Added 10 Jun 2010
Updated 10 Jun 2010
Type Conference
Year 2006
Where CSFW
Authors Anupam Datta, Ante Derek, John C. Mitchell, Bogdan Warinschi
Comments (0)
books