Paper 2009/392

Computational Soundness for Key Exchange Protocols with Symmetric Encryption

Ralf Kuesters and Max Tuengerthal

Abstract

Formal analysis of security protocols based on symbolic models has been very successful in finding flaws in published protocols and proving protocols secure, using automated tools. An important question is whether this kind of formal analysis implies security guarantees in the strong sense of modern cryptography. Initiated by the seminal work of Abadi and Rogaway, this question has been investigated and numerous positive results showing this so-called computational soundness of formal analysis have been obtained. However, for the case of active adversaries and protocols that use symmetric encryption computational soundness has remained a challenge. 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.

Metadata
Available format(s)
PDF
Category
Cryptographic protocols
Publication info
Published elsewhere. Abridged version appears in CCS 2009.
Keywords
protocol analysiscomputational soundnesssimulation-based security
Contact author(s)
tuengerthal @ uni-trier de
History
2009-08-15: received
Short URL
https://ia.cr/2009/392
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2009/392,
      author = {Ralf Kuesters and Max Tuengerthal},
      title = {Computational Soundness for Key Exchange Protocols with Symmetric Encryption},
      howpublished = {Cryptology ePrint Archive, Paper 2009/392},
      year = {2009},
      note = {\url{https://eprint.iacr.org/2009/392}},
      url = {https://eprint.iacr.org/2009/392}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.