Publications

Expressing attack-defence trees in a multi-agent setting allows for studying a new aspect of security scenarios, namely how the number of agents and their task assignment impact the performance, e.g. attack time, of strategies executed by opposing coalitions. Optimal scheduling of agents’ actions, a non-trivial problem, is thus vital. We discuss associated caveats and propose an algorithm that synthesises such an assignment, targeting minimal attack time and using minimal number of agents for a given attack-defence tree

Expressing attack-defence trees (ADTrees) in a multi-agent setting allows for studying a new aspect of security scenarios, namely how the number of agents and their task assignment impact the performance of attacking and defending strategies executed by agent coalitions. Our tool ADT2AMAS allows for transforming ADTrees into extended asynchronous multi-agent systems and computing an optimal schedule with the minimal number of agents. ADT2AMAS is integrated within the graphical verification platform CosyVerif, but can also be run standalone.

In earlier work, we presented translations of attack-defence trees (ADTrees) to extended asynchronous multi-agent systems. By avoiding some sequences, agent models constructed via these transformations already embed state space reductions. Here, we introduce Guarded Update Systems and their synchronisation topology, allowing us to define a new general reduction scheme that applies to tree topologies, and in particular to ADTrees. The reduction exploits the layered structure of a tree by avoiding unnecessary interleavings between nodes at different depths. We prove the soundness of this new method and present extensive experimental results, including scalable models, to demonstrate it can be effectively used alongside previously employed techniques.

Attack-Defence Trees (ADTrees) are a well-suited formalism to assess possible attacks to systems and the efficiency of counter-measures. This paper extends the available ADTree constructs with reactive patterns that cover further security scenarios, and equips all constructs with attributes such as time and cost to allow for quantitative analyses. We model ADTrees as (an extension of) Asynchronous Multi-Agents Systems: EAMAS. The ADTree–EAMAS transformation allows us to quantify the impact of different agents configurations on metrics such as attack time. Using EAMAS also permits parametric verification: we derive constraints for property satisfaction, e.g. the maximum time a defence can take to block an attack. Our approach is exercised on several case studies using the Uppaal and IMITATOR tools. We developed the open-source tool adt2amas implementing our transformation.