Model checking detectability of attacks in multiagent systems

Information security is vital to many multiagent system applications. In this paper we formalise the notion of detectability of attacks in a MAS setting and analyse its applicability. We introduce a taxonomy of detectability specifications expressed in temporal-epistemic logic. We illustrate the practical relevance of attack detectability in a case study applied to a variant of Kerberos protocol. We model-check attack detectability in automatically generated MAS models for security protocols. Categories and Subject Descriptors D.2.4 [Software/Program Verification]: Model checking General Terms Verification, Security Keywords Verification of MAS; Logics of Agency; Logic-based approaches and methods; Privacy, safety and security; Formal models of agency

• Type: Conference
• Year: 2010
• Where: ATAL
• Authors: Ioana Boureanu, Mika Cohen, Alessio Lomuscio
• Keywords: ATAL 2010, Attack Detectability, Detectability, Intelligent Agents, Model-check Attack Detectability