Tue Nov 21, 2006, 4:15-5:15, 4000A Math Sciences. 

Reasoning about Security and Privacy

Anupam Datta
Stanford University

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 hand-proofs done by cryptographers. 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.

About the speaker:
Anupam Datta is a Research Associate in the Computer Science Department at
Stanford University. He obtained PhD (2005) and MS (2002) degrees in
Computer Science from Stanford University and a BTech from IIT Kharagpur
(2000).

Host: Jens Palsberg.