Cryptology ePrint Archive: Report 2006/218

Computationally Sound Symbolic Secrecy in the Presence of Hash Functions

Veronique Cortier, Steve Kremer, Ralf Kuesters, 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.

Category / Keywords: foundations / automatic verification, computational soundness

Publication Info: submitted to fsttcs

Date: received 29 Jun 2006, last revised 29 Jun 2007

Contact author: bogdan at cs stanford edu

Available format(s): Postscript (PS) | Compressed Postscript (PS.GZ) | PDF | BibTeX Citation

Version: 20070629:074456 (All versions of this report)

Short URL: ia.cr/2006/218

Discussion forum: Show discussion | Start new discussion