Protocol Composition Logics

Опубликовано 6 сентября 2016, 5:34

The design and analysis of network protocols that use cryptographic primitives is one of the most fundamental and challenging areas of security research. In this talk, I will present logical methods for protocol analysis that address two central problems in this area. The first is compositionality, where the goal is to develop methods for proving correctness of compound protocols by combining independent proofs of their components. Protocol Composition Logic (PCL) is a Floyd-Hoare style logic that supports axiomatic proofs of protocol properties. Protocol proofs in PCL are compositional and follow the designer intuition when constructing protocols using standard components. The second research goal is to develop symbolic methods for protocol analysis while being faithful to the complexity-theoretic model of modern cryptography. Our first result here is Computational PCL - a symbolic logic with syntax and proof system similar to PCL. However, the semantics of CPCL is defined with respect to the complexity-theoretic model of cryptography. These methods have been successfully applied to a number of network security protocols including the IEEE 802.11i wireless authentication protocol, IPSec's new key exchange protocol IKEv2, and SSL/TLS.