Reasoning about resource-bounded knowledge: theory and application to security protocol analysis
Joseph Halpern, Riccardo Pucella · 2004
Existing approaches for analyzing security protocols, while quite successful, are limited in a number of ways. One limitation is that they often do not supply a specification language. Another limitation is that the model of the adversary is quite restricted, unable to capture protocol-specific knowledge or to support guessing. Informal specifications of security in the literature are typically phrased in terms of knowledge. It thus seems natural to use an epistemic logic as a specification language, where specifications can be written directly in terms of knowledge. However, the standard interpretation of knowledge in such logics suffers from the logical omniscience problem: agents know all logical consequences of their knowledge. This gives a notion of knowledge too strong for the purpose of reasoning about security, since the adversary knows information that no realistic adversary should know. Using a notion known as algorithmic knowledge it is possible to define a logic for reasoning about security protocol under different adversary models, where adversaries use algorithms to compute their knowledge. The contributions of this dissertation are two-fold. Firstly, I develop the theory of algorithmic knowledge in more depth. More precisely, I investigate the properties of the logic when the knowledge algorithms implement deductions in a logical theory for the agents and when the knowledge algorithms are randomized. Dealing with specifications in the presence of randomized knowledge algorithms requires a notion of evidence, a concept heavily studied in the philosophical literature, but not so much in computer science. Secondly, I develop a logic for reasoning about security protocols based on the well-understood notions of knowledge, time, and probability, as well as algorithmic knowledge to capture the capabilities of the adversary. I show this logic is flexible enough to capture many of the adversaries considered in the literature. I finally provide evidence that this logic is sufficiently expressive to reason about security protocols: it can captures subtleties in the handling of nonces that are not captured by non-epistemic approaches to security protocol analysis, and it can capture many operators believed to be important for security protocol analysis.