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

## TL;DR

This paper enhances Attack-Defence Trees with reactive patterns and attributes, modeling them as Asynchronous Multi-Agent Systems to enable quantitative security analysis and parametric verification.

## Contribution

It introduces a systematic transformation of ADTs into EAMAS, allowing for quantitative analysis and verification of security scenarios.

## Key findings

- Enriched ADTs with reactive patterns, time, and cost attributes.
- Systematic transformation ensures correctness and enables quantitative analysis.
- Case studies demonstrate the approach using Uppaal and IMITATOR tools.

## Abstract

Attack-Defence Trees (ADTs) are well-suited to assess possible attacks to systems and the efficiency of counter-measures. In this paper, we first enrich the available constructs with reactive patterns that cover further security scenarios, and equip all constructs with attributes such as time and cost to allow quantitative analyses. Then, ADTs are modelled as (an extension of) Asynchronous Multi-Agents Systems--EAMAS. The ADT-EAMAS transformation is performed in a systematic manner that ensures correctness. The 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. Our approach is exercised on several case studies using the Uppaal and IMITATOR tools.