Skip to main content

Computationally Sound Compositional Logic for Key Exchange Protocols

Anupam Datta, Ante Derek, John Mitchell, Bogdan Warinschi, Computationally Sound Compositional Logic for Key Exchange Protocols . Proceedings of 19th IEEE Computer Security Foundations Workshop, pp. 321–334. February 2006. No electronic version available.


\begin{abstract} 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 \emph{secure key exchange} that \cut{, unlike conventional key indistinguishability,} is closed under general composition with steps that use the key. We present formal proof rules based on this game-based 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.

Bibtex entry.

Contact details

Publication Admin