Protocol Composition Logic (PCL)

Summary

PCL is a logic for proving security properties of network protocols. Two central results for PCL are a set of composition theorems and a computational soundness theorem. In contrast to traditional folk wisdom in computer security, the composition theorems allow proofs of complex protocols to be built up from proofs of their constituent sub-protocols. The computational soundness theorem guarantees that, for a class of security properties and protocols, axiomatic proofs in PCL carry the same meaning as reduction-style cryptographic proofs. Tool implementation efforts are also underway. PCL and a complementary model-checking method have been successfully applied to a number of internet, wireless and mobile network security protocols developed by the IEEE and IETF Working Groups. This work identified serious security vulnerabilities in the IEEE 802.11i wireless security standard and the IETF GDOI standard. The suggested fixes have been adopted by the respective standards bodies.

PCL has been the topic of invited talks at premier venues including ASL'01, MFPS'03, ICALP'05, LCC'06, and ASIAN'06. It has been taught in security courses at a number of universities including Aachen, CMU, Penn, Stanford, and Texas. Three papers on this work have been invited to special issues of journals, which are compilations of the best papers presented at the respective venues.

The following paper and set of slides provides an overview of this project. For further details, please read the other papers included below.

• A. Datta, A. Derek, J. C. Mitchell, A. Roy, Protocol Composition Logic (PCL), Electronic Notes in Theoretical Computer Science, Volume 172 , 1 April 2007, Pages 311-358. Computation, Meaning, and Logic: Articles dedicated to Gordon Plotkin. [ Paper ]

• J. C. Mitchell, Symbolic and Computational Analysis of Network Protocol Security, Invited Talk, ASIAN Computing Science Conference, December 2006. [ Slides ]

Also see the model-checking page for related projects.

Publications

Methodology

• A. Roy, A. Datta, A. Derek, J. C. Mitchell, and J.-P. Seifert, "Secrecy Analysis in Protocol Composition Logic", in Formal Logical Methods for System Security and Correctness, IOS Press, 2008. Volume based on presentations at Summer School 2007, Formal Logical Methods for System Security and Correctness, Marktoberdorf, Germany. [ Paper ]
• A. Roy, A. Datta, J. C. Mitchell, "Formal Proofs of Cryptographic Security of Diffie-Hellman-based Protocols", to appear in Proceedings of 3rd Symposium on Trustworthy Global Computing, November 2007. [ Paper ]
• A. Roy, A. Datta, A. Derek, J. C. Mitchell, Inductive Proofs of Computational Secrecy, in Proceedings of 12th European Symposium On Research In Computer Security , September 2007. [ Full paper in preparation ]
• A. Datta, A. Derek, J. C. Mitchell, A. Roy, Protocol Composition Logic (PCL), Electronic Notes in Theoretical Computer Science, Volume 172 , 1 April 2007, Pages 311-358. Computation, Meaning, and Logic: Articles dedicated to Gordon Plotkin. [ Paper ]
• A. Roy, A. Datta, A. Derek, J. C. Mitchell, J.-P. Seifert, Secrecy Analysis in Protocol Composition Logic, to appear in Proceedings of 11th Annual Asian Computing Science Conference, December 2006. [ Paper ]
• A. Datta, A. Derek, J. C. Mitchell, B. Warinschi, Computationally Sound Compositional Logic for Key Exchange Protocols, in Proceedings of 19th IEEE Computer Security Foundations Workshop, pp. 321-334, July 2006. [ Paper ]
• A. Datta, Security Analysis of Network Protocols: Compositional Reasoning and Complexity-theoretic Foundations, PhD Thesis, Computer Science Department, Stanford University, September 2005. [ PS ] [ PDF ]
• A. Datta, A. Derek, J. C. Mitchell, V. Shmatikov, M. Turuani, Probabilistic Polynomial-time Semantics for a Protocol Security Logic, in Proceedings of 32nd International Colloquium on Automata, Languages and Programming, pp. 16-29, July 2005. [ Paper ]    Invited Paper
• A. Datta, A. Derek, J. C. Mitchell, D. Pavlovic, A Derivation System and Compositional Logic for Security Protocols, Journal of Computer Security (Special Issue of Selected Papers from CSFW-16), Vol. 13, pp. 423-482, 2005. [ Paper ]
• A. Datta, A. Derek, J. C. Mitchell, D. Pavlovic, Abstraction and Refinement in Protocol Derivation, in Proceedings of 17th IEEE Computer Security Foundations Workshop, pp. 30-45, June 2004. [ Paper ] [ slides ]
• A. Datta, A. Derek, J. C. Mitchell, D. Pavlovic, Secure Protocol Composition.
  • In Proceedings of 19th Annual Conference on Mathematical Foundations of Programming Semantics, Electronic Notes in Theoretical Computer Science, Vol. 83, 2004. [ Paper ]
  • Extended abstract in Proceedings of ACM  Workshop on Formal Methods in Security Engineering, pp. 11-23, October 2003. [ Paper ] [ slides ]
• A. Datta, A. Derek, J. C. Mitchell, D. Pavlovic, A Derivation System for Security Protocols and its Logical Formalization, in Proceedings of 16th IEEE Computer Security Foundations Workshop, pp. 109-125, June 2003. [ Paper ] [ slides ]    Award Paper
• A. Datta, J. C. Mitchell, D. Pavlovic, Derivation of the JFK Protocol, Kestrel Institute Technical Report, KES.U.02.03, July 2002.  [ TR ] [ slides ]
• N. Durgin, J. C. Mitchell, D. Pavlovic, A Compositional Logic for Proving Security Properties of Protocols.
  • In Journal of Computer Security (Special Issue of Selected Papers from CSFW-14), 11(4):677-721, 2003. [ Paper ]
  • In Proceedings of 14th IEEE Computer Security Foundations Workshop, pp. 241-255, June 2001. [ Paper]    Award Paper

Applications

• C. He, M. Sundararajan, A. Datta, A. Derek, J. C. Mitchell, A Modular Correctness Proof of TLS and IEEE 802.11i, in Proceedings of 12th ACM Conference on Computer and Communications Security , pp. 2-15, November 2005. (Invited to ACM Transactions on Information and System Security, Special Issue of Selected Papers from CCS'05.) [ Paper ]    Award Paper
• M. Backes, A. Datta, A. Derek, J. C. Mitchell, M. Turuani, Compositional Analysis of Contract-Signing Protocols, in Proceedings of 18th IEEE Computer Security Foundations Workshop, pp. 94-110, June 2005. [ Paper ]
• C. Meadows, D. Pavlovic, Deriving, attacking and defending the GDOI protocol, in Proceedings of 9th European Symposium On Research in Computer Security, pp. 53-72, September 2004. [ Paper ]

Cryptographic Foundations

A. Roy, A. Datta, A. Derek, J. C. Mitchell, "Inductive Trace Properties for Computational Security", in ACM SIGPLAN and IFIP WG 1.7 7th Workshop on Issues in the Theory of Security, March 2007. (Invited to special issue of Journal of Computer Security.)  [Full paper in preparation]  Award Paper

Tool Support

• Isabelle Proof Assistant for Protocol Composition Logic (Preliminary)
• PDA: Protocol Derivation Assistant

Other Talks

• J. C. Mitchell, Logic for Computer Security Protocols, Plenary Lecture, Association for Symbolic Logic, 2001. [ Slides ]
• D. Pavlovic Protocol Composition and Refinement Patterns, Mathematical Foundations of Programming Semantics, 2003. [ Slides ]
• A. Derek, Logic for Computer Security Protocols, CS259: Security Analysis of Network Protocols, Stanford University, Winter 2004. [ Slides ]
• A. Scedrov, Logic for Computer Security Protocols, MATH690: Mathematical Foundations of Computer Security, University of Pennsylvania, Spring 2004.
• V. Shmatikov, Derivation of the JFK Protocol, CS395T: Design and Analysis of Security Protocols , University of Texas at Austin, Fall 2004. [ Slides ]
• V. Shmatikov, Protocol Composition Logic, CS395T: Design and Analysis of Security Protocols , University of Texas at Austin, Fall 2004. [ Slides ]
• J. C. Mitchell, Security Analysis of Network Protocols: Logical and Computational Methods, Invited Talk, ICALP, July 2005. [ Slides ]
• A. Datta, PCL: A Logic for Security Protocols, 18732: Secure Software Systems, CMU, Fall 2005. [ Slides ]
• H. Mantel, Derivation of Security Protocols, Current Topics in Infomation Security, RWTH Aachen University, Winter 2006.
• J. C. Mitchell, Computationally Sound Formal Logic for Network Security Protocols, Invited Talk, Logic and Computational Complexity, August 2006.
• J. C. Mitchell, Symbolic and Computational Analysis of Network Protocol Security, Invited Talk, ASIAN Computing Science Conference, December 2006. [ Slides ]
• A. Roy, Protocol Composition Logic, CS259: Security Analysis of Network Protocols, Stanford University, Winter 2008. [ Slides ]