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
The following paper provides an overview of this project. For further details, please read the other papers included below.
Methodology
· 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.
· 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.
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 ]