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. 3 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 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 (Gordon D. Plotkin Festschrift), to appear 2007. [ Paper ]

Publications:

    Methodology

  • A. Roy, A. Datta, A. Derek, J. C. Mitchell, Inductive Trace Properties for Computational Security, to appear in Journal of Computer Security, 2009. [ Paper]
  • A. Roy, A. Datta, A. Derek, J. C. Mitchell, J.-P. Seifert, Secrecy Analysis in Protocol Composition Logic, in Formal Logical Methods for System Security and Correctness, IOS Press, 2008. [ Paper ]
  • A. Roy, A. Datta, J. C. Mitchell, Formal Proofs of Cryptographic Security of Diffie-Hellman based Protocols, in Proceedings of 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. [ Paper ]
  • A. Datta, A. Derek, J. C. Mitchell, A. Roy, Protocol Composition Logic (PCL), in Electronic Notes in Theoretical Computer Science (Gordon D. Plotkin Festschrift), 2007. [ Paper ]    Invited Paper

·         A. Datta, A. Derek, J. C. Mitchell, A. Roy, Protocol Composition Logic (PCL), Electronic Notes in Theoretical Computer Science (Gordon D. Plotkin Festschrift), to appear 2007. [ 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

·         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 ]

Tool Support:

Other Talks: