Stanford Security Lab

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 papers and set of slides provides an overview of this project. For further details, please read the other papers included below.

  • A. Datta, J. C. Mitchell, A. Roy, S. H. Stiller, Protocol Composition Logic, to appear as a book chapter in an upcoming publication of IOS Press, July 2010. [ Paper ] [ Execution trace and full proof ]    symbolic PCL | detailed presentation of PCL with a new semantics; challenge-response: auth

  • 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 ]    symbolic PCL | ISO-9798-3: authentication, secrecy

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

Also see the model-checking page for related projects.

The following table shows what we proved (eg: authentication, secrecy) about which protocols, using PCL:

Protocol/topicWhat we proved/discussed
Diffie-Hellmanauthentication, secrecy (M3); secrecy for symmetric keys (C1; M16); discussion (M15)
GDOIfound flaw, proposed fix (A1)
Asokan-Shoup-Waidnerfairness, accountability, abuse-freeness (A2)
Garay-Jacobson-MacKenziefairness, accountability, abuse-freeness (A2)
TLSauthentication, secrecy (A3)
IEEE 802.11iauthentication, secrecy (A3)
EAP-GPSKfound three weaknesses, proposed fixes (A4); authentication, secrecy for fixed version (A4)
Needham-Schroederattack (M1)
Needham-Schroeder-Lowecorrectness (M1)
variant of Needham-Schroedersecrecy (M10; M14)
JFKcase study (M2); discussion (M5; M6)
CRauthentication, secrecy (M3)
ISO-9798-2authentication (initiator) (M5)
ISO-9798-3authentication (initiator) (M5); authentication, secrecy (M3; M4; M5; M6; M11); key usability (M9)
SKID3authentication (initiator) (M5)
IKEdiscussion (M5; M6)
IKEv2authentication, secrecy (M13); discussion (M15)
STSdiscussion (M6)
Kerberos V5authentication, secrecy (M10; M12; M14); discussion (M15)
Diffie-Hellman variant of Kerberosauthentication, secrecy, found deficiency (M13)
papers with expository contentcomputational PCL (M7); derivation of complex protocols by composition/refinement/transformation (M8); computational soundness of symbolic protocol analysis (M8); detailed presentation of PCL with a new semantics (M17)

The following table shows which papers use symbolic and which ones use computational PCL:

Symbolic or computational PCLPaper
symbolic PCLA1, A2, A3, A4, M1, M2, M3, M4, M5, M6, M8, M10, M11, M14, M17
computational PCLC1, M6, M8, M9, M12, M13, M15, M16

Publications

Methodology

  • [M17] A. Datta, J. C. Mitchell, A. Roy, S. H. Stiller, Protocol Composition Logic, to appear as a book chapter in an upcoming publication of IOS Press, July 2010. [ Paper ] [ Execution trace and full proof ]    symbolic PCL | detailed presentation of PCL with a new semantics; challenge-response: auth

  • [M16] A. Roy, A. Datta, A. Derek, J. C. Mitchell, Inductive Trace Properties for Computational Security, to appear in Journal of Computer Security, 2010. [ Paper ]    computational PCL | Diffie-Hellman: secrecy for symmetric keys
  • [M15] A. Roy, Formal Proofs of Cryptographic Security of Network Protocols, PhD Thesis, Computer Science Department, Stanford University, December 2009. [ Thesis ]    computational PCL | computational PCL, secrecy, Diffie-Hellman, Kerberos, IKEv2
  • [M14] 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 ]    symbolic PCL | variant of Needham-Schroeder: secrecy; Kerberos V5: authentication, secrecy
  • [M13] 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 ]    computational PCL | Diffie-Hellman variant of Kerberos: authentication, secrecy, found deficiency; IKEv2: authentication, secrecy
  • [M12] 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 ]    computational PCL | Kerberos V5: authentication, secrecy
  • [M11] 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 ]    symbolic PCL | ISO-9798-3: authentication, secrecy
  • [M10] 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 ]    symbolic PCL | variant of Needham-Schroeder: secrecy; Kerberos V5: authentication, secrecy
  • [M9] 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 ]    computational PCL | ISO-9798-3: key usability
  • [M8] A. Datta, Security Analysis of Network Protocols: Compositional Reasoning and Complexity-theoretic Foundations, PhD Thesis, Computer Science Department, Stanford University, September 2005. [ PS ] [ PDF ]    symbolic PCL, computational PCL | derivation of complex protocols by composition/refinement/transformation, computational soundness of symbolic protocol analysis
  • [M7] 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    computational PCL | introduces computational PCL
  • [M6] 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 ]    symbolic PCL | ISO-9798-3: authentication, secrecy; also discussed: STS, JFK, IKE
  • [M5] 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 ]    symbolic PCL | ISO-9798-2, ISO-9798-3, SKID3: authentication (initiator); ISO-9798-3: authentication, secrecy; also discussed: JFK, IKE
  • [M4] A. Datta, A. Derek, J. C. Mitchell, D. Pavlovic, Secure Protocol Composition.    symbolic PCL | ISO-9798-3: authentication, secrecy
    • 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 ]
  • [M3] 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    symbolic PCL | CR: authentication, secrecy; Diffie-Hellman: authentication, secrecy; ISO-9798-3: authentication, secrecy
  • [M2] A. Datta, J. C. Mitchell, D. Pavlovic, Derivation of the JFK Protocol, Kestrel Institute Technical Report, KES.U.02.03, July 2002.  [ TR ] [ slides ]    symbolic PCL | case study of JFK
  • [M1] N. Durgin, J. C. Mitchell, D. Pavlovic, A Compositional Logic for Proving Security Properties of Protocols.    symbolic PCL | Needham-Schroeder: attack, Needham-Schroeder-Lowe: correctness
    • 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

  • [A4] J. C. Mitchell, A. Roy, P. Rowe, A. Scedrov, Analysis of EAP-GPSK Authentication Protocol, in Proceedings of Applied Cryptography and Network Security, 6th International Conference, pp. 309-327, June 2008. [ Paper ]    symbolic PCL | EAP-GPSK: found three weaknesses, proposed fixes, proved authentication and secrecy for fixed version
  • [A3] 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    symbolic PCL | TLS: authentication, secrecy; IEEE 802.11i: authentication, secrecy
  • [A2] 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 ]    symbolic PCL | Asokan-Shoup-Waidner: fairness, accountability, abuse-freeness; Garay-Jacobson-MacKenzie: fairness, accountability, abuse-freeness
  • [A1] 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 ]    symbolic PCL | GDOI: a flaw is found and a fix is proposed

Cryptographic Foundations

  • [C1] 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    computational PCL | Diffie-Hellman: secrecy for symmetric keys

Tool Support

Other Talks