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.
Boi Faltings, Sujit Prakash Gujar, Dimitrios Chatzopoulos, Anurag Jain
Serge Vaudenay, Andrea Felice Caforio, Daniel Patrick Collins, Hailun Yan