Deciding knowledge properties of security protocols
R. Ramanujam, S. P. Suresh · 2005
Logics for specifying properties of security protocols and reasoning about them have received increasing attention over the past few years. In this paper, we propose a propositional logic of knowledge, augmented with tense modalities, in which many important properties of security protocols can be naturally expressed. We also describe in some detail the protocol model, which helps provide a precise and general semantics for the logic. The main technical result is the decidability of the verification problem for the logic.