Protocol Composition Logic (PCL)

TLDR

Protocol Composition Logic (PCL) is a logic for proving security properties of network protocols that use public and symmetric key cryptography. PCL enables proving security properties of protocols under attack by reasoning only about the actions of honest parties. PCL is built on a process calculus with actions for generating random numbers, sending and receiving messages, and performing decryption and signature verification, and its proof system uses axioms about individual actions and inference rules to derive assertions about composed protocols. PCL is sound: any provable assertion about a sequence of actions holds in all protocol runs containing those actions, and it has been applied to industry standards such as SSL/TLS, IEEE 802.11i, and Kerberos V5.

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.