My research focus is on developing principled methods for modeling, analysis, and design of security mechanisms that are applicable to real-world systems. In this talk, I will present two examples. In the first part, I will describe PCL - a logic for proving security properties of network protocols. This logic 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. Two central results for PCL are a composition theorem and a computational soundness theorem. In contrast to traditional folk wisdom in computer security, the composition theorem allows 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 proofshand-proofs. In the remaining time, I will describe my current work on LPU - a logic for stating and enforcing privacy policies and its application to problems in medical privacy. One significant contribution of this work is the reduction of problems pertaining to policy compliance, combination and refinement to standard decision procedures in temporal logic.
Anupam Datta is a Research Associate in the Computer Science Department at Stanford University. He obtained PhD (2005) and MS (2002) degrees from Stanford University and a BTech from IIT Kharagpur (2000), all in Computer Science.