[Resource Topic] 2004/300: Relating Symbolic and Cryptographic Secrecy

Welcome to the resource topic for 2004/300

Relating Symbolic and Cryptographic Secrecy

Authors: Michael Backes, Birgit Pfitzmann


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.

ePrint: https://eprint.iacr.org/2004/300

See all topics related to this paper.

Feel free to post resources that are related to this paper below.

Example resources include: implementations, explanation materials, talks, slides, links to previous discussions on other websites.

For more information, see the rules for Resource Topics .