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.

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.

Tables

Table 1. Table 1 : ADT constructs (selection) and their semantics

Name	Domains	Graphics	Semantics
Attack	$a\in {\Sigma }_a$		$a$
Defence	$d\in {\Sigma }_d$		$d$
And attack	$A,a{}_1{}^{},\cdots ,a{}_n{}^{}\in {\Sigma }_a$	​​	$A=a{}_1{}^{}\wedge \cdots \wedge a{}_n$
Or defence	$D,d{}_1{}^{},\cdots ,d{}_n{}^{}\in {\Sigma }_d$	​​	$D=d{}_1{}^{}\vee \cdots \vee d{}_n$
Counter defence		​​	$A=a\wedge \neg d$
No defence		​​	$A=a\vee \neg d$
Inhibiting attack		​​	$D=d\vee \neg a$
Sequential and attack	$A,a{}_1{}^{},\cdots ,a{}_n{}^{}\in {\Sigma }_a$	​​	$A=a{}_1{}^{}\wedge \cdots \wedge a{}_n$
Failed reactive defence		​​	$A=a\wedge \neg d$

Table 2. Table 2 : ADT nodes and corresponding agent models

ADT construct	Agent model
Leaf node
Conjunction/disjunction nodes
​​
​​
Countering nodes
​​
Sequential nodes

Equations

$$f\left(init\_time(\mathtt{ST}),g(init\_time(\mathtt{b}),init\_time(\mathtt{f}))\right)$$

$$\mathtt{AND}({\mathtt{SAND}}_1({\mathtt{a}}_1,{\mathtt{a}}_2),{\mathtt{SAND}}_2({\mathtt{a}}_2,{\mathtt{a}}_3))$$

$$time(\mathtt{AND})=\sum _{i=1}^{3}init\_time({\mathtt{a}}_{\mathtt{i}})+\sum _{j=1}^{2}init\_time({\mathtt{SAND}}_j).$$

Full text

1 Introduction

Over the past ten years of security analysis, a multitude of formalisms has been developed to study interactions between attacker and defender parties. Attack-defence trees stand out among these, as a graphical, straightforward formalism of great modelling versatility. However, research is thus far focused on bipartite graph characterisations, where nodes belong to either the attacker or defender party. In real security scenarios each of these parties may be formed of multiple agents. Agents distribution over the tree nodes, i.e. which agent performs which task for which goal, determines not only the performance but also the feasibility of an attack or defence strategy. Studying these distributions is thus paramount.

To analyse the impact of different agents distributions, we model attack-defence trees in an agent-aware formalism. Our approach permits quantifying performance metrics (e.g. cost and time) of attack/defence strategies under distinct agents coalitions. Employing modern verification tools such as IMITATOR, we determine the feasibility of coalition strategies, and synthesise the value of the attributes that make them feasible, such as the maximum time allowed for a defence mechanism to be triggered. This way, we make an important step towards richer ADT representations for real-world security analysis.

Contributions.

Concretely, in this paper we introduce:

($i$) a unified scheme for ADT representation with counter- and sequential operators, including a new construct;

($ii$) a formalism—EAMAS—to model ADTs where all nodes have attributes, and can be operated by different agents;

($iii$) compositional and sound transformation rules from ADT to EAMAS;

($iv$) measurements of the impact of different agents coalitions on attack performance metrics, such as time, exercised on several case studies;

($v$) synthesis of ADT attributes—by encoding them as EAMAS parameters—for feasibility analysis of attack/defence strategies.

Outline.

The paper is structured as follows. In Sec. 2 we review the basic notions of ADTs, using a unified syntactic and semantic representation. Sec. 3 reviews the AMAS formalism, which we extend in Sec. 4 to model ADTs enriched with attributes. Sec. 5 presents graph-based transformation patterns to model each ADT construct as an (extended) AMAS model. Such compositional modelling avoids state space issues; we prove it correct for our semantics and illustrate it in our running example. The effectiveness of our approach is demonstrated in Sec. 6, by using two state-of-the-art verification tools to quantitatively analyse three case studies from the literature. This work concludes in Sec. 7, where we finally draw possible lines of future research.

2 Attack-Defence Trees

2.1 The basic ADT model and related work

Attack trees are well-known tree-like representations of attack scenarios, that allow for evaluating the security of complex systems to the desired degree of refinement [MO06]. The root of the tree is the attacker’s goal, and the children of a node represent refinements of the node’s goal into sub-goals. The tree leaves are (possibly quantified) foreseeable attacker’s actions. For instance, if the attack goal is to Steal Jewels from a museum (SJ), where burglars must break in (attack leaf bi) and force a display (fd), the attack tree is: $\mathtt{SJ}=\mathtt{{AND}}(\mathtt{bi},\mathtt{fd})$.

Attack-defence trees (ADTs, [KMRS11]) are an extension of attack trees including possible counteractions of a defender, thus representing security scenarios as an interplay between attacker’s and defender’s actions. This can model mechanisms triggered by the occurrence of specified opposite actions. So for instance, the jewels burglary will succeed (SJS) only if all attack actions are performed, and the alerted police (p) doesn’t stop them: $\mathtt{SJS=\mathtt{{NAND}}(SJ,p)}$, see Fig. 1.

Countering actions emerged recently to express pointwise interactions between opposite players. This can be reactive, such as the police above, or passive, such as message encryption to avoid eavesdropping in open channels. The intuition behind the counter actions in [KMRS11] can be described as follows:

• $\blacktriangleright$

counter defence $A=\mathtt{{NAND}}(a,d)$: if attack $a$ succeeds and the countering defence $d$ fails, then the attack goal $A$ is successful;

• $\blacktriangleright$

counter attack $D=\mathtt{{NAND}}(d,a)$: if defence $d$ happens and attack $a$ fails, then the defence goal $D$ is successful.

Formally, we give Boolean semantics to the nodes composing ADTs as shown in Table 1. As with counter defence/attack above, constructs are symmetric for attack or defence goals; thus the table shows only a selection. In the graphical

representations, triangular nodes indicate (arbitrary) subtrees can be the children of a gate, whereas circular (resp. rectangular) nodes represent attack (resp. defence) leaves. In this way, with Table 1 we extend [KMRS11] with $\mathtt{{AND}}$/$\mathtt{{OR}}$ gates along the lines of [KSR*+*18]. We further extend notation—in accordance with these semantics—for nodes that represent countering a defence or an attack. Thus, for instance, the ADT jewels burglary example has the semantics $\mathtt{SJS=bi\land fd\land\lnot p}$, graphically depicted as in Fig. 1.

In Table 1 we also introduce operators for a choice between a successful attack and a failing defence (named no defence), and vice-versa (inhibiting attack). These constructs are less usual in the literature [KPS14], yet they model realistic scenarios such as attack goals succeeding by security negligence rather than by performing an elaborated (and costly!) attack. This is of interest for quantitative analyses of e.g. cost and probability, and thus we include them in Table 1.

Moreover, we consider sequential order operators, which lack a standard interpretation for ADTs. The survey of [KPS14] lists several ways to model order-dependent events: sequential enforcement, time dependent ordered-$\mathtt{{AND}}$, priority- or sequential-$\mathtt{{AND}}$, etc. For attack trees, in the sequentially ordered conjunction ($\mathtt{{SAND}}$) of [JKM*+*15], attacks succeed when all children occurred in the required order. This abstracts away the exact time of occurrence of events; with few exceptions, e.g. [ÇY07], this is the preferred approach in the literature [SSSW98, BLP*+*06, KPS14, JKM*+*15, KSR*+*18]. Therefore $\mathtt{{SAND}}$s describe the order in which actions will take place, rather than a potential order of events. Their role is to enforce sequential events and rule out parallel executions, which is a fundamental construct when working with multi-agent systems. For instance, Steal Jewels (SJ) in Fig. 1 is modelled with an $\mathtt{{AND}}$ gate. Say that breaking in (bi) takes 10 min and forcing the display (fd) 5 min. If two attackers operate in parallel, analysing the ADT can conclude that SJ succeeds after a 10 min attack. But fd depends logically on bi, since the display can only be forced after breaking in. Using instead a $\mathtt{{SAND}}$ gate for SJ enforces this sequentiality so that attacks cannot take less than 15 min. We integrate such $\mathtt{{SAND}}$ gates in our ADT framework, as the sequential and attack/defence in Table 1.

We further introduce $\mathtt{{SNAND}}$ gates: sequential gates that have attacks and defences as children. To the best of our knowledge, this is novel in a typed setting where subtrees (rather than leaves) can be assigned attack/defence goals. This contribution is conservative: it extends the $\mathtt{{SAND}}$ gates of [JKM*+*15] to coincide with previous works on sequential operators in defence-aware representations, e.g. attack-defence diagrams [HKKS16]. We distinguish two scenarios: a successful attack followed by a failed defence (named failed reactive defence in Table 1), and vice versa. We disregard the second scenario as uninteresting—it models defence goals which depend on attacks failing by themselves—and focus on the first one. $\mathtt{{SNAND}}$s then model an attack goal that must overcome some reactive defence, triggered only after the incoming attack has been detected.

2.2 Attributes and agents for ADTs

Attributes (also “parameters” and “gains” [BLP*+*06, AN15, KSR*+*18]) are numeric properties of attack/defence nodes that allow for quantitative analyses. Typical attributes include cost, time, and probability: in the Steal Jewels example, the 10 min it takes to break in is a time attribute of this attack leaf. If all nodes in an ADT have a time attribute, one can compute the min/max time required by the attack goal, whereas in general attributes are associated to tree leaves. As in [ALRS19], attributes can be parameters over which we synthesize constraints indicating which attribute values can lead to a successful attack.

General attributes.

We extend attributes to all constructs (i.e. nodes) in ADTs, because a construct may not be fully described by just its children. An attribute is then given by a node’s initial (aka intrinsic) value, and a computation function. For example, refine bi to be an $\mathtt{{AND}}$ gate with children pick main lock (pml, 7 min) and saw padlock (sp, 2 min). Then it may still take an extra minute to enter stealthily and locate the correct display, to be counted after pml and sp have succeeded. In general, when the goal of a gate is successful, its attribute value is the result of its computation function applied to its intrinsic value and to the attributes of its children. For bi, if two burglars cooperate, the computation function is $\mathit{init\_time}(\mathtt{bi})+\max(\mathit{init\_time}(\mathtt{pml}),\mathit{init\_time}(\mathtt{sp}))$. This allows for flexibility in describing different kinds of attributes, and gains special relevance when considering coalitions of agents, as we will further illustrate in Sec. 2.3.

Agents.

Each action described by an ADT construct can be performed by a particular agent. Different attacks/defences could be handled by one or multiple agents, which allows to express properties on agents coalitions. For instance, in the original Steal Jewels example of Fig. 1, the minimal number of burglars required to minimise the SJS attack time is two: one to do bi and another to parallelly perform fd. If the SJ gate is changed to a $\mathtt{{SAND}}$, then one burglar suffices, since bi and fd cannot be parallelised. Upon using the refinement $\mathtt{bi=\mathtt{{AND}}(pml,sp)}$, then again a coalition of two burglars minimises the attack time, since pml and sp can be parallelised. Each node in the ADT will thus be assigned to an agent, and a single agent can handle multiple nodes. In the general case, the only constraint is that no agent handles both attack and defence nodes. As shown above, specific ADTs might enforce additional constraints.

Conditional counter measures.

It may happen that a countering node has a successful or unsuccessful outcome depending on the attributes of its children. We therefore associate conditions with countering nodes, which are Boolean functions over the attributes of the ADT. When present, the condition then comes as an additional constraint for the node operation to be successful.

2.3 Example: Treasure hunters

We present a simple running example in Fig. 2 that extends Fig. 1, featuring thieves that try to steal a treasure in a museum. To achieve their goal, they first must access the treasure room, which involves distracting and bribing a guard (b), and forcing the secure door (f). Both actions are costly and take some time. Two coalitions are possible: it may be that a single thief has to carry out both actions, or there could be two thieves that collaborate to parallelise b and f.

After these actions succeed the thieves can steal the treasure ($\mathtt{{ST}}$), which takes a little time for opening its display stand and putting it in a bag. Then

the thieves are ready to flee ($\mathtt{{TF}}$), but to do that they have to choose an escape route to go away ($\mathtt{{GA}}$): this can be a spectacular escape in a helicopter (h), or a mundane escape via the emergency exit (e). The helicopter is expensive but fast while the fire exit is slower but at no cost. These values will allow for experimenting different solutions. Furthermore, the time to perform a successful escape can be inversely proportional to the number of agents involved in the robbery. This is easy to encode via a computation function in the gate $\mathtt{{GA}}$.

As soon as the treasure room is penetrated (i.e. after b and f but before $\mathtt{{ST}}$) an alarm goes off at the police station, so while the thieves flee the police hurries to intervene (p). The treasure is then successfully stolen iff the thieves have fled and the police failed to arrive (e.g. because they were on strike111https://en.wikipedia.org/wiki/2013_police_revolts_in_Argentina) or does so too late. This last possibility is captured by the additional condition associated with the treasure stolen gate (TS), which states that the arrival time of the police must be greater than the time for the thieves to steal the treasure and go away.

3 Asynchronous Multi-Agent Systems

Asynchronous Multi-Agent Systems (AMAS, [JPDM18]) are a modern semantic model for the study of agents’ strategies in asynchronous systems. They offer a (succinctly represented) analysis framework capable of efficient reachability checks even on non-trivial models [JPDM18]. By linking protocols to agents, AMAS are a natural compositional formalism for analysing multi-agent systems.

Technically, AMAS are similar to networks of automata that synchronize on shared actions, and interleave local transitions to execute asynchronously [FHMV95, LPQ10, JPDM18]. Works that give semantics to attack-trees via automata usually do not consider defence nodes [ÇY07, KSR*+*18]. The attack-defence diagrams of [HKKS16] use stochastic timed automata as a semantic base: this grants them ample expressive power, but also entails large state spaces and undecidable reachability in the general case, which AMAS circumvents.

Definition 1 (Asynchronous Multi-Agent Systems, [JPDM18])

An asynchronous multi-agent system (AMAS) consists of $n$ agents $A=\{1,\dots,n\}$, where each agent has an associated tuple $A_{i}=(L_{i},\iota_{i},Act_{i},P_{i},T_{i})$ including

(i) a set of local states $L_{i}=\{l_{i}^{1},l_{i}^{2},\dots,l_{i}^{n_{i}}\}$;

(ii) an initial state $\iota_{i}\in L_{i}$;

(iii) a set of actions $Act_{i}=\{a_{i}^{1},a_{i}^{2},\ldots,a_{i}^{m_{i}}\}$;

(iv) a local protocol $P_{i}\colon L_{i}\to 2^{Act_{i}}$ which selects the actions available at each local state; and

(v) a (partial) local transition function $T_{i}\subseteq L_{i}\times Act_{i}\times L_{i}$ s.t. $(l_{i},a,l^{\prime}_{i})\in T_{i}$ for some $l^{\prime}_{i}\in L_{i}$ iff $a\in P_{i}(l_{i})$.

Sets $Act_{i}$ need not be disjoint. $Act=\bigcup_{i\in A}Act_{i}$ and $Loc=\bigcup_{i\in A}L_{i}$ are the set of all actions and all local states, respectively. For each action $a\in Act$, the set $\mathit{Agent}(a)=\left\{i\in A\mid a\in Act_{i}\right\}$ contains all agents that can perform action $a$. The parallel composition of AMAS is given by Interleaved Interpreted Systems, which extend AMAS with variables and define global states and global transitions.

Definition 2 (Interleaved Interpreted System, [JPDM18])

Let $\mathit{PV}$ be a set of propositional variables. An interleaved interpreted system (IIS) is an AMAS extended with

(i) a set of global states $S\subseteq\prod_{i=1}^{n}L_{i}$;

(ii) an initial state $\iota\in S$;

(iii) a (partial) global transition function $T\colon S\times Act\to S$ s.t. $\forall i\in\mathit{Agent}(a)$, $T(s_{1},a)=s_{2}$ iff $T_{i}(s_{1}^{i},a)=s^{i}_{2}$, whereas $\forall i\in A\setminus\mathit{Agent}(a)$, $s_{1}^{i}=s^{i}_{2}$, where $s_{1}^{i}$ is the $i$-th local state of $s_{1}$; and

(iv) a valuation function $V\colon S\to 2^{\mathit{PV}}$.

4 Extending the AMAS model

As defined in [JPDM18], AMAS do not include attributes. Therefore, to model ADTs we now define Extended AMAS, associating attributes to local transitions.

Definition 3 (Extended Asynchronous Multi-Agent Systems)

An Extended Asynchronous Multi-Agent System (EAMAS) is an AMAS where each local transition function $t\in\mathit{LT}=\bigcup_{i\in A}T_{i}$ is equipped with a finite set of variables $\mathit{AT}_{t}=\{v^{1}_{t},\ldots,v^{k}_{t}\}$, called attributes, over a domain $D_{t}=d_{t}^{1}\times\cdots\times d_{t}^{k}$.

Let $\mathit{AT}=\bigcup_{t\in T}\mathit{AT}_{t}$ and $D=\prod_{t\in T}D_{t}$. Let $\mathit{Guards}$ be the set of formulas of the form $\beta\sim 0$, where $\beta$ is a linear expression over attributes of $\mathit{AT}$ and ${\sim}\!\in\!\{<,\leq,=,\geq,>\}$. Let $\mathit{FUN}$ be all functions taking arguments in $\mathit{AT}$, and $\mathit{EXP}(\mathit{AT},\mathit{FUN})$ be linear expressions over $\mathit{AT}$ and $\mathit{FUN}$. Each transition $t\in\mathit{LT}$ has associated

(i) a message $f_{M}(t)\in(\{!,?\}\times\{\mathit{ok,nok}\})\cup\{\bot\}$;

(ii) a guard $f_{G}(t)\in\mathit{Guards}$; and

(iii) a modification function $f_{t}\colon\mathit{AT}_{t}\to\mathit{EXP}(\mathit{AT},\mathit{FUN})$.

Item i indicates whether $t$ is not a synchronised transition ($\bot$), or whether it is sending (marked with $!$) or receiving ($?$) a message $\in\{\mathit{ok,nok}\}$. Guards in item ii constrain transitions. Item iii states how to modify the associated attributes when taking a transition. To model ADTs we must also extend IIS.

Definition 4 (Extended Interleaved Interpreted System)

Let $\mathit{PV}$ be a set of propositional variables, ${\bf v}\colon\mathit{AT}\to D$ a valuation of the attributes, and ${\bf v}_{0}$ an initial valuation. An extended interleaved interpreted system (EIIS) $M$, or a model, is an EAMAS extended with

(i) a set of global states $S\subseteq L_{1}\times\dots\times L_{n}\times D$;

(ii) an initial state $s_{0}=\langle(\iota_{1},\dots,\iota_{n}),{\bf v}_{0}\rangle\in S$;

(iii) a global transition relation $T\subseteq S\times Act\times S$ s.t. $\langle(l_{1},\ldots,l_{n},{\bf v}),a,(l^{\prime}_{1},\ldots,l^{\prime}_{n},{\bf v}^{\prime})\rangle\in T$ iff:

(a) \exists i,j\in Agent(a)$$\land$$\exists t_{i}=(l_{i},a,l^{\prime}_{i})\in T_{i}$$\land$$\exists t_{j}=(l_{j},a,l^{\prime}_{j})\in T_{j}$$\,s.t.~{}f_{M}(t_{i})=(!,m)\wedge f_{M}(t_{j})=(?,m);

(b) $\forall k\in A\setminus\{i,j\}~{}\,l_{k}=l^{\prime}_{k}$;

(c) ${\bf v}\models f_{G}(t_{i})\land f_{G}(t_{j})$;

(d) ${\bf v}^{\prime}={\bf v}[\mathit{AT}_{t_{i}}][\mathit{AT}_{t_{j}}]$;

and

(iv) a valuation function $V:S\rightarrow 2^{\mathit{PV}}$, 

where ${\bf v}[\mathit{AT}_{t_{i}}][\mathit{AT}_{t_{j}}]$ in item iiid indicates the substitution of attributes in the valuation ${\bf v}$ according to transitions $t_{i}$ and $t_{j}$, that is ${\bf v}^{\prime}={\bf v}\left[\bigwedge_{v_{t_{i}}\in\mathit{AT}_{t_{i}}}v_{t_{i}}:=f_{t_{i}}(v_{t_{i}})\right]\left[\bigwedge_{v_{t_{j}}\in\mathit{AT}_{t_{j}}}v_{t_{j}}:=f_{t_{j}}(v_{t_{j}})\right]$.

In the definition of the global transition relation $T$, item iiia specifies the synchronisation of transition $t_{i}$ (with a sending action) and $t_{j}$ (with a receiving action) that share the message $m$. Item iiib ensures that agents other than $i$ and $j$ do not change their states in such a synchronisation. Item iiic guarantees that the guards of $t_{i}$ and $t_{j}$ hold for the valuation ${\bf v}$. Finally, item iiid indicates how ${\bf v}^{\prime}$ is obtained by updating ${\bf v}$ with the attributes values modified by $t_{i}$ and $t_{j}$.

5 EAMAS transformation of ADTs

Each ADT node is modelled as an EAMAS agent via transformation patterns. These synchronise among themselves via shared actions. The approach is compositional, i.e. the resulting EIIS model of the ADT contains an agent per node in the tree, and correct, i.e. all relevant (ADT) paths are captured by the model. Note that unlike timed formalisms, e.g. (priced) time automata where clocks let time pass, time in EAMAS is an attribute. This allows e.g. to give minimum and maximum time values, and also makes EAMAS much easier to model check.

Transformation patterns.

Table 2 shows how each ADT construct is transformed into an agent (sub)model. Models communicate via the blue transitions. Transformations are symmetrical for attack and defence nodes: Table 2 shows attack patterns. A leaf signals action $a$ or fails. For DAG ADTs where gates can share children, self-loops in states $l_{1},l^{\prime}_{1}$ synchronise with all nodes that depend on the attack.

In conjunctions, (all) actions must be signaled in any order. Then, attack $A$ occurs, followed by the model signaling success. The conjunction fails if any action fails. Disjunctions and counter actions operate in the expected analogous way. Sequential constructs enforce the absence of parallelism, as per the semantics chosen for $\mathtt{{SAND}}$ and $\mathtt{{SNAND}}$ gates (see Sec. 2.1). Note that patterns use a single order of actions: other orders are shufflings of the semantically equivalent sequence shown in Table 2, and are thus already present in the state space.

Correctness of the transformation.

Communication between two patterns involves pairwise synchronisation, given by item iiia in Def. 4: the parent receives the status from each child, updates its own status, and then informs its own parent. Self-loops ensure that all parents are informed in DAG ADTs. The order of reception is not important as long as there is a representative sequence for the attack/defence semantics, which the patterns ensure. This covers expected action signals, i.e. those that a parent must receive from its children to achieve its goal. For sequences containing unexpected signals it could happen that a parent does not receive all information from its children, thus entering a deadlock before reaching its final state to signal success to its own parent(s). Notice that these sequences are precisely those that inhibit the goal of the (parent) gate. Therefore, not reaching the final state is indeed the desired behaviour.

Adding node attributes.

Transformation patterns in LABEL:\LongVersion{sec:transformation:patterns}\ShortVersion{tab:transform:short} concern only an ADT structure. To take attributes values into account, a child must transmit these to all parents during transition synchronisation. Attributes in a node are given by the intrinsic value and computation function of the node—see Sec. 2.2 and the EAMAS modification function in item iii of Def. 3. For example, the cost of an $\mathtt{{AND}}$ gate is typically its own cost plus those of all children. Attributes values are computed after all the node preconditions are satisfied. $\mathtt{{OR}}$ gates involve a choice among children: here, computation happens upon receiving the message from one child. Conditions associated to ADT countering nodes (e.g. TS in Fig. 2) are added as guards to the corresponding action transition. Computation functions may be sensitive to the distribution of agents over nodes for certain gates and attributes. For instance, time computation for $\mathtt{{AND}}$ gates is typically affected by the parallel operation of multiple agents with the same goal; but this is not true in general for cost, neither for time in $\mathtt{{SAND}}$ gates. We illustrate this with our running example222Computation functions for agents coalitions are further discussed in Appendix 0.A. ​​.

Example: EAMAS of the Treasure hunters.

Applying the transformation patterns to the Treasure hunters ADT of Fig. 2 gives the EAMAS in Fig. 3.

Green labels indicate cost and time of each operation. The computation for the $\mathtt{{OR}}$ gate ($\mathit{GA}$) depends on the child from which the message is received. The condition associated to $\mathit{TS}$ is depicted in orange. It checks whether the attack succeeds, but does not modify its cost nor its time. Time computation for the $\mathtt{{AND}}$ gate $\mathit{ST}$ uses function $\mathit{timeC}$, which returns the sum of its arguments if the children are handled by the same agent (there is one thief) and their maximum otherwise (two or more thieves collaborate). Note that sequential gates like $\mathtt{{SAND}}$ enforce the (sequentially) dependent execution of its children regardless of agents distributions. This models situations of logical dependencies based on the nature of the attack/defence instead of the resources available. In our example the thieves must complete stealing the treasure before going away, irrespective of the number of thieves. Hence the time for the thieves to flee is

{\color[rgb]{0,0.75,0.16}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.75,0.16}\pgfsys@color@cmyk@stroke{0.92}{0}{0.59}{0.25}\pgfsys@color@cmyk@fill{0.92}{0}{0.59}{0.25}\mathit{t_{TF}}}={\color[rgb]{0,0.75,0.16}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.75,0.16}\pgfsys@color@cmyk@stroke{0.92}{0}{0.59}{0.25}\pgfsys@color@cmyk@fill{0.92}{0}{0.59}{0.25}\mathit{t_{ST}}}+{\color[rgb]{0,0.75,0.16}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.75,0.16}\pgfsys@color@cmyk@stroke{0.92}{0}{0.59}{0.25}\pgfsys@color@cmyk@fill{0.92}{0}{0.59}{0.25}\mathit{t_{GA}}}.

6 Experiments

To demonstrate our approach we implement the transformation patterns in Uppaal and IMITATOR. With these popular and versatile software tools for quantitative verification, we analyse the following case studies from the literature.

6.1 Case studies

Forestalling a software release (forestall).

This example, shown in Fig. 4 and based on a real-world instance [BLP*+*06], models an attack to the intellectual property of a company $C$, by an unlawful competitor company $U$ aiming at being “first to the market.”

Software extraction from $C$ must take place before $U$ builds it into its own product. Also, $U$ must deploy to market before $C$, which can only take place after $U$ integrates the stolen software into its product.

Compromise IoT device (iot-dev).

This case study describes an attack to an Internet-of-Things (IoT) device either via wireless or wired LAN. Once the attacker gains access to the private network and has acquired the corresponding credentials, it can exploit a software vulnerability in the IoT device to run a malicious script.

[KSR*+*18] presents an attack tree for this example as an extension of the one in [SL15]. The ADT of Fig. 5 enriches that with defence nodes.

Obtain admin privileges (gain-admin).

To gain administrative privileges on a UNIX system, an attacker needs either physical access to an already logged-in console (entering the computer centre or corrupting an operator) or remote access via privilege escalation (attacking the SysAdmin). This well-known case study [Wei91, Edg07, JW08, KPS14, KRS15] exhibits a mostly branching structure: all gates but one are disjunctions in the original tree from [Wei91]. We enrich this scenario with the $\mathtt{{SAND}}$ from [KRS15], and add reactive defences. The full ADT is presented in Fig. 7 of Appendix 0.B.

6.2 Uppaal

All case studies from Sec. 6.1 were modelled in Uppaal [BDL04, DLL*+*15], a state-of-the-art tool for validation and verification of real-time systems. Automata templates are declared via its GUI and later instantiated for model verification via PCTL-like queries. This allows a straightforward encoding of the ADT-to-EAMAS translations as Uppaal templates. Modelling an ADT is achieved by instantiating these templates. Moreover, support for agents distribution can be easily encoded assigning agents to tree nodes in a dedicated array.

We compared the original Uppaal models from [KRS15, KSR*+*18] (extended with defences as detailed in Sec. 6.1) with our EAMAS translations. Our goal was twofold: on the one hand we verified correctness, checking that reachability queries (“can the attack succeed?”) and quantitative queries (“what is the time of the fastest possible attack?”, “what is the cost incurred?”) coincide between our models and those from [KRS15, KSR*+*18]; on the other hand (for the EAMAS translations) we studied the impact of agent coalitions on these metrics.

Uppaal modelling in [KRS15, KSR*+*18] uses clock variables to represent time, and clock constraints to encode the duration of attacks and defences. This is the natural approach in a tool designed for the verification of timed systems, yet it has two drawbacks when it comes to the analysis of ADTs:

• •

Uppaal uses abstractions and approximations for time regions that rule out decidability in the general case [BDL04]. Thus reachability queries like “can the attack be performed” can at best result in a “this may be true” answer.

In contrast, EAMAS transformations are untimed (see Secs. 2 and 4) and verification is exact. The price to pay is a larger state space and approximately $3\times$ longer computation times.

• •

Unless explicitly encoded case-per-case in the gates, time elapses simultaneously for all clocks. Thus, modelling the dependent execution of nodes requires e.g. using a $\mathtt{{SAND}}$ rather than an $\mathtt{{AND}}$. This contaminates the structure of the ADT with the distribution of the agents for analysis. EAMAS can keep the ADT structure unmodified while studying agents coalitions.

Case study forestall.

The minimum time for a successful attack is 43 days, via the $\mathtt{{NAND}}$ attack gate PRS. Both Uppaal models of the system (EAMAS and [KRS15]) produced the same correct result. The maximum time for a successful attack is 92 days: this implies a failed network attack (NA) due to the presence of the intrusion detection (id) defence, a failed physical robbery (PR) due to the company’s use of secure coding rooms (scr), and a successful bribery to a programmer (BRB). Notice that the time for NA, PR, and BR must be added if we consider the same person is performing all actions, i.e. there is only one attacker. This cannot be enforced in the Uppaal model from [KRS15] without sequential $\mathtt{{OR}}$ gates, in the absence of which the query for maximum time yields “55 days”. The EAMAS Uppaal model can produce the correct result (92 days) by specifying that a single agent is performing all attacks; and it also yields “55 days” if independent agents are used for the BRB, NA, and PR attacks. In the case of costs, the cheapest attack is performed via NAS (€ $\mathrm{4k}$) whereas the most expensive one (€ $\mathrm{10500}$) involves all attacks, with failures of NA and PR due to the id and scr defences. Both models yield the correct values to these queries.

Case study iot-dev.

In this case the same subtree is the source of the fastest and cheapest attack, via the access LAN strategy (AL) to connect to the private network (CPN). The minimum cost is € $\mathrm{270}$ and the maximum one is € $\mathrm{380}$, when AW is chosen in addition to AL. The EAMAS and the [KSR*+*18] Uppaal models yield correct results. For this ADT both the minimum and maximum time depend on the agent coalition. This is because the access private network subtree (APN) is an $\mathtt{{AND}}$ gate, which can be executed in parallel or not depending on how many attackers are involved. For this reason and given its use of clocks, the [KSR*+*18] model can only produce 694 minutes as the fastest attack, which is correct (and the EAMAS model also computes) when different agents perform the CPN and GVC attacks. When instead the same agent is used for both attacks, the EAMAS models returns the correct 784 minutes minimum time. The only way to achieve this in the [KSR*+*18] model is to modify the tree, replacing the $\mathtt{{AND}}$ for a $\mathtt{{SAND}}$ in APN. Furthermore, the longest attack takes 1204 minutes, which can be computed from the ADT of Fig. 5 by the EAMAS model but not by the [KSR*+*18] model without modifications to the tree structure.

Case study gain-admin.

The fastest attack takes 2942 minutes via breaking into the computer centre to access a connected CLI (ACLI through bcc), whereas the slowest takes 23070 minutes via looking over the SA’s shoulder (LSAS). For full parallelism of attacks, these values are computed correctly by both the [KRS15] and the EAMAS models. To study other agent coalitions, [KRS15] suffers from the same limitations as in the other two case studies. Regarding costs, there are two cheapest attacks (€ $\mathrm{100}$) via either GAPS or TSA. The most expensive attack (€ $\mathrm{15820}$) is the summation of the costs of all attack leaves. Again both values are correctly computed by the two models. The reachability query “is an attack feasible?”is computed for the EAMAS model in a few milliseconds, whereas it takes more than three minutes for the [KRS15] model. This is a consequence of the reduction techniques applied to timed-systems where reachability is nontrivial; in contrast, the full state space exploration in the EAMAS model can quickly reach the goal state starting from the csa or co leaves. As discussed earlier, state space bloating in the EAMAS model impacts quantitative queries.

6.3 Imitator

IMITATOR (www.imitator.fr, [AFKS12]) is a model-checker for Parametric Timed Automata [AHV93]. Models are composed of automata that synchronise on shared transitions (actions); in ADTs this involves message passing between a child and its parent(s), where all combinations must be explicit for DAGs.

We modelled our running example in IMITATOR as the EIIS of Fig. 3. Cost and time are constants for the nodes with fixed attributes—see the table in Fig. 2—and variables for the remaining nodes. We could verify that location $l_{\mathit{TS}}$ is reachable in the model, i.e. the attack is feasible for the selected attributes values. This holds even for a single attacker, since GA must be done after ST, and the police is alerted as soon as b and f succeed (but before ST does).

Moreover, we considered the question “To catch the thieves, what is the maximum time the police can take to arrive?” This requires synthesising a value for the time attribute of the p node, which becomes a model parameter. IMITATOR computed that the police can take at most 5 minutes to prevent the burglary.

For the three case studies of Sec. 6.1, the min/max costs and times were also found by state space exploration with IMITATOR, confirming the results obtained with Uppaal. Regarding parameter synthesis, we considered an attack is successful if its associated defence was slower:

($i$) for forestall, we computed that id should take at most 1 day to block NA—since NAS is a failed reactive defence, id is triggered as soon as heb succeeds, and has to finish faster than the intrinsic time of NA;

($ii$) for iot-dev, inc is effective iff it takes at most 3 minutes;

($iii$) finally, for gain-admin we proved that whatever the time for tla, an attack is feasible (as GSAP is a disjunction), and hence the other defences are required.

7 Conclusion and Future work

In this work we revisited attack-defence trees under a unified syntax, extending the usual constructs with a new sequential counter-operator. Our syntax framed this extension naturally among the other constructs, and in accordance to the chosen semantics and other related work.

More importantly, we extended AMAS to model ADTs in an agent-aware formalism—EAMAS—and provided transformation patterns from ADT constructs to agent models. Our ADT–EAMAS transformation preserves the compositional system description, ensuring a succinct state space where reachability queries can be efficiently checked.

EAMAS models decorate all ADT nodes with attributes and an operating agent. We exploited this flexibility to analyse (via Uppaal on three case studies) the impact of different agent coalitions on attack/defence performance metrics such as time and cost.

Finally, we analised the feasibility of specific goals using IMITATOR: we synthesised parameters (i.e. attribute values of ADT nodes) rendering an attack/defence feasible, or we proved them infeasible.

Overall, our experimental results show how different agent distributions affect the time of attacks/defence strategies, possibly rendering some infeasible. We expect this will open the gate to richer studies of real-world security scenarios, with multiple distinct agents.

Our next objectives include designing logics to express properties of EAMAS, and adapt the partial order reduction (POR) methodology presented in [JPDM18] to reason about the abilities of agents in EAMAS models. Moreover, we will extend this to handling parametric timing information. Finally, we plan to extend our tool that currently transforms ADTs into EAMAS models, to automatically generate IMITATOR and Uppaal models.

Appendix 0.A Computation functions for EAMAS agents

To model and study the impact of different strategies and agent coalitions on ADTs, computation functions for node attributes are a versatile solution. In our running example, the computation function for the time of the attack gate $\mathtt{{ST}}=\mathtt{{AND}}(\mathtt{b},\mathtt{f})$ can be generically expressed with functions $f$ and $g$:

[TABLE]

• $\blacktriangleright$

$f=+$ necessarily, because the operations involved in stealing the treasure depend logically on the completion of both children nodes, and

• $\blacktriangleright$

$g$ depends on the agent coalition: if two or more thieves cooperate then $g=\max$; but if there is a single attacker then $g=+$.

In the general case, the children of a gate will be subtrees $\mathtt{L}$ and $\mathtt{R}$ rather than leaves, which allows more complex computations of potential parallelism between the agents in $\mathtt{L}$ and $\mathtt{R}$. One could for instance encode a simple worst-case scenario: take an $\mathtt{{AND}}$ gate involving agents $\mathit{A}$, and let $\mathit{A_{\mathtt{L}}}\subseteq\mathit{A}$ (resp. $\mathit{A_{\mathtt{R}}}\subseteq\mathit{A}$) be all agents from subtree $\mathtt{L}$ (resp. $\mathtt{R}$). Then make the time of the gate be either

• $\blacktriangleright$

the sum of the times taken to complete $\mathtt{L}$ and $\mathtt{R}$ if $\mathit{A_{\mathtt{L}}}\cap\mathit{A_{\mathtt{R}}}\neq\varnothing$, because then some agents are present in both children of the $\mathtt{{AND}}$, or

• $\blacktriangleright$

the maximum between these times otherwise, because then $\mathtt{L}$ and $\mathtt{R}$ are fully independent.

Furthermore, the sharing of children nodes by different gates in DAG ADTs can also be captured in any desired way, by a careful choice of the computation functions for each attribute. Take for instance the tree

[TABLE]

where $\mathtt{a_{1},a_{2},a_{3}}$ are attack leaves and $\mathtt{{SAND}}_{1},\mathtt{{SAND}}_{2}$ are standard $\mathtt{{SAND}}$ gates. Due to the sequential operation of these gates, the computation function for the time attribute of $\mathtt{{SAND}}_{1}$ must be $\mathit{time}(\mathtt{{SAND}}_{1})=\mathit{init\_time}({\mathtt{{SAND}}_{1}})+\mathit{init\_time}({\mathtt{a_{1}}})+\mathit{init\_time}({\mathtt{a_{2}}})$, and analogously for $\mathtt{{SAND}}_{2}$. However, the time of the full $\mathtt{{AND}}$ attack is

[TABLE]

In particular, even for a single agent, $\mathit{init\_time}({\mathtt{a_{2}}})$ must be counted only once: when $\mathtt{{SAND}}_{1}$ finishes, it means that $\mathtt{a_{2}}$ has already been completed for $\mathtt{{SAND}}_{2}$ too.

To encode this compositionally via computation functions, one must operate at the level of the parent(s) that close the DAG loop, e.g. the $\mathtt{{AND}}$ in equation 1. This is because only at those nodes the sharing of children

$(i)$ can be realised, and

$(ii)$ it may have an impact in computations

: $\mathit{time}(\mathtt{{SAND}}_{1})$ considered individually is not influenced by operations in $\mathtt{{SAND}}_{2}$.

Let us finally analyse time computations for a coalition of two agents, i.e. two attackers cooperate. In this case, $\mathtt{{SAND}}_{1}$ and $\mathtt{{SAND}}_{2}$ can neither operate in parallel, because $\mathtt{a_{2}}$ is the same attack for both gates. The root cause of this restriction is that the tree in equation 1 is isomorphic to $\mathtt{{SAND}}(\mathtt{a_{1},a_{2},a_{3}})$, so equation 2 is the only correct way to compute $\mathit{time}(\mathtt{{AND}})$, regardless of agent coalitions. Again, computation functions can encode this by operating at the level of the $\mathtt{{AND}}$ gate, where the shared children in the DAG re-join.

Appendix 0.B Case study: gain-admin