This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Relating Symbolic and Cryptographic Secrecy
April-June 2005 (vol. 2 no. 2)
pp. 109-123
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 formal proof techniques to establish cryptographically sound proofs of secrecy for payload messages and exchanged keys.

[1] D. Dolev and A.C. Yao, “On the Security of Public Key Protocols,” IEEE Trans. Information Theory, vol. 29, no. 2, pp. 198-208, 1983.
[2] S. Even and O. Goldreich, “On the Security of Multi-Party Ping-Pong Protocols,” Proc. 24th IEEE Symp. Foundations of Computer Science (FOCS), pp. 34-39, 1983.
[3] M. Merritt, “Cryptographic Protocols,” PhD dissertation, Georgia Inst. of Tech nology, 1983.
[4] J.K. Millen, “The Interrogator: A Tool for Cryptographic Protocol Security,” Proc. Fifth IEEE Symp. Security and Privacy, pp. 134-141, 1984.
[5] C. Meadows, “Using Narrowing In the Analysis of Key Management Protocols,” Proc. 10th IEEE Symp. Security and Privacy, pp. 138-147, 1989.
[6] R. Kemmerer, C. Meadows, and J. Millen, “Three Systems for Cryptographic Protocol Analysis,” J. Cryptology, vol. 7, no. 2, pp. 79-130, 1994.
[7] S. Schneider, “Security Properties and CSP,” Proc. 17th IEEE Symp. Security and Privacy, pp. 174-187, 1996.
[8] M. Abadi and A.D. Gordon, “A Calculus for Cryptographic Protocols: The Spi Calculus,” Proc. Fourth ACM Conf. Computer and Comm. Security, pp. 36-47, 1997.
[9] G. Lowe, “Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR,” Proc. Second Conf. Tools and Algorithms for Construction and Analysis of Systems, 1996.
[10] L. Paulson, “The Inductive Approach to Verifying Cryptographic Protocols,” J. Cryptology, vol. 6, no. 1, pp. 85-128, 1998.
[11] M. Abadi and P. Rogaway, “Reconciling Two Views of Cryptography: The Computational Soundness of Formal Encryption,” Proc. First IFIP Int'l Conf. Theoretical Computer Science, 2000.
[12] M. Abadi and J. Jürjens, “Formal Eavesdropping and Its Computational Interpretation,” Proc. Fourth Int'l Symp. Theoretical Aspects of Computer Software (TACS), pp. 82-94, 2001.
[13] P. Laud, “Semantics and Program Analysis of Computationally Secure Information Flow,” Proc. 10th European Symp. Programming (ESOP), pp. 77-91, 2001.
[14] J. Herzog, M. Liskov, and S. Micali, “Plaintext Awareness Via Key Registration,” Proc. Conf. Advances in Cryptology (CRYPTO 2003), 2003.
[15] M. Backes, B. Pfitzmann, and M. Waidner, “A Composable Cryptographic Library with Nested Operations (Extended Abstract),” Proc. 10th ACM Conf. Computer and Comm. Security, pp. 220-230, Jan. 2003.
[16] M. Backes, B. Pfitzmann, and M. Waidner, “Symmetric Authentication Within A Simulatable Cryptographic Library,” Proc. Eighth European Symp. Research in Computer Security (ESORICS), July 2003.
[17] M. Backes and B. Pfitzmann, “Symmetric Encryption in a Simulatable Dolev-Yao Style Cryptographic Library,” Proc. 17th IEEE Computer Security Foundations Workshop (CSFW), Feb. 2004.
[18] M. Backes and C. Jacobi, “Cryptographically Sound and Machine-Assisted Verification of Security Protocols,” Proc. 20th Ann. Symp. Theoretical Aspects of Computer Science (STACS), 2003.
[19] M. Backes and B. Pfitzmann, “Computational Probabilistic Noninterference,” Proc. Seventh European Symp. Research in Computer Security (ESORICS), 2002.
[20] A. Sabelfeld and D. SandsChalmers, “Intransitive Noninterference For Cryptographic Purposes,” Proc. 24th IEEE Symp. Security and Privacy, pp. 140-152, 2003.
[21] M. Backes, B. Pfitzmann, M. Steiner, and M. Waidner, “Polynomial Fairness and Liveness,” Proc. 15th IEEE Computer Security Foundations Workshop (CSFW), pp. 160-174, 2002.
[22] M. Backes and B. Pfitzmann, “A Cryptographically Sound Security Proof of the Needham-Schroeder-Lowe Public-Key Protocol,” Proc. 23rd Conf. Foundations of Software Technology and Theoretical Computer Science, pp. 1-12, June 2003.
[23] M. Backes, “A Cryptographically Sound Dolev-Yao Style Security Proof of the Otway-Rees Protocol,” Proc. Ninth European Symp. Research in Computer Security (ESORICS), 2004.
[24] P. Laud, “Symmetric Encryption in Automatic Analyses for Confidentiality against Active Adversaries,” Proc. 25th IEEE Symp. Security and Privacy, pp. 71-85, 2004.
[25] D. Micciancio and B. Warinschi, “Soundness of Formal Encryption in the Presence of Active Adversaries,” Proc. First Theory of Cryptography Conf. (TCC), pp. 133-151, 2004.
[26] R. Canetti and J. Herzog, “Universally Composable Symbolic Analysis of Cryptographic Protocols (The Case of Encryption-Based Mutual Authentication and Key Exchange),” Cryptology ePrint Archive, Report 2004/334, 2004.
[27] B. Blanchet, “Automatic Proof of Strong Secrecy for Security Protocols,” Proc. 25th IEEE Symp. Security and Privacy, pp. 86-100, 2004.
[28] S. Goldwasser and S. Micali, “Probabilistic Encryption,” J. Computer and System Sciences, vol. 28, pp. 270-299, 1984.
[29] M. Backes and B. Pfitzmann, “Cryptographic Key Secrecy of the Strengthened Yahalom Protocol via a Symbolic Security Proof,” Research Report 3601, IBM Research, 2005.
[30] G. Lowe, “Casper: A Compiler for the Analysis of Security Protocols,” Proc. 10th IEEE Computer Security Foundations Workshop (CSFW), pp. 18-30, 1997.
[31] A.C. Yao, “Theory and Applications of Trapdoor Functions,” Proc. 23rd IEEE Symp. Foundations of Computer Science (FOCS), pp. 80-91, 1982.
[32] B. Pfitzmann and M. Waidner, “A Model for Asynchronous Reactive Systems and Its Application to Secure Message Transmission,” Proc. 22nd IEEE Symp. Security and Privacy, pp. 184-200, 2001.
[33] M. Backes, B. Pfitzmann, and M. Waidner, “A General Composition Theorem for Secure Reactive Systems,” Proc. First Theory of Cryptography Conf. (TCC), pp. 336-354, 2004.
[34] P. Lincoln, J. Mitchell, M. Mitchell, and A. Scedrov, “A Probabilistic Poly-Time Framework for Protocol Analysis,” Proc. Fifth ACM Conf. Computer and Comm. Security, pp. 112-121, 1998.

Index Terms:
Index Terms- Relations between models, probabilistic computation—cryptography, Dolev-Yao model, secrecy, simulatability.
Citation:
Michael Backes, Birgit Pfitzmann, "Relating Symbolic and Cryptographic Secrecy," IEEE Transactions on Dependable and Secure Computing, vol. 2, no. 2, pp. 109-123, April-June 2005, doi:10.1109/TDSC.2005.25
Usage of this product signifies your acceptance of the Terms of Use.