A Spatial-Epistemic Logic for Reasoning About Security Protocols
Reasoning about security properties involves reasoning about where the information of a system is located, and how it evolves over time. While most security analysis techniques need to cope with some notions of information locality and knowledge propagation, usually they do not provide a general language for expressing arbitrary properties involving local knowledge and knowledge transfer. Building on this observation, the authors introduce a framework for security protocol analysis based on dynamic spatial logic specifications. Their computational model is a variant of existing calculi, while specifications are expressed in a dynamic spatial logic extended with an epistemic operator. They present the syntax and semantics of the model and logic, and discuss the expressiveness of the approach, showing it complete for passive attackers.