In this paper, we show the first general computational soundness result for key exchange protocols with symmetric encryption, along the lines of a paper by Canetti and Herzog on protocols with public-key encryption. More specifically, we develop a symbolic, automatically checkable criterion, based on observational equivalence, and show that a key exchange protocol that satisfies this criterion realizes a key exchange functionality in the sense of universal composability. Our results hold under standard cryptographic assumptions.
Category / Keywords: cryptographic protocols / protocol analysis, computational soundness, simulation-based security Publication Info: Abridged version appears in CCS 2009. Date: received 11 Aug 2009 Contact author: tuengerthal at uni-trier de Available format(s): PDF | BibTeX Citation Version: 20090815:023716 (All versions of this report) Discussion forum: Show discussion | Start new discussion