To know or not to know: Epistemic approaches to security protocol verification (Q625717)

The authors survey the epistemic approaches to security protocol verification with the questions: are security protocols essentially about knowledge (what is there to know), what kind of knowledge can we distinguish (how to know), and does an epistemic approach bring benefits (why to know)? First they distinguish between different types of knowledge relevant in the security setting, and then give an overview of commonly used techniques in the epistemic approaches. In particular, they compare various equivalence relations defined in the literature (simple deduction equivalence, pattern matching equivalence, static equivalence, permutation equivalence) that correspond to the semantics of propositional knowledge. They also compare two major epistemic logical approaches proposed to model interaction in multi-agent systems. It turns out that, in the security protocol verification setting, ETL (epistemic temporal logic) approaches are more suitable to model message passing over time, based on which appropriate equivalence relation can be generated. On the other hand, the DEL (dynamic epistemic logic) approach offers all freedom to model higher-order information and uncertainties in term of agents' knowledge about each other. The model checker results of ETL also confirm that it is better to focus on a single agent case: in security setting, this would be the intruder. Finally, they collect clues for the comparison of expressivity of ETL and TL (temporal logic), in order to see when an epistemic approach is inevitable. They show under the assumption of synchronicity, that ETL can define more (security) properties of the temporal structures.