Model checking detectability of attacks in multiagent systems - Boureanu,I; Cohen,M; Lomuscio,A (2010)
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. Copyright © 2010, International Foundation for Autonomous Agents and Multiagent Systems (www.ifaamas.org). All rights reserved.