In this talk we present PCL - a logic for proving security properties of network protocols. Two central results for this logic are a "composition theorem" and a "computational soundness theorem". The composition theorem allows proofs of complex protocols to be built up from proofs of their constituent sub-protocols. It is formulated and proved by adapting ideas from the assume-guarantee paradigm for reasoning about distributed systems. The computational soundness theorem guarantees that, for a class of security properties and protocols, axiomatic proofs in PCL carry the same meaning as hand-proofs done by cryptographers. The soundness proof uses standard proof techniques from cryptography, in particular, complexity-theoretic reductions. PCL has been successfully applied to a number of internet, wireless and mobile network security protocols developed by the IEEE and IETF Working Groups, in several cases identifying serious security vulnerabilities.
Logic and Computation Seminar
Wednesday, November 16, 2005 - 3:00pm
Anupam Datta
Stanford University