Computationally Sound Compositional Logic for Key Exchange Protocols

\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.