**Relating Symbolic and Cryptographic Secrecy**

*Michael Backes and Birgit Pfitzmann*

**Abstract: **We investigate the relation between symbolic and cryptographic secrecy
properties for cryptographic protocols. Symbolic secrecy of payload
messages or exchanged keys is arguably the most important notion of
secrecy shown with automated proof tools. It means that an adversary
restricted to symbolic operations on terms can never get the entire
considered object into its knowledge set. Cryptographic secrecy
essentially means computational indistinguishability between the real
object and a random one, given the view of a much more general
adversary. In spite of recent advances in linking symbolic and
computational models of cryptography, no relation for secrecy under
active attacks is known yet.

For exchanged keys, we show that a certain strict symbolic secrecy definition over a specific Dolev-Yao-style cryptographic library implies cryptographic key secrecy for a real implementation of this cryptographic library. For payload messages, we present the first general cryptographic secrecy definition for a reactive scenario. The main challenge is to separate secrecy violations by the protocol under consideration from secrecy violations by the protocol users in a general way. For this definition we show a general secrecy preservation theorem under reactive simulatability, the cryptographic notion of secure implementation. This theorem is of independent cryptographic interest. We then show that symbolic secrecy implies cryptographic payload secrecy for the same cryptographic library as used in key secrecy. Our results thus enable existing formal proof techniques to establish cryptographically sound proofs of secrecy for payload messages and exchanged keys.

**Category / Keywords: **foundations / secrecy, symbolic, cryptographic, formal methods, reactive simulatability, security analysis of cryptographic protocols

**Date: **received 12 Nov 2004

**Contact author: **mbc at zurich ibm com

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

**Version: **20041112:153223 (All versions of this report)

**Short URL: **ia.cr/2004/300

**Discussion forum: **Show discussion | Start new discussion

[ Cryptology ePrint archive ]