Security protocols enable useful tasks over untrusted networks. For example, confidential communication over the Internet between users and Web services like Google, Facebook, Amazon and Bank of America rely on protocols like SSL/TLS and the supporting Public Key Infrastructure (PKI). These protocols are designed to provide global security properties like authentication and confidentiality when various parties (e.g., the user, the Web service, and participants in the PKI such as certificate authorities) execute their prescribed programs. However, when individual parties deviate from their prescribed programs and the global security property is violated, it is important to hold agents accountable by detecting deviant behavior and determining which deviations actually caused the violation. Such determinations are useful in a wide range of distributed security settings, including in protocols for authentication and key exchange, electronic voting, and online auctions.
This project develops logic and language-based methods for deviance and causal determination in distributed systems. The project addresses the following scientifically challenging tasks: (1) Developing a language for distributed computing in which prescribed behavior of agents are represented with contracts. The contracts are specified via types and a type-directed distributed monitoring infrastructure is designed to detect deviance from contracts. The technical approach is based on novel dependent and stateful session types to express and verify security-relevant properties of systems. (2) Developing a formal blame semantics for distributed systems that is extensional (protocol- or system-independent). Recognizing that some deviations may not affect the security property, the blame semantics combines deviance from contracts with a novel definition of programs as actual causes of global security properties. The formalization of actual causation in this setting, while inspired by counterfactual theories of actual causation in philosophy and in computer science, goes beyond those theories by dealing with interacting distributed programs with nondeterministic operational semantics. (3) Applications of these methods to conduct a comprehensive study of proposed protocols for augmenting accountability in the public key infrastructure.
The project has potential for significant broader impact on society. Recent results have exposed the fragility of the Public Key Infrastructure on which hundreds of millions of people around the world rely to protect their communication over the Internet. A systematic basis for design, analysis, and comparison of protocols that improve accountability of the PKI can help protect Internet users from malicious adversaries who seek to snoop on their communications. The project also provides extensive training and educational opportunities for undergraduate and graduate students at Carnegie Mellon University.
