An Automated Approach for Proving PCL Invariants

Protocol composition logic, PCL, is a formal approach for proving security properties of a class of network protocols. PCL involves reasoning directly about properties achieved by protocols steps, in a setting that does not require explicit reasoning about attacker actions. The method relies on protocol invariants to combine properties of different roles of a protocol. While some protocol invariants can be complex to identify and prove, many useful PCL invariants are relatively straightforward consequences of the programs (roles) executed by the agents involved in the protocol. We present a logic program based approach for automating proofs of invariants that appears effective for invariants that are required for several standardized, widely deployed protocols. We use the well-known Transport Layer Security Protocol (TLS/SSL) to illustrate the approach.