ABSTRACT
PCL is a logic for proving security properties of network protocols. Two central
results for PCL are a set of composition theorems and a computational soundness
theorem. The composition theorems allow proofs of complex protocols to be built
up from proofs of their constituent sub-protocols. The computational soundness
theorem guarantees that, for a class of security properties and protocols,
axiomatic proofs in PCL carry the same meaning as reduction-style cryptographic
proofs. 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. Specific
applications include the IEEE 802.11i wireless security standard, and the IETF
IKEv2, Kerberos and GDOI standards.
BIOGRAPHY
Anupam Datta joined the research faculty at CMU in April 2007. Prior to that he
was a postdoctoral research associate at Stanford University. He obtained PhD
(2005) and MS (2002) degrees from Stanford, and a BTech from IIT Kharagpur
(2000), all in Computer Science. Anupam's research interests are in security,
cryptography and privacy. Specific topics include security analysis of network
protocols, theory of cryptography, languages for privacy policy specification
and enforcement, and software system security.