Abstract
We compare two views of symmetric cryptographic primitives in the context of the systems that use them. We express those systems in a simple programming language; each of the views yields a semantics for the language. One of the semantics treats cryptographic operations formally (that is, symbolically). The other semantics is more detailed and computational; it treats cryptographic operations as functions on bitstrings. Each semantics leads to a definition of equivalence of systems with respect to eavesdroppers. We establish the soundness of the formal definition with respect to the computational one. This result provides a precise computational justification for formal reasoning about security against eavesdroppers.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Martín Abadi and Andrew D. Gordon. A calculus for cryptographic protocols: The spi calculus. Information and Computation, 148(1):1–70, January 1999. An extended version appeared as Digital Equipment Corporation Systems Research Center report No. 149, January 1998.
Martín Abadi and Jan Jürjens. Formal eavesdropping and its computational interpretation, 2001. Longer version of this paper, available at http://www.jurjens.de/jan/lambdaweb.ps.
Martín Abadi and Phillip Rogaway. Reconciling two views of cryptography (The computational soundness of formal encryption). In Proceedings of the First IFIP International Conference on Theoretical Computer Science, volume 1872 of Lecture Notes in Computer Science, pages 3–22. Springer-Verlag, August 2000.
Mihir Bellare, Anand Desai, Eron Jokipii, and Phillip Rogaway. A concrete security treatment of symmetric encryption: analysis of the DES modes of operation. In Proceedings of 38th Annual Symposium on Foundations of Computer Science (FOCS 97), pages 394–403, 1997.
Mihir Bellare and Phillip Rogaway. Entity authentication and key distribution. In Advances in Cryptology-CRYPTO’ 94, volume 773 of Lecture Notes in Computer Science, pages 232–249. Springer-Verlag, 1993.
Steven M. Bellovin. Problem areas for the IP security protocols. In Proceedings of the Sixth Usenix Unix Security Symposium, pages 1–16, July 1996.
Manuel Blum and Silvio Micali. How to generate cryptographically strong sequences of pseudo random bits. In Proceedings of the 23rd Annual Symposium on Foundations of Computer Science (FOCS 82), pages 112–117, 1982.
Danny Dolev and Andrew C. Yao. On the security of public key protocols. IEEE Transactions on Information Theory, IT-29(12):198–208, March 1983.
Marc Fischlin. Pseudorandom function tribe ensembles based on one-way permutations: Improvements and applications. In Advances in Cryptology-Eurocrypt’ 99, volume 1592 of Lecture Notes in Computer Science, pages 429–444. Springer-Verlag, 1999.
Oded Goldreich, Silvio Micali, and Avi Wigderson. How to play any mental game. In Proceedings of the Nineteenth Annual ACM Symposium on Theory of Computing, pages 218–229, 1987.
S. Goldwasser and M. Bellare. Lecture notes on cryptography, 1999.
Shafi Goldwasser and Silvio Micali. Probabilistic encryption. Journal of Computer and System Sciences, 28:270–299, April 1984.
Shafi Goldwasser, Silvio Micali, and Ronald Rivest. A digital signature scheme secure against adaptive chosen-message attack. SIAM Journal on Computing, 17:281–308, 1988.
Jan Jürjens. Composability of secrecy. In International Workshop on Mathematical Methods, Models and Architectures for Computer Networks Security (MMM 2001), volume 2052 of Lecture Notes in Computer Science, pages 28–38. Springer-Verlag, 2001.
Jan Jürjens. Secrecy-preserving refinement. In J. Fiadeiro and P. Zave, editors, Formal Methods Europe, volume 2021 of Lecture Notes in Computer Science, pages 135–152. Springer-Verlag, 2001.
R. Kemmerer, C. Meadows, and J. Millen. Three system for cryptographic protocol analysis. Journal of Cryptology, 7(2):79–130, Spring 1994.
P. Lincoln, J. Mitchell, M. Mitchell, and A. Scedrov. A probabilistic poly-time framework for protocol analysis. In Proceedings of the Fifth ACM Conference on Computer and Communications Security, pages 112–121, 1998.
Gavin Lowe. Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In Tools and Algorithms for the Construction and Analysis of Systems, volume 1055 of Lecture Notes in Computer Science, pages 147–166. Springer-Verlag, 1996.
A. Menezes, P. van Oorschot, and S. Vanstone. Handbook of Applied Cryptography. CRC Press, 1996.
Robin Milner. Communicating and Mobile Systems: the π-Calculus. Cambridge University Press, 1999.
John C. Mitchell. Foundations for Programming Languages. MIT Press, 1996.
Lawrence C. Paulson. The inductive approach to verifying cryptographic protocols. Journal of Computer Security, 6(1-2):85–128, 1998.
Birgit Pfitzmann, Matthias Schunter, and Michael Waidner. Cryptographic security of reactive systems (extended abstract). Electronic Notes in Theoretical Computer Science, 32, April 2000.
Birgit Pfitzmann and Michael Waidner. Composition and integrity preservation of secure reactive systems. In Proceedings of the 7th ACM Conference on Computer and Communications Security, pages 245–254, November 2000.
Birgit Pfitzmann and Michael Waidner. A model for asynchronous reactive systems and its application to secure message transmission. In Proceedings of the 2001 IEEE Symposium on Security and Privacy, pages 184–200, May 2001.
Andrew C. Yao. Theory and applications of trapdoor functions. In Proceedings of the 23rd Annual Symposium on Foundations of Computer Science (FOCS 82), pages 80–91, 1982.
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Abadi, M., Jürjens, J. (2001). Formal Eavesdropping and Its Computational Interpretation. In: Kobayashi, N., Pierce, B.C. (eds) Theoretical Aspects of Computer Software. TACS 2001. Lecture Notes in Computer Science, vol 2215. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45500-0_4
Download citation
DOI: https://doi.org/10.1007/3-540-45500-0_4
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42736-0
Online ISBN: 978-3-540-45500-4
eBook Packages: Springer Book Archive