Key Exchange Protocols: Security Definition, Proof Method and Applications.
Anupam Datta, Ante Đerek, John C. Mitchell, Bogdan Warinschi · 2006
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 induction-like arguments about properties preserved by each run, we formulate a specification of secure key exchange that, unlike conventional key indistinguishability, is closed under general composition with steps that use the key.