Security Protocol Analysis and Algorithmic Knowledge
For the past two decades, logical approaches to security protocol analysis have been based on notions of knowledge used to reason about distributed computing. Unfortunately, the classical notion of knowledge is often inappropriate in a security context. Specifically, modeling the knowledge of the intruder using an information-theoretic definition of knowledge does not easily yield common adversary models such a Dolev-Yao, is not very flexible, and more importantly, does not take into account the computational capabilities of the adversary. We show how we can analyze security protocols under different adversary models by using a logic with a notion of algorithmic knowledge. Roughly speaking, adversaries are assumed to use algorithms to compute their knowledge; adversary capabilities are captured by suitable restrictions on the algorithms used. It is straightforward to model the standard Dolev-Yao adversary in this setting, and to extend Dolev-Yao with protocol-specific knowledge and probabilities.