Tableau methods for formal verification of multi-agent distributed systems

Formal verification is a key step in the development of trusted and reliable multi-agent distributed systems. This is particularly relevant when security concerns such as privacy, integrity and availability impose limitations on the operations that can be performed on sensitive data. The aim of access control is to limit what agents (humans, programs, softbots, etc.) of distributed systems can do directly or indirectly by delegating their powers and tasks. As the size of the systems and the sensitivity of data increase, the availability of automated reasoning methods becomes essential for logical analysis of access control. This paper presents a prefixed tableau method for the calculus of access control developed at the Digital System Research Center. This calculus is particularly interesting for a number of reasons. First it was the basis for the development and the verification of an implemented system. Second, it poses many technical challenges for classical modal tableaux: it lacks the tree-model property, has some features of the universal modality, and can introduce delegation certificates between agents "on-the-fly" not compilable into axiom schemata.