International Association for Cryptologic Research

International Association
for Cryptologic Research

CryptoDB

Computationally Sound Symbolic Secrecy in the Presence of Hash Functions

Authors:
Veronique Cortier
Steve Kremer
Ralf Küsters
Bogdan Warinschi
Download:
URL: http://eprint.iacr.org/2006/218
Search ePrint
Search Google
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.
BibTeX
@misc{eprint-2006-21711,
  title={Computationally Sound Symbolic Secrecy in the Presence of Hash Functions},
  booktitle={IACR Eprint archive},
  keywords={foundations / automatic verification, computational soundness},
  url={http://eprint.iacr.org/2006/218},
  note={submitted to fsttcs bogdan@cs.stanford.edu 13693 received 29 Jun 2006, last revised 29 Jun 2007},
  author={Veronique Cortier and Steve Kremer and Ralf Küsters and Bogdan Warinschi},
  year=2006
}