Secure protocol composition

ABSTRACT

Modular composition of security mechanisms is complicated by the way that one mechanism may reveal information that interferes with the security of another. We develop methods for modular reasoning about security protocols, using before-after assertions and protocol invariants. The before-after assertions allow us to prove properties of a sequential composition of protocol steps and therefore enable construction of complex protocols from smaller sub-protocols. Invariants provide a mechanism for ensuring that sub-protocols which are individually secure do not interact insecurely when they are composed to construct a bigger protocol. The application of the method is demonstrated by giving modular formal proofs involving two standard protocols.

REFERENCES

• 1: Martín Abadi , Andrew D. Gordon, A calculus for cryptographic protocols, Information and Computation, v.148 n.1, p.1-70, Jan. 10, 1999 [doi>10.1006/inco.1998.2740]
• 2: Mihir Bellare , Phillip Rogaway, Entity authentication and key distribution, Proceedings of the 13th annual international cryptology conference on Advances in cryptology, p.232-249, January 1994, Santa Barbara, California, United States
• 3: Gérard Berry , Gérard Boudol, The chemical abstract machine, Theoretical Computer Science, v.96 n.1, p.217-248, 6 April 1992
• 4: R. Canetti, C. Meadows, and P. Syverson. Environmental requirements for authentication protocols. In Proceedings of Software Security - Theories and Systems, Mext-NSF-JSPS International Symposium, ISSS, LNCS 2609, pages 339-355. Springer-Verlag, 2003.
• 5: A. Datta, A. Derek, J. C. Mitchell, and D. Pavlovic. A derivation system for security protocols and its logical formalization. In Proceedings of 16th IEEE Computer Security Foundations Workshop, pages 109-125. IEEE, 2003.
• 6: W. Diffie and M. E. Hellman. New directions in cryptography. IEEE Transactions on Information Theory, IT-22(6):644-654, 1976.
• 7: Whitfield Diffie , Paul C. Van Oorschot , Michael J. Wiener, Authentication and authenticated key exchanges, Designs, Codes and Cryptography, v.2 n.2, p.107-125, June 1992 [doi>10.1007/BF00124891]
• 8: D. Dolev and A. Yao. On the security of public-key protocols. IEEE Transactions on Information Theory, 2(29), 1983.
• 9: Nancy Durgin , John Mitchell , Dusko Pavlovic, A Compositional Logic for Protocol Correctness, Proceedings of the 14th IEEE Workshop on Computer Security Foundations, p.241, June 11-13, 2001
• 10: F. J. T. Fábrega, J. C. Herzog, and J. D. Guttman. Strand spaces: Why is a security protocol correct? In Proceedings of the 1998 IEEE Symposium on Security and Privacy, pages 160-171, Oakland, CA, May 1998. IEEE Computer Society Press.
• 11: L. Gong and P. Syverson. Fail-stop protocols: An approach to designing secure protocols. Dependable Computing for Critical Applications, 5:79-100, 1998.
• 12: Joshua D. Guttman , F. Javier Thayer, Protocol Independence through Disjoint Encryption, Proceedings of the 13th IEEE Computer Security Foundations Workshop (CSFW'00), p.24, July 03-05, 2000
• 13: D. Harkins and D. Carrel. The Internet Key Exchange (IKE), 1998. RFC 2409.
• 14: Nevin Heintze , J. D. Tygar, A Model for Secure Protocols and Their Compositions, IEEE Transactions on Software Engineering, v.22 n.1, p.16-30, January 1996 [doi>10.1109/32.481514]
• 15: IEEE. Entity authentication mechanisms - part 3: Entity authentication using asymmetric techniques. Technical report ISO/IEC IS 9798-3, ISO/IEC, 1993.
• 16: John Kelsey , Bruce Schneier , David Wagner, Protocol Interactions and the Chosen Protocol Attack, Proceedings of the 5th International Workshop on Security Protocols, p.91-104, April 07-09, 1997
• 17: Gavin Lowe, Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR, Proceedings of the Second International Workshop on Tools and Algorithms for Construction and Analysis of Systems, p.147-166, March 27-29, 1996
• 18: Nancy Lynch, I/O Automaton Models and Proofs for Shared-Key Communication Systems, Proceedings of the 1999 IEEE Computer Security Foundations Workshop, p.14, June 28-30, 1999
• 19: Zohar Manna , Amir Pnueli, Temporal verification of reactive systems: safety, Springer-Verlag New York, Inc., New York, NY, 1995
• 20: Heiko Mantel, On the Composition of Secure Systems, Proceedings of the 2002 IEEE Symposium on Security and Privacy, p.88, May 12-15, 2002
• 21: D. McCullough. Noninterference and the composability of security properties. In Proceedings of the IEEE Symposium on Security and Privacy, pages 177-186, Oakland, CA, USA, May 1988. IEEE Computer Society.
• 22: Daryl McCullough, A Hookup Theorem for Multilevel Security, IEEE Transactions on Software Engineering, v.16 n.6, p.563-568, June 1990 [doi>10.1109/32.55085]
• 23: J. McLean. Security models and information flow. In Proceedings of the IEEE Symposium on Security and Privacy, Oakland, CA, USA, May 1990. IEEE Computer Society.
• 24: John McLean, A General Theory of Composition for a Class of "Possibilistic" Properties, IEEE Transactions on Software Engineering, v.22 n.1, p.53-67, January 1996 [doi>10.1109/32.481534]
• 25: C. Meadows. A model of computation for the NRL protocol analyzer. In Proceedings of 7th IEEE Computer Security Foundations Workshop, pages 84-89. IEEE, 1994.
• 26: C. Meadows. The NRL protocol analyzer: An overview. Journal of Logic Programming, 26(2):113-131, 1996.
• 27: C. Meadows. Analysis of the Internet Key Exchange protocol using the NRL protocol analyzer. In Proceedings of the IEEE Symposium on Security and Privacy. IEEE, 1998.
• 28: Alfred J. Menezes , Scott A. Vanstone , Paul C. Van Oorschot, Handbook of Applied Cryptography, CRC Press, Inc., Boca Raton, FL, 1996
• 29: R. Milner. Action structures. LFCS report ECS-LFCS-92-249, Department of Computer Science, University of Edinburgh, JCMB, The Kings Buildings, Mayfield Road, Edinburgh, December 1992.
• 30: R. Milner. Action calculi and the pi-calculus. In NATO Summer School on Logic and Computation, Marktoberdorf, November 1993.
• 31: Robin Milner, Communicating and mobile systems: the &pgr;-calculus, Cambridge University Press, New York, NY, 1999
• 32: Roger M. Needham , Michael D. Schroeder, Using encryption for authentication in large networks of computers, Communications of the ACM, v.21 n.12, p.993-999, Dec. 1978 [doi>10.1145/359657.359659]
• 33: Duško Pavlović, Categorical logic of names and abstraction in action calculi, Mathematical Structures in Computer Science, v.7 n.6, p.619-637, December 1997 [doi>10.1017/S0960129597002296]
• 34: Doron A. Peled , David Gries , Fred B. Schneider, Software reliability methods, Springer-Verlag New York, Inc., Secaucus, NJ, 2001
• 35: Paul Syverson , Catherine Meadows, A Formal Language for Cryptographic Protocol Requirements, Designs, Codes and Cryptography, v.7 n.1-2, p.27-59, Jan. 1996 [doi>10.1007/BF00125075]
• 36: F. Javier Thayer , Jonathan C. Herzog , Joshua D. Guttman, Mixed Strand Spaces, Proceedings of the 1999 IEEE Computer Security Foundations Workshop, p.72, June 28-30, 1999
• 37: Thomas Y. C. Woo , Simon S. Lam, A Semantic Model for Authentication Protocols, Proceedings of the 1993 IEEE Symposium on Security and Privacy, p.178, May 24-26, 1993

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

General Terms:
Security, Theory, Verification

Keywords:
invariants, logic, protocol composition, security protocols