loading...
Relating Symbolic and Cryptographic Secrecy
Oakland, California May 08-May 11
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SP.2005.172005 IEEE Symposium on Security and P ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Michael Backes, IBM Zurich Research Laboratory, R?schlikon, Switzerland
Birgit Pfitzmann, IBM Zurich Research Laboratory, R?schlikon, Switzerland
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.
Citation:
Michael Backes, Birgit Pfitzmann, "Relating Symbolic and Cryptographic Secrecy," sp, pp.171-182, 2005 IEEE Symposium on Security and Privacy (S&P'05), 2005
Usage of this product signifies your acceptance of the Terms of Use.