Abstract
This material was presented in a series of lectures at fosad, a summer school on Foundations of Security Analysis and Design, at the University of Bologna Center at Bertinoro in September 2000. It has two main purposes.
The first purpose is to explain how to model and analyze two important security problems, and how to derive systematic solutions to them. One problem area is the “packet protection problem,” concerning how to use the security services provided by routers—services such as packet filtering and the IP security protocols—to achieve useful protection in complex networks. The other problem area, the “Dolev-Yao” problem, concerns how to determine, given a cryptographic protocol, what authentication and confidentiality properties it achieves, assuming that the cryptographic primitives it uses are ideal.
Our secondary purpose is to argue in favor of an overall approach to modeling and then solving information security problems. We argue in favor of discovering security goals for specific domains by examining the threats and enforcement mechanisms available in those domains. Mathematical modeling allows us to develop algorithms and proof methods to ensure that the mechanisms achieve particular security goals. This leads to a systematic approach to trust management, often a more pressing information security problem than inventing new and improved security mechanisms.
Work reported here was supported by the National Security Agency through US Army CECOM contract DAAB07-99-C-C201. Work was in collaboration with Amy L. Herzog, Jonathan C. Herzog, and F. Javier Thayer.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Martín Abadi and Roger Needham. Prudent engineering practice for cryptographic protocols. In Proceedings, 1994 IEEE Symposium on Research in Security and Privacy, pages 122–136. ieee, ieee Computer Society Press, 1994. 252
Karl S. Brace, Richard L. Rudell, and Randal E. Bryant. Efficient implementation of a BDD package. In 27th ACM/IEEE Design Automation Conference, pages 40–45, 1990. 213
Randal E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677–691, August 1986. 210, 212
Michael Burrows, Martín Abadi, and Roger Needham. A logic of authentication. Proceedings of the Royal Society, Series A, 426(1871):233–271, December 1989. Also appeared as SRC Research Report 39 and, in a shortened form, in ACM Transactions on Computer Systems 8, 1 (February 1990), 18-36. 219
Ulf Carlsen. Optimal privacy and authentication on a portable communications system. Operating Systems Review, 28(3):16–23, 1994. 226
John Clark and Jeremy Jacob. A survey of authentication protocol literature: Version 1.0. University of York, Department of Computer Science, November 1997.219, 251
Edmund Clarke, Somesh Jha, and Will Marrero. Using state space exploration and a natural deduction style message derivation engine to verify security protocols. In Proceedings, IFIP Working Conference on Programming Concepts and Methods (Procomet), 1998. 240
T. Dierks and C. Allen. The TLS protocol. RFC 2246, January 1999. 219, 251
D. Dolev and A. Yao. On the security of public-key protocols. IEEE Transactions on Information Theory, 29:198–208, 1983. 198, 219, 251
Li Gong and Paul Syverson. Fail-stop protocols: An approach to designing secure protocols. In 5th International Working Conference on Dependable Computing for Critical Applications, pages 44–55, September 1995. 251
Joshua D. Guttman. Filtering postures: Local enforcement for global policies. In Proceedings, 1997 IEEE Symposium on Security and Privacy, pages 120–29. IEEE Computer Society Press, May 1997. 199, 200, 208, 209, 210
Joshua D. Guttman. Packet filters and their atoms. Lecture at University of Pennsylvania, host C. Gunter, April 1999. 210
Joshua D. Guttman, Amy L. Herzog, and F. Javier Thayer. Authentication and confidentiality via IPsec. In D. Gollman, editor, ESORICS 2000: European Symposium on Research in Computer Security, LNCS. Springer Verlag, 2000. 199, 200,203
Joshua D. Guttman and F. Javier Thayer Fábrega. Authentication tests. In Proceedings, 2000 IEEE Symposium on Security and Privacy. May, IEEE Computer Society Press, 2000. 199, 251
Joshua D. Guttman and F. Javier Thayer Fábrega. Protocol independence through disjoint encryption. In Proceedings, 13th Computer Security Foundations Workshop. IEEE Computer Society Press, July 2000. 199
Joshua D. Guttman and F. Javier Thayer Fábrega. Authentication tests and the structure of bundles. Theoretical Computer Science, 2001. To appear. 199, 224, 229, 234, 246
Joshua D. Guttman, F. Javier Thayer Fábrega, and Lenore D. Zuck. Faithful to the cryptography. Submitted for publication. Available at http://cs.nyu.edu/zuck. 229
D. Harkins and D. Carrel. The Internet Key Exchange (IKE). IETF Network Working Group RFC 2409, November 1998. 251
James Heather, Gavin Lowe, and Steve Schneider. How to prevent type flaw attacks on security protocols. In Proceedings, 13th Computer Security Foundations Workshop. IEEE Computer Society Press, July 2000. 252
James Heather and Steve Schneider. Toward automatic verification of authentication protocols on an unbounded network. In Proceedings, 13th Computer Security Foundations Workshop. IEEE Computer Society Press, July 2000. 240
Mei Lin Hui and Gavin Lowe. Safe simplifying transformations for security protocols. In 12th Computer Security Foundations Workshop Proceedings, pages 32–43. IEEE Computer Society Press, June 1999. 252
Jan Jürjens and Guido Wimmel. Specification-based testing of firewalls. Submitted for publication, 2001. 218
John Kelsey, Bruce Schneier, and David Wagner. Protocol interactions and the chosen protocol attack. In Security Protocols, International Workshop April 1997 Proceedings, pages 91–104. Springer-Verlag, 1998. 251
J. Kohl and C. Neuman. The Kerberos network authentication service (v5). RFC 1510, September 1993. 255
Xavier Leroy, Damien Doligez, Jacques Garrigue, Didier Rémy, and Jérôme Vouillon. The Objective Caml System. INRIA, http://caml.inria.fr/, 2000. Version 3.00. 217
Gavin Lowe. An attack on the Needham-Schroeder public key authentication protocol. Information Processing Letters, 56(3):131–136, November 1995. 247
Gavin Lowe. Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In Proceeedings of tacas, volume 1055 of Lecture Notes in Computer Science, pages 147–166. Springer Verlag, 1996. 221, 231, 247
Gavin Lowe. Some new attacks upon security protocols. In Proceedings of the Computer Security Foundations Workshop IX. IEEE Computer Society Press, 1996. 219
Gavin Lowe. Casper: A compiler for the analysis of security protocols. In 10th Computer Security Foundations Workshop Proceedings, pages 18–30. IEEE Computer Society Press, 1997. 236
Gavin Lowe. A hierarchy of authentication specifications. In 10th Computer Security Foundations Workshop Proceedings, pages 31–43. IEEE Computer Society Press, 1997. 238
Gavin Lowe. Toward a completeness result for model checking of security protocols. In 11th Computer Security Foundations Workshop Proceedings, pages 96–105. IEEE Computer Society Press, 1998. 252
Will Marrero, Edmund Clarke, and Somesh Jha. A model checker for authentication protocols. In Cathy Meadows and Hilary Orman, editors, Proceedings of the DIMACS Workshop on Design and Verification of Security Protocols. DIMACS, Rutgers University, September 1997. 236
D. Mau ghan, M. Schertler, M. Schneider, and J. Tu rner. Internet Security Association and Key Management Protocol (ISAKMP). IETF Network Working Group RFC 2408, November 1998. 251
Alain Mayer, Avishai Wool, and Elisha Ziskind. Fang: A firewall analysis engine. In Proceedings, IEEE Symposium on Security and Privacy, 2000. 210
Catherine Meadows. Analysis of the Internet Key Exchange protocol using the NRL protocol analyzer. In Proceedings, 1999IEEE Symposium on Security and Privacy. IEEE Computer Society Press, May 1999. 251
Catherine Meadows. Open issues in formal methods for cryptographic protocol analysis. In DISCEX Workshop. DARPA, January 2000. 251
Roger Needham and Michael Schroeder. Using encryption for authentication in large networks of computers. Communications of the ACM,21(12), December 1978. 220
B. Clifford Neuman and Stuart G. Stubblebine. A note on the use of timestamps as nonces. Operating Systems Review, 27(2):10–14, April 1993. 248, 255
Lawrence C. Paulson. Proving properties of security protocols by induction. In 10th IEEE Computer Security Foundations Workshop, pages 70–83. IEEE Computer Society Press, 1997. 236
Lawrence C. Paulson. The inductive approach to verifying cryptographic protocols. Journal of Computer Security, 1998. Also Report 443, Cambridge University Computer Lab. 237, 240
Adrian Perrig and Dawn Xiaodong Song. Looking for diamonds in the desert: Extending automatic protocol generation to three-party authentication and key agreement protocols. In Proceedings of the 13th IEEE Computer Security Foundations Workshop. IEEE Computer Society Press, July 2000. 246
Dag Prawitz. Natural Deduction: A Proof-Theoretic Study. Almqvist and Wiksel, Stockholm, 1965. 240
Steve Schneider. Verifying authentication protocols with CSP. In Proceedings of the 10th IEEE Computer Security Foundations Workshop, pages 3–17. IEEE Computer Society Press, 1997. 237
Scott Stoller. A bound on attacks on authentication protocols. Available at http://www.cs.indiana.edu/~stoller/, July 1999. 252
Scott Stoller. A reduction for automated verification of authentication protocols. In Workshop on Formal Methods and Security Protocols, July 1999. Available at http://www.cs.indiana.edu/~stoller/. 252
F. Javier Thayer Fábrega, Jonathan C. Herzog, and Joshua D. Guttman. Mixed strand spaces. In Proceedings of the 12th IEEE Computer Security Foundations Workshop. IEEE Computer Society Press, June 1999. 251, 252, 257
F. Javier Thayer Fábrega, Jonathan C. Herzog, and Joshua D. Guttman. Strand spaces: Proving security protocols correct. Journal of Computer Security,7(2/3):191–230, 1999. 199, 224, 225, 229, 232, 234, 238
D. Wagner and B. Schneier. Analysis of the SSL 3.0 protocol. In Proceedings, Second USENIX Workshop on Electronic Commerce, pages 29–40, 1996. Available at http://www.counterpane.com/ssl.html. 251
Thomas Y. C. Woo and Simon S. Lam. Verifying authentication protocols: Methodology and example. In Proc. Int. Conference on Network Protocols, October 1993. 238
T. Ylonen, T. Kivinen, and M. Saarinen. SSH prototcol architecture. Internet draft, November 1997. Also named draft-ietf-secsh-architecture-01.txt. 219
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Guttman, J.D. (2001). Security Goals: Packet Trajectories and Strand Spaces. In: Focardi, R., Gorrieri, R. (eds) Foundations of Security Analysis and Design. FOSAD 2000. Lecture Notes in Computer Science, vol 2171. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45608-2_4
Download citation
DOI: https://doi.org/10.1007/3-540-45608-2_4
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42896-1
Online ISBN: 978-3-540-45608-7
eBook Packages: Springer Book Archive