Protocol Composition Logic (PCL)

Citations Over TimeTop 1% of 2007 papers

Abstract

Protocol Composition Logic (PCL) is a logic for proving security properties of network protocols that use public and symmetric key cryptography. The logic is designed around a process calculus with actions for possible protocol steps including generating new random numbers, sending and receiving messages, and performing decryption and digital signature verification actions. The proof system consists of axioms about individual protocol actions and inference rules that yield assertions about protocols composed of multiple steps. Although assertions are written only using the steps of the protocol, the logic is sound in a strong sense: each provable assertion involving a sequence of actions holds in any protocol run containing the given actions and arbitrary additional actions by a malicious adversary. This approach lets us prove security properties of protocols under attack while reasoning only about the actions of honest parties in the protocol. PCL supports compositional reasoning about complex security protocols and has been applied to a number of industry standards including SSL/TLS, IEEE 802.11i and Kerberos V5.

Related Papers

• → Automated analysis of cryptographic protocols using Murφ(2002)475 cited
• → Cryptographic design vulnerabilities(1998)184 cited
• → Cryptographic protocol flaws: know your enemy(2002)51 cited
• → Formal Modeling and Analyzing Kerberos Protocol(2009)12 cited
• → Enhancing the Security of Protocols against Actor Key Compromise Problems(2015)