Hackers vs. Security: Attack-Defence Trees as Asynchronous Multi-Agent Systems

Jaime Arias (1, 2) , Carlos E. Budde (3) , Wojciech Penczek (4) , Laure Petrucci (2) , Teofil Sidoruk (4, 5) , Mariëlle Stoelinga (3)

1 CNRS - Centre National de la Recherche Scientifique
2 LIPN - Laboratoire d'Informatique de Paris-Nord
3 FMT group - Formal Methods and Tools
4 Institute of Computer Science [Warszawa]
5 Warsaw University of Technology [Warsaw]

Attack-Defence Trees (ADTrees) are a well-suited formalism to assess possible attacks to systems and the efficiency of countermeasures. This paper extends the available ADTree constructs with re-active 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.

Domaines: Cryptographie et sécurité [cs.CR]; Système multi-agents [cs.MA]; Modélisation et simulation; Mathématiques [math]

Jaime Arias, Carlos E. Budde, Wojciech Penczek, Laure Petrucci, Teofil Sidoruk, et al.. Hackers vs. Security: Attack-Defence Trees as Asynchronous Multi-Agent Systems. 22nd International Conference on Formal Engineering Methods (ICFEM 2020), Mar 2021, Singapore, Singapore. pp.3-19, ⟨10.1007/978-3-030-63406-3_1⟩. ⟨hal-02902348⟩