Paper 2006/218

Computationally Sound Symbolic Secrecy in the Presence of Hash Functions

Veronique Cortier, Steve Kremer, Ralf Kuesters, and Bogdan Warinschi

Abstract

The standard symbolic, deducibility-based notions of secrecy are in general insufficient from a cryptographic point of view, especially in presence of hash functions. In this paper we devise and motivate a more appropriate secrecy criterion which exactly captures a standard cryptographic notion of secrecy for protocols involving public-key enryption and hash functions: protocols that satisfy it are computationally secure while any violation of our criterion directly leads to an attack. Furthermore, we prove that our criterion is decidable via an NP decision procedure. Our results hold for standard security notions for encryption and hash functions modeled as random oracles.

Metadata
Available format(s)
PDF PS
Category
Foundations
Publication info
Published elsewhere. submitted to fsttcs
Keywords
automatic verificationcomputational soundness
Contact author(s)
bogdan @ cs stanford edu
History
2007-06-29: revised
2006-06-30: received
See all versions
Short URL
https://ia.cr/2006/218
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2006/218,
      author = {Veronique Cortier and Steve Kremer and Ralf Kuesters and Bogdan Warinschi},
      title = {Computationally Sound Symbolic Secrecy in the Presence of Hash Functions},
      howpublished = {Cryptology ePrint Archive, Paper 2006/218},
      year = {2006},
      note = {\url{https://eprint.iacr.org/2006/218}},
      url = {https://eprint.iacr.org/2006/218}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.