Ranking risks and countermeasures is one of the foremost goals of
quantitative security analysis. One of the popular frameworks, used also in industrial practice, for this task are attack-defense trees.
Standard quantitative analyses
available for attack-defense trees can distinguish likely from
unlikely vulnerabilities.
We provide a tool that allows for easy synthesis and analysis of those models, also featuring probabilities, costs and time. Furthermore, it provides a variety of interfaces to existing model checkers and analysis tools.

Unfortunately, currently available tools rely on precise
quantitative inputs (probabilities, timing, or costs of attacks),
which are rarely available.
Instead, only statistical, imprecise information is typically available, leaving us with probably approximately correct ()
estimates of the real quantities.
As a part of our tool, we extend the standard analysis techniques so they can handle the PAC input and yield rigorous bounds on the imprecision and uncertainty of the final result of the  analysis.

§ INTRODUCTION

Attack trees, e.g.,  <cit.>, and their extensions are a widespread formalism for threat modeling and risk assessment. Their applications range from analyzing attacks on smart grids <cit.>, ATMs <cit.>, optical power meters <cit.>, SCADA control systems <cit.> or software supply chains <cit.> to intelligent autonomous vehicles and vehicular networks <cit.>, secure deployment of HTTPS <cit.> or cybersecurity awareness trainings for election officials <cit.>. Moreover, attack trees are particularly useful for meta-modeling threats, combining several risk analyses together, e.g., in telemedicine <cit.>, impersonation attacks in e-learning <cit.> or IoT systems <cit.>.  Besides these individual usages, attack trees are generally recommended as a means to identify the point of the weakest resistance according to the OWASP CISO AppSec Guide,[<https://www.owasp.org/index.php/CISO_AppSec_Guide:_Criteria_for_Managing_Application_Security_Risks>] or to retrospectively understand attacks (through so-called red teams) by NATO's Improving Common Security Risk Analysis report <cit.>.

In practice, there are not enough resources to fix every single vulnerability found in security assessment. Hence, the need to rank their importance arises. Quantitative analysis of attack trees can utilize quantitative information such as probabilities, costs, and timing to compute how likely particular vulnerabilities are, how much the defense may cost, or how long attacks might take.  Consequently, it can distinguish unrealistically costly or improbable attacks from those that need to be fixed.  While there is a recent body of theoretical work in this direction, e.g. <cit.>, there are two main hindrances to practical use.  Firstly, it is the very limited tool support for convenient quantitative modeling and analysis. Secondly, it is the uncertainty and imprecision of the quantitative input information, arising in this domain even more than elsewhere. Indeed, apart from standard questions like What is the actual failure rate of the security camera?, we may need to ask What is the probability of guessing a password using a database of the most common passwords and one year of CPU time? or How much faster and cheaper is a particular attack going to be next year based on past years' data?

We address both issues: we provide a convenient tool, which also features quantitative analysis capable of rigorously reflecting the uncertainty and imprecision of the quantitative inputs.  To this end, we formalize such models as -quantitative trees. Then, we show how to obtain them practically using our tool and provide an algorithm for their analysis.
In order to properly evaluate our tool and the -input quantitative analysis we create a benchmark suite  of $\ADT$ found in literature and ones generated randomly.
We make all models available to the public.[For review, all models are in our artifact at <https://zenodo.org/records/11090469>.]

Tool.  We provide , a tool for the whole modeling-analysis workflow. The tool can import trees in the  format and  format of  <cit.>. The graphical interface allows for convenient creating, editing, and combining trees and generating -quantities directly from provided data. Further, the tool translates the trees to formats of model checkers  <cit.>,  <cit.>,  <cit.>,  <cit.>, and  <cit.> (via  <cit.> export of ). Consequently, the GUI effectively interfaces with other available analyses (such as <cit.>) and to our new -input analysis. Besides, to help non-experts successfully construct meaningful models, we provide detailed automatically generated feedback on compliance with the assumptions of each of the offered analyses.

-quantitative attack-defense trees.  All the previously cited quantitative analyses assume that the quantities (transition probabilities, costs, delays) are given as exact numbers, allowing analyses to output exact numbers, too.  However, in reality, we often lack perfect quantities.

Nonetheless, this data allows us to derive estimates of the actual value, possibly together with confidence intervals bounding these estimates' uncertainty. Hence, we assume the input quantities are probably approximately correct (), i.e., with a given probability in a given interval around the estimate. We demonstrate how easily such trees can be obtained, relying on statistics or time-series analysis. To that end, we consider independent samples of the unknown quantity data (e. g., past years' information). We then extend the traditional bottom-up analyses to bound the final  uncertainty resulting from the input quantities'  uncertainty. Interestingly, our extended analysis comes with little additional computational cost in comparison to the standard analysis on average-size attack-defense trees.  Consequently,  our approach allows practitioners to stick to their current analysis and learn about the quality and reliability of its results with almost no additional effort.

To summarize, our contribution is threefold:

* Our tool  addresses practical needs in attack-defense tree modeling and analysis, including a GUI and a CLI for editing and analyzing . It also gives feedback on suitable exports for further analyses.

* The tool features a novel quantitative analysis of -attack-defense trees, the first extensions of attack-defense trees reflecting the data inaccuracy.

* The tool comes equipped with AT BEnchmark SuiTe (), collecting benchmarks from literature as well as randomly generated ones.

Organization. The paper is organized as follows. After exemplifying the framework of attack-defense trees in sec:attack-defense-trees, the tool functionality is presented in
sec:functionality. We describe our -input analysis in sec:pac.
sec:experiments evaluates our contributions experimentally and sec:conclusion concludes. We provide an artifact with the tool and modelsfn:artifact.

Related work.
Besides two industrial tools dedicated to attack-defense tree analysis[see <http://www.amenaza.com> and <http://www.isograph.com/software/>], which neither support more complex attack-defense tree structures such as <cit.>, nor export to standard model checking tools, there are three dedicated (and up-to-date) quantitative attack-defense tree analysis tools:

*  <cit.> supports attack-defense trees with the operators $\opAnd$, $\opOr$ and Sequential-$opAnd$ $\opSand$ and attack-defense trees with operators $\opAnd$ and $\opOr$. It uses the standard bottom-up traversal for quantitative model checking. In contrast to our tool,  does not support -input analysis.   Additionally, one cannot add -input analysis to  as a `custom' domain since multi-parameter attack-defense trees are not supported. We compare the performance of the bottom-up analysis using  and  in sec:experiments.

*  <cit.> is a software bridging tool, which provides various horizontal and vertical model transformations to the  2.0 input format or to the model checker UPPAAL, however not to  or .  models and  analysis are not supported.

* [https://github.com/RisQFLan/RisQFLan/wiki] allows specifying attack-defense trees with quantitative constraints using a dedicated probabilistic language (XTEXT grammar)[While the XTEXT files get compiled to dot-files for graphical display, these are currently not entirely compatible with the  import.]. Statistical model checking and precise analysis using  and  are supported. However,  neither supports -inputs nor continuous-time. Additionally, exports to  and  rely on discrete-time Markov chains rather than games or stochastic timed automata. Stochastic model checking in  relies on .[<https://github.com/andrea-vandin/MultiVeStA/wiki>]  Hence  does not allow synthesizing optimal attack and defense strategies. However,  allows assigning detection-rates to inner nodes and to separate defenses from countermeasures (which we do not feature). Hence, a complete performance comparision between  and  is not possible.

All these quantitative analyses have precise inputs and outputs (rather than  values). The resulting uncertainty is not bound, i.e., there is no estimate of how likely the analysis results are close to the actual results. In contrast our  analysis takes uncertainty of each input value into account. Hence, our resulting confidence interval covers likely deviations and bounds the uncertainty, which previous quantitative analysis cannot.

Surprisingly, the uncertainty of the input quantities in attack-defense trees has not gained too much attention yet <cit.>.

Buldas et al. <cit.> present the first approach to account for inconsistency and gaps in historical data and experts' estimates in attack-defense trees. The main limitation of their approach is the impossibility of reflecting the data accuracy, which is the main contribution of this paper.

In <cit.> a new approach to extend quantitative analysis on Attack Trees is presented, that may lift the structural bounds our tool currently has, but does cover a smaller set of operators compared to our approach. Additionally, there is no support for defense operations, yet.

§ ATTACK-DEFENSE TREES

In this section, we briefly recall the notion of attack-defense trees (), e.g., <cit.>. Attack-defense trees are labeled trees, where the root represents the overall goal to attack a system. This goal can be recursively refined into smaller sub-goals, giving rise to descendant nodes, until no further refinement is possible. Inner nodes receive operators as labels binding the roles of the children. The leaves represent basic events (denoted $\basicEvents$), unique observable happenings in
the real world. They are partitioned into basic attack steps and basic defense steps.

An attack-defense tree[In literature,  are often directed acyclic graphs (DAG), yet called trees. Hence, we call our framework attack-defense trees, although the underlying structure is a graph.] (over a set of basic events $\basicEvents$) is a tuple $\exampleADD$ where

* $\left (\vertices, \edges \right)$ is a directed acyclic graph, with a designated goal sink vertex $\topGoal$ for the attacker. The source vertices $\basicEvents \subseteq \vertices$ are called basic events. All other vertices, , are called gates; direct predecessors w.r.t. $(\vertices,\edges)$ of each gate are called its inputs.

* We additionally require that gates labeled with $\opAnd$, $\opOr$ and their sequential versions $\opSand$ or $\opSor$  have at least two inputs and that other gates have exactly one input.

* $\typeFunction{} \colon\ \gates \to \operators$ is the type function assigning an operator to each gate.

* $\triggerTransitions \subseteq \set{\vertex \in \gates \mid \typeFunction(\vertex) = \opTrigger} \times \basicEvents$ are trigger edges from $\opTrigger$ gates to BE;

* $\resetTransitions \subseteq \set{\vertex \in \gates \mid \typeFunction(\vertex) = \opReset}\times \basicEvents$ are reset edges from $\opReset$ gates to BE;

The $\ADT{}$ from <cit.> represents ways to gain access to a power meter. We will use this model also in sec:pacanalysis. In sec:experiments we evaluate our tool on more complex attack-defense trees.

In fig:toyexample, we present a small attack-defense tree representing an attacker (nodes in red) who wants to maliciously gain access to a digital power meter. The goal node at the top (with a blue border) represents the overall attack goal. All leaves of the tree are basic attack steps (colored red or green).
The goal is refined into different subtrees using the operator $\opAnd$, i.e., all of the subtrees need to be successfully attempted for the overall attack to be successful. The overall attack is successful if, the attacker gained the credentials (event (4)) and successfully entered them (event (9)). Also for the attack to be successful the defender (node in green) must not (event (17) with operator $\opNeg$) have installed additional authentication (event (6)).
Event (4) is refined with the operator $\opOr$ meaning it is successfully attempted if one of its children (event (1), (2), (3)) is attempted successfully.

To model complex attack-defense scenarios, a rich set of operators
\[\operators = \set{\opAnd,\opOr,\opNeg, \opSand,\opSor,\opTrigger,\opReset}\]
is necessary: Intuitively, $\opAnd,\opOr, \opNeg$ behave like their logical counterparts. $\opSand$ and $\opSor$ pose temporal (but not causal) restrictions on the order in which its children are attempted.

Further, for Trigger $\opTrigger$,  suppose its child is successfully attempted. In that case, several basic events are activated (triggered) for attempting (they cannot be attempted earlier than this).

Finally, Reset $\opReset$ is successfully attempted if its input is attempted successfully. As a side effect, events that have been reset can be attempted again, i.e., we allow players to attempt events several times.

A formal semantics of the operators used in the theoretical development in the subsequent section can be found in def:powerset in the Appendix. Formal semantics for the remaining operators are not necessary to follow the paper (They can be found in <cit.>).

§ TOOL OVERVIEW

This section shows the usage of $\quadtool{}$ both in a graphical user interface and direct command-line access. We evaluate our analyses in sec:experiments.

[auto,node distance=8mm,>=latex,font=]

[cost] (s3) construct or two import model;

[cost,right=7mm of s3] (s4) use default values or
two add values from various sources;

[cost,right=5mm of s4] (s5) export to
model checker two for further analyses;

[cost,above=8mm of s4] (s6) exact or -analysis
two in tool for costs, delays, probabilities;

[above left=3mm and 5mm of s3] (s0) ;
[above left=-4mm and 5mm of s3] (s1) ;
[below left=-4mm and 5mm of s3] (s2) GUI;
[below left=3mm and 5mm of s3] (s21) ;

[below left=6mm and -10mm of s4] (s11) iid samples;
[below=6mm of s4] (s12) time series;
[below right=6mm and -10mm of s4] (s13) expert estimates;

[above right=0mm and 5mm of s5] (s8) ;
[right=5mm of s5] (s9) ;
[below right=0mm and 5mm of s5] (s10) ;

[->] (s5) to node[midway,above,sloped] (s8);
[->] (s5) to node[midway,above,sloped] (s9);
[->] (s5) to node[midway,below,sloped] (s10);

[->] (s0) to node[midway,above,sloped] (s3);
[->] (s1) to node[midway,above,sloped] (s3);
[->] (s2) to node[midway,below,sloped] (s3);
[->] (s21) to node[midway,below,sloped] (s3);

[->] (s3) to node[midway,above,sloped] (s4);
[->] (s4) to node[midway,above,sloped] (s5);
[->] (s4) to node[midway,above,sloped] (s6);
[->,dashed] (s6) to node[above left]refine (s3);

[->] (s11) to node[midway,above,sloped] (s4);
[->] (s12) to node[midway,above,sloped] (s4);
[->] (s13) to node[midway,above,sloped] (s4);

The Workflow with  allows for input from four sources. In the next step the nodes can be refined using quantitative date from different sources. Additionally, the tool allows for analysis of said data. In a last step the data can be exported to model-checkers for further analysis.

§.§ Model Construction

The workflow using $\quadtool{}$ (see fig:quadtool) starts with
model construction. For convenient modeling, $\quadtool{}$ supports a
dedicated graphical user interface and the following two input

* The -format as described in the Graphviz-Tool <cit.>. We recommend this format as it supports storing all additional parameters like -parameters and simple formatting.

* The -format used in  <cit.>. To ensure compatibility with this tool, our tool only exports strict tree structured $\ADT$ without -values to this format.

Our GUI, see fig:editor, offers drag-and-drop manipulation of trees, creating new ones from scratch or by import. One can also easily combine existing models by importing several trees and connecting them.

There exist various approaches to attack-defense tree analysis supporting different features (see <cit.> for a survey on quantitative attack-defense tree analysis). Hence, $\quadtool{}$ comes with an integrated feedback system (see fig:editor) to support the user in finding potential errors or incompatibilities before exporting. Furthermore, it gives advice on which export formats may be beneficial for the particular model.

§.§  Benchmark Collection for Attack-Defense Trees

To support the standardization and benchmark collection among attack-defense tree researchers and practitioners, we bring forth an attack-tree benchmark collection AT BEnchmark SuiTe () accessible at . By uploading a model and registering with a name and email address, users receive a token to access all uploaded models in the database. In more details, our benchmark set consists of 42 models from 24 previously published papers, <cit.>, which we constructed using . Additionally, we generated 626 models of various sizes for performance testing. These are binary  using the gates $\opAnd$ and $\opOr$, created by combining two smaller models with a new root recurrently.

§.§ Obtaining -Quantities for Attack-Defense Trees

After creating a model, we add default values or estimates to basic events (second step in the workflow (see fig:quadtool)). Our  (s. sec:pac) assumption is less restrictive than the standard assumption of exact quantities and already applicable to various examples.

To derive -parameters, the simplest way is to calculate a Gaussian estimate with confidence intervals. The Gaussian estimate is best for independent identically distributed (i.i.d.)  samples. Our tool allows the generation of those values via csv-input. One can also directly use a AutoRegressive-Moving Average (ARIMA) model <cit.> inside the tool to derive bounds for cases with time-series data.

Please note that we do not aim to create the best possible time-series model for a given data-set using our tool since this still requires a more detailed analysis. However, we want to allow users to get a reasonably good prediction quickly.

§.§ Analyses

allows to analyze models using an exact or  analysis or using existing model checkers.

Like the , $\quadtool$ supports direct analyses on the tree for exact minimal attack costs, exact minimal attack delays, and exact success probabilities. Additionally, we support our new -input analyses for each of these domains.

Furthermore, users can export the final model to various other tools and model checkers using one of the following file formats: , , -, -, -input-language. For , we use the semantics in terms of stochastic turn-based games given in <cit.> and for
and  the semantics in terms of stochastic timed automata given in <cit.>. [To use , we suggest using the export to  first and then, use their export to the -format.]  In the following, we describe the interfaces to other tools and their use in more detail.

Connection to  and  These two attack-defense tree tools have a restricted set of features and expect  inputs. Thus, we cannot analyze every attack-defense tree constructed in  using these tools. For instance, whenever a model has multiple root nodes, our export omits all but one tree. Furthermore, the  only supports the operators $\opOr$, $\opAnd$, $\opSand$ and no timed events (with clocks or distributions).

Timed Analysis Analysis involving time can be either done within $\quadtool{}$ or outsourced to  or .

The translation to  uses actions for each three-valued logic state, i.e., each basic event can either be undecided, successfully or unsuccessfully attempted. For  a similar approach with automata for every state is used. Both approaches can model systems with multiple root nodes and complex operators.

Game Analysis Lastly, $\quadtool{}$ can also export to the  format, not supporting time, but supporting games.  In this framework, all basic events have the same chance to be executed at a given (discrete) point in time, impacting the evaluation of sequential operators.

Integration We provide the functionality to send a model directly to  cora, ,  and  simulator in the GUI, after specifying the Tool location, as seen in fig:editor (right lower panel).

$\quadtool$ with the case study from <cit.>. At the bottom, one can see the feedback for the selected export or general issues. On the right, the quantitative results for the selected domain (here probabilities) are given for all nodes with the -quantities. Below is the result of a model checker (here ).

§ -QUANTITATIVE : FIGHTING THE UNCERTAINTY

In this section we describe the technique underlying our tools' functionality to analyze $\adt$ with not fully known quantities. While it is less standard to do so in a tool paper, this is not described elsewhere and thus must be included in the tools' contributions for completeness here.

A standard way to reason about costs, probabilities, and time within attack-defense trees is to equip basic events with quantitative information and use bottom-up traversal algorithms to derive the root's final value <cit.>. In this section, we augment this analysis to bound the uncertainty resulting from estimating the quantitative values of the basic events.

In app:correctness, we show that our computations of
probabilities, costs and delays are correct with reference to standard Boolean
and powerset valuations of attack-defense
trees <cit.>. However, standard
bottom-up traversal algorithms are efficient and correct only on
simpler structures than our  in def:add (for more
details, see <cit.>). In particular, they require a
static interpretation, i.e., there is only one shot to decide
which basic events players try and which they do not
try. Consequently, we restrict ourselves to one of two domains supported by the
(attack-defense trees with gates $\opAnd$, $\opOr$ and
$\opNeg$). For reader's convenience, we exclude $\opTrigger$ in this
section but include it in app:correctness. Hence, our analysis also covers
the second domain of the .

§.§ Quantitative  and -Quantitative

Quantitative . Given a type $\type$ of the quantitative information, the quantitative  is an  equipped with a quantitative valuation of basic events $\valuesBE: \basicEvents \to \type$.  The definition is generic to carry over to various settings: While real numbers may represent cost <cit.>, acylic phase-type distributions may, for instance, represent the likelihood of a successful attack over time <cit.>.

For success probabilities, we simply take $\type=[0,1]$. For costs and delays, we take $\type=\RR_{\geq 0}$.

-Quantities. In most real-world examples, the quantitative information attached to basic events is rarely known precisely but comes with uncertainty. We call quantitative information probably approximately correct (), if there is an imprecision bound $\error$ and an uncertainty probability $\prob$, such that the distance between the true value and the given estimate is less than $\error$ with probability at least $1-\prob$. Formally:

Let $\type$ be a set equipped with a metric $\metric$. We say that a $\type$-valued random variable $X$ is $(\error,\prob)$- for the true value $\val$ if the probability[The method used to learn the estimate $X$ from data sampled from a distribution parametrized by $\val$ usually determines the probability space. For instance, for a $\val$-biased coin with $\val=0.49$ and 20 samples (coin tosses),
the standard statistics methods yield a probability space with highest density of $X$ in $0.49$ and inducing the respective confidence intervals for $X$ depending on the outcome of the experiment.] of $X \in \set{t \mid \metric(t,\val)\le \error}$ is (at least) $1-\prob$. Exact values can be considered $(0,0)$-.

For probabilities, costs, and delays, the metric is the standard Euclidean distance (absolute value of their difference).

-Quantitative  Given a type $\type$ of the quantitative information, the -quantitative  is a quantitative  equipped additionally with -parameters $\error[\basicEvent] \in \RR_{\geq 0}$ and $\prob[\basicEvent] \in [0,1]$ for each basic event $\basicEvent\in\basicEvents$.

§.§ -Input Extension of Bottom-Up Analyses

Before giving the generic algorithm for the bottom-up propagation of quantitative values <cit.>, we will give a short introduction to bottom-up analyses.

Bottom-Up Traversal Analysis Let $\ADT$ be an attack-defense tree with set $\vertices$ of nodes, $\topGoal$ its root, $\type$ a non-empty domain of quantitative information, $\interpretation$ an interpretation i.e. a mapping of -operators to operations over $\type$, and $\valuesBE$ a basic-events valuation with input values from $\type$. Then its bottom-up traversal semantics $\values \colon \vertices \to \type$ for $\ADT$ is defined recursively. The valuation of $\ADT{}$ is defined as the value of its root node $\values(\topGoal)$.

[Probabilistic ]  We have already seen that the domain for probabilities is $[0,1]$.  Here we instantiate the interpretation for probabilities. We define a probabilistic interpretation $\interpretation$ (with $\type=[0,1]$) as follows: (Similar examples for the domain of Cost and Probability can be found in app:examplesBottomUp)

* $\displaystyle{\interpretation(\vertex) (x_1,x_2)= x_1 \cdot x_2}$, if

* $\displaystyle{\interpretation(\vertex)(x_1,x_2)= x_1 + x_2 - x_1 \cdot x_2}$ for $\typeFunction(\vertex)=\opOr$

* $\displaystyle{\interpretation(\opNeg)(x)=1-x}$

Extension to PAC-Values In the following, we devise an algorithmic approach that allows us to derive a -aware variant from almost any bottom-up traversal analysis (according to its previous definition)[In fact, the  approach is independent of the concrete interpretation $\interpretation$ chosen, as long as for $\RR_{\geq0}$-interpretation it involves solely the operations $+$, $-$, $\max$, $\min$ and $\cdot$, or any combination thereof.] as long as it holds $\type \subseteq \RR_{\geq 0}$ for the domain $\type$. To this end, we use the notation $x_i \pm \error[i] \coloneqq [\max(0,x_i-\error[i]),x_i+\error[i]]$[For success probabilities, we set $x_i \pm \error[i] \coloneqq

We propagate the uncertainty along with the nodes during the bottom-up traversal analysis resembling interval arithmetics from canonical error analysis. Whenever the interpretation uses one of the operators $+$, $-$, $\cdot$, $\max$, $\min$ over $\RR_{\geq 0}$, for its -aware variant, we additionally compute a new uncertainty bound and uncertainty probability for the resulting value. The nodes' uncertainty bound and uncertainty probability are solely based on its operands' uncertainty bounds and uncertainty probabilities.

-Bounds Propagation Without any assumptions on the distribution of the uncertainty, operations are as follows:
Given values $x_1, x_2 \in [0,1]$ that are $(\error[i],\prob[i])$-, the uncertainty of

* $1-x_i$ can be bound by $\error = \error[i]$.

* $x_1 \cdot x_2$ can be bound by $\error = x_1\cdot \error[2] + x_2 \cdot \error[1] + \error[1]\cdot\error[2]$.

* $x_1 + x_2 - x_1 \cdot x_2$ can be bound by  $\error = \error[1] + \error[2] + x_1\cdot \error[2] + x_2 \cdot
\error[1] + \error[1]\cdot\error[2]$

* $\max(x_1,x_2)$ can be bound by $\error=\max(\error[1],\error[2])$

* $\min(x_1,x_2)$ can be bound by $\error=\max(\error[1],\error[2])$

For all operations the uncertainty probability $\delta$ is (at most) $1 - (1-\prob[1]) \cdot (1-\prob[2]) $, if all $x_i$ are independent, and otherwise (at most) $\prob[1] + \prob[2]$. As probability analysis relies on independence of the basic events, we will use the first bound in the following.

In summary, the result of each of the given operations is $(\error,\prob)$-. Furthermore, each constant $c \in \RR$ is (0,0)-.

[PAC-Bounds Computation for Probabilities]
Let $\ADT$ be an attack-defense tree with set $\vertices$ of nodes, let $\values[\basicEvents]$ be a  probability valuation for basic events, i.e., for every basic event $\basicEvent \in \basicEvents$, it holds $\values[\basicEvents](\basicEvent)$ is $(\error[\basicEvent],\prob[\basicEvent])$- for some $\error[\basicEvent] \in \RR_{\geq 0}$ and $\prob[\basicEvent] \in [0,1]$. The  uncertainty for $\vertex \in \vertices$ is computed as follows:

* $\vertex \in \basicEvents$ and $\vertex$ is not triggerable: return $(\error[\basicEvent],\prob[\basicEvent])$.

* $\typeFunction(\vertex)=\opAnd$ and $\inp[1],\inp[2]$ are its inputs: recursively compute $(\error[\inp[1]],\prob[\inp[1]])$ and $(\error[\inp[2]],\prob[\inp[2]])$. Use rule for multiplication R2, i.e., return  $\error= \values(\inp[1]) \cdot \error[\inp[2]] + \values(\inp[2]) \cdot \error[\inp[1]] + \error[\inp[1]]\cdot\error[\inp[2]]$ and $\prob = 1 - (1-\prob[\inp[1]]) \cdot (1-\prob[\inp[2]]) $

* $\typeFunction(\vertex)=\opOr$ and $\inp[1],\inp[2]$ are its inputs: recursively compute $(\error[\inp[1]],\prob[\inp[1]])$ and $(\error[\inp[2]],\prob[\inp[2]])$. Use rule R3, i.e., return
$\error= \error[\inp[1]]+ \error[\inp[2]] + \values(\inp[1]) \cdot \error[\inp[2]] + \values(\inp[2]) \cdot \error[\inp[1]] + \error[\inp[1]]\cdot\error[\inp[2]]$ and $\prob = 1 - (1-\prob[\inp[1]]) \cdot (1-\prob[\inp[2]]) $

* $\typeFunction(\vertex)=\opNeg$ and $\inp$ is its input: recursively compute $(\error[\inp],\prob[\inp])$. Use rule R1, i.e., return $\error= \error[\inp]$ and $\prob = \prob[\inp]$

Formally, we can state that the resulting interval is the tightest reflecting the input intervals: Let $\interpretation(\vertex) \in x_{\vertex} \pm \epsilon_{\vertex}$ for each $\vertex \in \basicEvents$ and $\gate \in \gates$ then $\interpretation(\gate)$ lies in the interval computed above. Vice versa, for every $\interpretation(\gate)$ in the interval, there are $\interpretation(\vertex) \in x_{\vertex} \pm \epsilon_{\vertex}$ (consistent with $\interpretation(\gate)$). Furthermore, with $\delta_{\vertex}$ denoting the probability that $\interpretation(\vertex) \notin x_{\vertex} \pm \epsilon_{\vertex}$, the probability, that the resulting value is outside of the computed  interval, is at most the computed $\delta$.

In , we also provide -aware bottom-up analyses for delays and costs. The proof of correctness can be found in app:pac.

[Propagation of Uncertainty]
In practice, $\delta = 0.05$ or $\delta=0.01$ seem reasonably small uncertainty probabilities for meaningful  data (since they are most commonly used significance criteria). As most examples from literature have less than 30 nodes (s. sec:experiments), a corresponding binary tree would have a depth of 5.  This would lead to $\delta \approx 0.56$ or  $\delta \approx 0.15$ for an inital $\delta$ of $0.05$ or $0.01$ at the root node respectively. Thus, selecting data of high confidence i.e. low $\delta$ is crucial for good overall estimates.

* ID 10 $p: 0.4594491$

* ID 19 $p: 0.9188982$

* ID 4 $p: 0.92818$

* ID 1 $p: 0.24$

* ID 2 $p: 0.65$

* ID 3 $p: 0.73$

* ID 9 $p: 0.99$

* ID 17 $p: 0.5$

* ID 6 $p: 0.5$

* ID 10 $p: 0.456463\;\epsilon: 0.130461\;\delta: 0.226219$

* ID 19 $p: 0.924015\;\epsilon: 0.193929\;\delta: 0.185494$

* ID 4 $p: 0.930528\;\epsilon: 0.1894165\;\delta: 0.142625$

* ID 1 $p: 0.233\;\epsilon: 0.026214\;\delta: 0.05$

* ID 2 $p: 0.667\;\epsilon: 0.029225\;\delta: 0.05$

* ID 3 $p: 0.728\;\epsilon: 0.027594\;\delta: 0.05$

* ID 9 $p: 0.993\;\epsilon: 0.005170\;\delta: 0.05$

* ID 17 $p: 0.494\;\epsilon: 0.031003\;\delta: 0.05$

* ID 6 $p: 0.506\;\epsilon: 0.031003\;\delta: 0.05$

Example evaluation of the model in fig:toyexample (a) without  values and (b) with -values. The -values were generated by sampling from Bernoulli distributions parameterized by the exact value.

§.§ Analysis Example

We use one of the models introduced by Fila and Widel in <cit.>(s. fig:toyexample) about manipulating a power meter as example for the analysis workflow with  values.
We will use the domain of probability and assign each of the basic events a success probability from the paper (see fig:examplevaluation (a)). For the defender node with id 6 we set the probability to 50% to represent, that only half of the power meters have this function enabled.

Using the exact properties the probability for a successful attack is about 46% (see fig:examplevaluation (a)). To generate the  values we use R 4.3.1 to sample a Bernoulli distribution, with the exact values as parameter, 1000 times. From these values we use the built-in calculation of our tool to retrieve the  values using a Gaussian-Estimator.

The propagated values are displayed in fig:examplevaluation (b). The calculations in the tool are done with arbitrary precision. The intermediate values are only rounded for display. Due to the initial confidence level of 5% the confidence level of the overall analysis is about 77%. Taking the $\epsilon$ in account the analysis returns an estimate of the true probability with confidence interval of about 45.65% [33.61%-57.69%]. So the true value calculated in the exact example lies inside the bound generated by our -propagation.

This extended analysis does, however, come with an increased computational effort, which still is inside acceptable bounds (see sec:experiments).

§ EXPERIMENTS

We discuss the performance of $\quadtool$ on our collection of benchmarks found on .

For performance measurements, we used 42 security models, ranging from 5 to 30 nodes, from existing literature (s. sec:atbest), allowing the whole operator set. 17 of them contained operators, that were incompatible with . Therefore, they were only used for the remaining formats. We executed the conversion 50 times each on a computer with Intel®Core™i7 processor and 16 GB RAM.

95%-confidence intervals of time (logarithmic scale) necessary for the corresponding model checker to evaluate models (for the success probability) depicted by the ADT size.
Most executions take less than 10 seconds. Y-position of line start corresponds with position in legend. As most models from  contain mostly player nodes, our timed analysis using  returns stack overflow errors on models of $size \geq 5$.  runtime seems to be more dependent on model composition, rather than just the size. The evaluation time for ,  and  Cora are all below 1 second.

Model checking times (mean per size)  (red triangles) vs. non- (blue dots) models in . The highest execution time was 1.2s for 1355 nodes.

In the next step, we conducted experiments on how long the model checkers , ,  and  need to analyze the  success and failure probability on the models previously used for conversion. Every execution was repeated five times.

Lastly, we compare the execution time of  analysis with only propagating the probability. Thus, we used 636 model generated randomly only having inner nodes with $\opAnd$ and $\opOr$ with a size of up to 1355 nodes, since literature examples are limited in amount and size. We calculate the success probability once with and once without  values.

Results are depicted in fig:tooleval and <ref>.  Our experiments show the following:

* Exports to the model checkers
, ,  and to the  format are
feasible for models of sizes commonly found in literature. With all except  needing less then a second for each model (see app:conversionTimes).

* Generating the stochastic game explicitly, which the
translation to  relies on, is time-consuming for models
with more than 30 nodes (see app:conversionTimes). Yet, verification using  may
still be of use in practice.

* The execution time may depend more on the model composition
than on the actual size of the underlying tree (see
fig:tooleval, <ref>).

* Verification using the  and  is faster than using  or . If evaluation is possible, the results are returned in less then ten seconds (see fig:tooleval).

*  model checking is useful for more complex objectives, posing an appropriate trade off.

* For  vs. non- analysis in , the slope of runtime differs roughly by a factor 10. None of the approaches takes more than a few seconds  (see fig:toolspac) even for attack-defense trees with more than 1000 vertices.

* The runtime of  and  using bottom-up analysis are in the same order in our experiments (see fig:tooleval).

§ CONCLUSION AND FUTURE WORK

We have provided a simple tool for synthesis and analysis of attack-defense trees that allows connection to model-checker workflows. The CLI enables further integration into other software pipelines. Settings for various degrees of background knowledge allow also non-experts to access the field of $\ADT{}$.
Furthermore, we provide a simple but effective way to bound the uncertainty in quantitative attack-defense tree analysis, using probably approximately correct inputs and outputs, obtaining uncertainty from data.
Our experiments show that all analysis can be done in reasonable time even for models much larger than found in literature.
Altogether,  presents several steps making the $\ADT{}$ framework more applicable in practice.

Future Work.
Firstly, we aim to support larger models and models with heterogeneous subtrees.  To this end, we want to design and implement compositional verification techniques to efficiently analyze, for instance, models where one subtree consists of only $\opAnd$ and $\opOr$ and one player, another requiring full-fledged timed analysis and a third one games.

Secondly, the semantics in terms of stochastic timed automata and stochastic turn-based games suffer from a  blow-up since all sequences of events need to be taken into account. One could employ partial-order reduction techniques in the conversion before model checking to reduce the model size.

Acknowledgments. We want to thank everyone who has contributed case studies to our benchmark collection  so far.
This research was funded in part by the German Research Foundation (DFG) project No. 427755713 GOPro, the MUNI Award in Science and Humanities MUNI/I/1757/2021 of the Grant Agency of Masaryk University, the  German Academic Scholarship Foundation and the ProSec project.

§ QUANTITATIVE BOTTOM-UP ANALYSES FOR COST AND DELAYS

[Delay ]

We define both the minimal and maximal delay interpretation $\interpretation$ with $\type=\RR_{\geq0}\times\RR_{\geq0}$, where the first component represents the delay of succeeding, the second component the delay of failing

* $\displaystyle{\interpretation(\vertex)((x_1,x_2),(y_1,y_2)) = (\max(x_1,y_1),\min(x_2,y_2))}$ (for minimal delay) and
$(\max(x_1,y_1).\max(x_2,y_2))$ (for maximal delay), if

* $\displaystyle{\interpretation(\vertex)((x_1,x_2),(y_1,y_2))= (\min(x_1,y_1),\max(x_2,y_2))}$ (for minimal delay) and
$\displaystyle{\interpretation(\vertex)((x_1,x_2),(y_1,y_2))= (\max(x_1,y_1),\max(x_2,y_2))}$ (for maximal delay)
if $\typeFunction(\vertex)=\opOr$

* $\displaystyle{\interpretation(\opNeg)(x_1,x_2)=(x_2,x_1)}$

[Cost ]

We define both the minimal and maximal cost interpretation $\interpretation$ with $\type=\RR_{\geq 0}\times \RR_{\geq0}$, where the first component represents the cost of succeeding, the second component the cost of failing.

* $\displaystyle{\interpretation(\vertex)((x_1,x_2),(y_1,y_2))= (x_1+y_1, \min(x_2,y_2))}$ (for minimal cost) and $(x_1+y_1,\max(x_2,y_2))$ (for maximal cost), if
if $\typeFunction(\vertex)=\opAnd$

* $\displaystyle{\interpretation(\vertex)((x_1,x_2),(y_1,y_2))=(\min(x_1,y_1),x_2+y_2)}$ (for minimal cost) and
$\displaystyle{\interpretation(\vertex)((x_1,x_2),(y_1,y_2))=(\max(x_1,y_1),x_2+y_2)}$ (for maximal cost) if $\typeFunction(\vertex)=\opOr$

* $\displaystyle{\interpretation(\opNeg)(x_1,x_2)=(x_2,x_1)}$

§ CONVERSION TIMES

Execution times for conversion of -files to the other formats.

§ CORRECTNESS OF BOTTOM-UP TRAVERSAL SEMANTICS

The following section recalls definitions from <cit.> and
adapts them to our attack-defense tree setting. We only allow
trees here (no DAGs).  We include the operator $\opTrigger$ only if
every basic event is triggered by at most one vertex. Additionally, we
require that vertices labeled with $\opTrigger$ have no successors,
and the main tree and the subtrees rooted in vertices with
$\opTrigger$ to be mutually disjoint. In this case, we can ensure an
order satisfying the constraints imposed by $\opTrigger$ for each
satisfying assignment.  In contrast to <cit.>, we allow
$\opTrigger$ as a restricted variant of $\opSand$[We use
$\opSand$ to represent a timed order and $\opTrigger$ to represent a
logic order.] and use $\opNeg$ rather than player swapping to focus
on the player controlling an event rather than whether an event
is useful or hindering for an attack. Additionally, we
assume that every basic event can only occur once in the tree. Thus,
we restrict the multiset semantics of <cit.> to a
powerset semantics.

In each case, $\interpretation(\opTrigger) = \Id$ and
$\interpretation(\basicEvent) = \interpretation(\opAnd)$ for
triggerable basic events $\basicEvent \in \basicEvents$.

Let $X$ be a set and let $X_1, X_2 \subseteq \powerset{X}$,
i.e. $X_1$ and $X_2$ are sets of sets with elements in $X$. We define
$X_1 \otimes X_2 \coloneqq \bigcup_{(x_1,x_2) \in X_{11} \times
X_{21}} \set{x_1\cup x_2}$. To restrict a set of basic events $X$ to
the basic events occurring in the subtree rooted in a
vertex $\vertex$, we write $X|_{\vertex}$.

We consider the operators $\opAnd$,$\opOr$, $\opTrigger$ and
$\opNeg$ and let all basic events be in
$\basicAttacks \disjointUnion \basicDefenses$. We define a powerset
interpretation $\interpretation$ with
$\type=\powerset{\powerset{\basicEvents}} \times \powerset{\powerset{\basicEvents}}$.

* $\interpretation(\vertex)((X_{11},X_{12}),(X_{21},X_{22}))=
(X_{11}\otimes X_{21},$ $X_{21} \cup X_{22} \cup (X_{21} \otimes
X_{22}) \cup (X_{12} \otimes X_{21}) \cup (X_{11} \otimes X_{22}))$ if $\vertex$ is a
triggerable basic event or $\typeFunction(\vertex)=\opAnd$

* $\interpretation(\vertex)((X_{11},X_{12}),(X_{21},X_{22}))=
((X_{11} \cup X_{21} \cup (X_{11} \otimes X_{21}) \cup$ $(X_{12}
\otimes X_{21}) \cup (X_{11} \otimes X_{22})), (X_{12}\otimes
X_{22}))$ for $\typeFunction(\vertex)=\opOr$

* $\displaystyle{\interpretation(\opNeg)((X_1,X_2))=(X_2,X_1)}$

* $\displaystyle{\interpretation(\opTrigger)=\Id}$

We denote the powerset bottom-up traversal semantics by $\values<P>$.

The powerset bottom-up traversal semantics computes two sets of
sets. In the first component, we collect all satisfying
assignments, in the second one all unsatisfying
assignments. Please note that we only denote events, which need to be
set to true. All events not contained, need to be set to false.

To compute successful and unsuccessful attacks at once, we
need to set
$\values[\basicEvents]<P>(\basicEvent) \coloneqq
(\set{\set{\basicEvent}},\set{\emptyset})$. For the powerset bottom-up
traversal semantics, we implicitely assume this valuation for basic
events in the following.

We consider the operators $\opAnd$,$\opOr$, $\opTrigger$ and
$\opNeg$ and let all basic events be in
$\basicAttacks \disjointUnion \basicDefenses$. We define a Boolean
interpretation $\interpretation$ with

* $\displaystyle{\interpretation(\vertex) (x_1,x_2)= \land
}$, if $\vertex$ is a triggerable basic event or

* $\displaystyle{\interpretation(\vertex)=\lor}$ for

* $\displaystyle{\interpretation(\opNeg)=\neg}$

* $\displaystyle{\interpretation(\opTrigger)=\Id}$

We denote the Boolean bottom-up traversal semantics by $\values<B>$.

Let $X \subseteq \basicEvents$. In the following, we denote by
$\values[\basicEvents,X]<B>$ the Boolean valuation such that
$\values[\basicEvents,X]<B>(\basicEvent)=\true$ if $\basicEvent \in X$
and false, otherwise.

Let $\exampleADD$ be an attack-defense tree and let
$\values<P>(\vertex) = (X_1,X_2)$.

* $x_1 \in X_1$ iff $\values<B>(\vertex)=\true$
w.r.t. $\values[\basicEvents,x_1]<B>$

* $x_2 \in X_2$ iff $\values<B>(\vertex)=\false$
w.r.t. $\values[\basicEvents,x_2]<B>$

Let $\exampleADD$ be an attack-defense tree. We proof both claims
simultaneously by induction on the structure of the attack-defense

* $\vertex$ is a non-triggerable basic
event. By definition $\values<B>(\vertex) = \true$ iff
$\values[\basicEvents]<B>(\vertex)=\true$. Since
$\values[\basicEvents]<P>(\vertex) = (\set{\set{\vertex}},
\set{\emptyset})$, the claims holds true.

* Induction Hypothesis: For all subtrees of $\vertex$
rooted in $\vertex<\ast>$ holds:

* $x_1 \in X_1$ iff $\values<B>(\vertex<\ast>)=\true$
w.r.t. $\values[\basicEvents,x_1]<B>$

* $x_2 \in X_2$ iff $\values<B>(\vertex<\ast>)=\false$
w.r.t. $\values[\basicEvents,x_2]<B>$

* $\typeFunction(\vertex)=\opTrigger$: The claim holds by
induction hypothesis and the definitions of $\values<P>$ and
$\values<B>$ (identity function for vertices labelled by

* $\vertex \in \basicEvents$ and triggered by
$\vertex<\ast> \in \vertices$. Let
$\values<P>(\vertex<\ast>)=(X_1^\ast,X_2^\ast)$. We have
$\values<B>(\vertex) = \values<B>(\vertex<\ast>) \land
\values<B>(\vertex)$. Thus, every satisfying assignment of the
subtree rooted in $\vertex<\ast>$ extended by $\vertex$ set to
true is a satisfying assignment of $\vertex$. We apply the
induction hypothesis to the subtree rooted in
$\vertex<\ast>$. Hence, by definition of $\otimes$ and the
induction hypothesis, Claim (1) holds true. Additionally,
$\values<B>(\vertex) = \false$ if $\vertex$ is set to false
(i.e. $\values[\basicEvents]<B>(\vertex)=\false$) or
$\values<B>(\vertex<\ast>)=\false$. Hence, by induction hypothesis
and the definition of $\values<P>$ for triggerable basic events,
Claim (2) holds, too.

* $\typeFunction(\vertex)=\opAnd$: Analogously to the proof for
triggerable basic events. However, the induction hypothesis needs
to be used on both subtrees.

* $\typeFunction(\vertex)=\opOr$: Analogously to the proof for
triggerable basic events. However, the induction hypothesis needs
to be used for both subtrees and the proofs of the two claims need
to be swapped.

* $\typeFunction(\vertex)=\opNeg$: Let $\vertex<\ast>$ be the input of
$\vertex$ and let $\values<P>(\vertex<\ast>)=(X_1,X_2)$. Since
$\values<B>(\vertex)=\true$ iff $\values<B>(\vertex<\ast>)=\false$ by
definition and each satisfying assignment of $\vertex<\ast>$ is an
unsatisfying assignment of $\vertex$ by definition, the claim
follows from the induction hypothesis.

We have proven theo:correctness by induction.

Let $\exampleADD$ be an attack-defense tree. We say that a
valuation $\values[\basicEvents] \colon \basicEvents \to
\set{\true,\false}$ is a successful attack if
$\val(\topGoal) = \true$, and unsuccessful attack
otherwise[Dually, this can be done for defenses by assigning
the goal $\topGoal$ to the defender. Since we do not use player
swapping as in <cit.>, there are no changes necessary to
this or the following semantics to apply them to defenses. However,
the valuation of the basic events might need to be modified (for
instance, excluding costs of the attacker when computing costs of
successful defenses). In the following, we only talk about attacks
and do not explicitely state that our results are dually correct for
defenses.]. We say a successful attack is minimal if there
does not exist an basic event $\basicEvent$ such that
$\values[\basicEvents](\basicEvent)=\true$ and the modified
valuation $\values<\ast>$ where $\values[\basicEvents]<\ast>(\basicEvent)=\false$ result both in $\val(\topGoal) = \true$.

\begin{equation}\label{eq:powerset}
\begin{aligned}
\values<\probabilityFunction>(\vertex)  =&  \sum_{x_1
\in X_1} \prod_{\basicEvent \in x_1|_{\vertex}}
\probabilityFunction(\basicEvent) \cdot \prod_{\basicEvent
\in \basicEvents\setminus x_1} 1-
\probabilityFunction(\basicEvent) =
\\
=&  1-\sum_{x_2|_{\vertex}
\in X_2} \prod_{\basicEvent \in x_2|_{\vertex}}
\probabilityFunction(\basicEvent) \cdot \prod_{\basicEvent \in
\basicEvents \setminus x_2|_{\vertex}} 1-
\probabilityFunction(\basicEvent)\\
\values<\costFunction,\min>(\vertex) = &  (\min_{x_1
\in X_1} \sum_{\basicEvent \in x_1}
\costFunction(\basicEvent), \min_{x_2|_{\vertex}
\in X_2} \sum_{\basicEvent \in x_2|_{\vertex}}
\costFunction(\basicEvent))\\
\values<\costFunction,\max>(\vertex) = & (\max_{x_1
\in X_1} \sum_{\basicEvent \in x_1}
\costFunction(\basicEvent),\max_{x_2|_{\vertex}
\in X_2} \sum_{\basicEvent \in x_2|_{\vertex}}
\costFunction(\basicEvent))\\
\values<\delayFunction,\min>(\vertex) = &  (\min_{x_1
\in X_1} \sum_{\basicEvent \in x_1}
\delayFunction(\basicEvent),\min_{x_2|_{\vertex}
\in X_2} \sum_{\basicEvent \in x_2|_{\vertex}}
\delayFunction(\basicEvent)) \\
\values<\delayFunction,\max>(\vertex) = & (\max_{x_1
\in X_1} \sum_{\basicEvent \in x_1}
\delayFunction(\basicEvent),\max_{x_1
\in X_1} \sum_{\basicEvent \in x_1}
\delayFunction(\basicEvent))
\end{aligned}
\end{equation}

Let $\exampleADD$ be an attack-defense tree and
$\values[\basicEvents]$ be a successful attack, let
$\vertex \in \vertices$ and $\values<P>(\vertex) = (X_1,X_2)$. The
equations in eq:powerset hold.

We prove all claims by an induction on the tree structure.

* $\vertex$ is a non-triggerable basic event. For each of the
five functions, the value assigned to the basic event is
returned. since
$(X_1|_{\vertex}, X_2|_{\vertex}) =
(\set{\set{\basicEvent}},\set{\emptyset})$, the claims hold by

* Induction Hypothesis: For subtrees rooted in a
vertex $\vertex<\ast>$, which are predecessors of the
vertex $\vertex$ , the equations in eq:powerset hold where
$\vertex$ is instantiated with the specific $\vertex<\ast>$.

* $\typeFunction(\vertex)=\opTrigger$: The claims follow by
definition of $\values<\probabilityFunction>$,
$\values<\costFunction,\min>$, $\values<\costFunction,\max>$,
$\values<\delayFunction,\min>$ and $\values<\delayFunction,\max>$
and the induction hypothesis (since $\opTrigger$ maps to the
identity function in all cases).

* $\typeFunction(\vertex)=\opNeg$: Let $\vertex<\ast>$ be the
input of vertex. The claims for $\values<\costFunction,\min>$,
$\values<\costFunction,\max>$, $\values<\delayFunction,\min>$ and
$\values<\delayFunction,\max>$ follow by their definition and the
induction hypothesis (since $\opNeg$ just swaps the components in
these cases). For $\values<\probabilityFunction>$, it holds
$\values<\probabilityFunction>(\vertex) =
1-\values<\probabilityFunction>(\vertex<\ast>)$. By induction
hypothesis, we have

* $1-\values<\probabilityFunction>(\vertex<\ast>) = 1 - \sum_{x_1
\in X_1|_{\vertex<\ast>}} \prod_{\basicEvent \in x_1}
\probabilityFunction(\basicEvent) \cdot \prod_{\basicEvent \in
\basicEvents\setminus x_1} 1-
\probabilityFunction(\basicEvent)$. By the definition of
$\values<P>$ for $\opNeg$, this is equivalent to
$1 - \sum_{x_2 \in X_2|_{\vertex<\ast>}} \prod_{\basicEvent \in
x_2} \probabilityFunction(\basicEvent) \cdot
\prod_{\basicEvent \in \basicEvents\setminus x_2|_{\vertex}} 1-
\probabilityFunction(\basicEvent)$.

* $1-\values<\probabilityFunction>(\vertex<\ast>) = 1 -
(1-\sum_{x_2 \in X_2|_{\vertex<\ast>}} \prod_{\basicEvent \in x_2}
\probabilityFunction(\basicEvent) \cdot \prod_{\basicEvent \in
\basicEvents \setminus x_2} 1-
\probabilityFunction(\basicEvent))$. By definition of
$\values<P>$ for $\opNeg$, this is equivalent to
$\sum_{x_1 \in X_1} 1-\prod_{\basicEvent \in \basicEvents
\setminus x_1} \probabilityFunction(\basicEvent) = \sum_{x_1
\in X_1} \prod_{\basicEvent \in x_1}
\probabilityFunction(\basicEvent)$

* $\vertex$ is a triggerable basic event and triggered by
$\vertex<\ast>$. Let $(X_1,X_2)=\values<P>(\vertex)$. We apply the
induction hypothesis to $\vertex<\ast>$.

* Let $(x.y) =
\values<\costFunction,\min>(\vertex<\ast>)$. Then,
$\values<\costFunction,\min>(\vertex) = (x +
\costFunction(\vertex), \min(y,\costFunction(\vertex)))$, which
is the same as
$(\min_{x_1 \in X_1|_{\vertex<\ast>}} \sum_{\basicEvent \in x_1}
\costFunction(\basicEvent) + \costFunction(\vertex),
\min(y,\costFunction(\vertex)))$. That is
$(\min_{x_1 \in X_1} \sum_{\basicEvent \in x_1}
\costFunction(\basicEvent), \min_{x_2 \in X_2}
\sum_{\basicEvent \in x_2} \costFunction(\basicEvent))$ by
the definition of $\values<P>$ for triggerable basic events (in
the first component, we add the vertex to all satisfying
assignments of the input, in the second component, we have a
union of all unsatisfying assignments, so the minimal element
can be computed this way).

* Analogously, we can prove the claims for
$\values<\costFunction,\max>$, $\values<\delayFunction,\min>$
and $\values<\delayFunction,\max>$

* $\values<\probabilityFunction>(\vertex) =
\values<\probabilityFunction>(\vertex<\ast>) \cdot
\probabilityFunction(\vertex)$. By induction hypothesis, this is
equivalent to
$(\sum_{x_1 \in X_1|_{\vertex<\ast>}} \prod_{\basicEvent \in
x_1} \probabilityFunction(\basicEvent) \cdot
\prod_{\basicEvent \in \basicEvents\setminus x_1} 1-
\probabilityFunction(\basicEvent)) \cdot
\probabilityFunction(\vertex) = \sum_{x_1 \in X_1}
\prod_{\basicEvent \in x_1} \probabilityFunction(\basicEvent)
\cdot \prod_{\basicEvent \in \basicEvents\setminus x_1} 1-
\probabilityFunction(\basicEvent)$. On the other hand, $\displaystyle{1-\sum_{x_2 \in X_2} \prod_{\basicEvent \in x_2}
\probabilityFunction(\basicEvent) \cdot \prod_{\basicEvent \in
\basicEvents\setminus x_2} 1-
\probabilityFunction(\basicEvent)}$ is equivalent to
$1-(k \cdot (1-\probabilityFunction(\vertex)) + k \cdot
\probabilityFunction(\vertex) + (1-k) \cdot
(1-\probabilityFunction(\vertex)))$ where
$k=\sum_{x_2 \in X_2|_{\vertex<\ast>}} \prod_{\basicEvent \in
x_2} \probabilityFunction(\basicEvent) \cdot
\prod_{\basicEvent \in \basicEvents\setminus x_2} 1-
\probabilityFunction(\basicEvent)$  by definition of $\values<P>$
for triggerable basic events. We have $1-(k -
k\cdot\probabilityFunction(\vertex) +
k\cdot\probabilityFunction(\vertex)+1 - k -
\probabilityFunction(\vertex) + k \cdot
\probabilityFunction(\vertex)) =
= \probabilityFunction(\vertex) \cdot (1-k)$. By induction
hypothesis, this is equivalent to $\probabilityFunction(\vertex)
\cdot \values<\probability>(\vertex<\ast>)$, which matches the
definition of $\values<\probability>$ for triggerable basic events.

* $\typeFunction(\vertex)=\opAnd$: Analogously to the proof for
triggerable basic events. However, the induction hypothesis needs
to be used on both subtrees.

* $\typeFunction(\vertex)=\opOr$: Analogously to the proof for
triggerable basic events. However, the induction hypothesis needs
to be used for both subtrees and the proofs of the two claims need
to be swapped.

§ CORRECTNESS OF PAC ANALYSIS

Let $\exampleADD$ be an attack-defense tree and let $\values[\basicEvents]$ be a  valuation for basic events, i.e., for every basic event $\basicEvent \in \basicEvents$, it holds $\values[\basicEvents](\basicEvent)$ is $(\error[\basicEvent],\prob[\basicEvent])$- for some $\error[\basicEvent] \in \RR_{\geq 0}$ and  $\prob[\basicEvent] \in [0,1]$. Let $(\error[\topGoal],\prob[\topGoal])$ be the error and the probability computed for the goal $\topGoal$. For any valuation $\values[\basicEvents]<\ast>$ such that $\values[\basicEvents]<\ast>(\basicEvent) \in \values[\basicEvents](\basicEvent) \pm \error[\basicEvent]$, it holds .

Instead of proving the claim directly, we show that for any two  values $x,y \in \RR_{\geq 0}$ (with $\error[x],\prob[x]$ and $\error[y],\prob[y])$, respectively), it holds: Let $x^\ast \in x\pm\error[x]$ and $y^\ast \in y\pm\error[y]$. Then

* $(1-x^\ast) \in (1-x)\pm\error[x]$: $x^\ast$ is at most $\error[x]$ away from $x$, i.e. the values range from
$(1-(x+\error[x]))=(1-x)-\error[x]$ to $(1-(x-\error[x])) = (1-x) + \error[x]$.

* $x^\ast \cdot y^\ast \in (x \cdot y) \pm x \cdot \error[y] + y \cdot \error[x] + \error[x]\cdot\error[y]$: This claim follows by $(x \pm\error[x])\cdot(y\pm\error[y]) = y\cdot x \pm \error[x]
\cdot y \pm y \cdot \error[x] \pm \error[x] \cdot \error[y]$.[While we can bound the error from above
clearly to $\error[1] \cdot x_2 + x_2 \cdot \error[2] + \error[1] \cdot \error[2]$, the respective term
$\error[1] \cdot x_2 - x_2 \cdot \error[2] - \error[1] \cdot \error[2]$ for a bound from below is not correct. Nevertheless,  we slightly over-estimate the true error from below to keep a centered interval under any circumstances and the claim still holds.]

* $x^\ast + y^\ast \in x+y\pm(\error[x]+\error[y])$: The claim holds since  $(x+\error[x])+(y+\error[y]) = x+y + (\error[x],\error[y])$ and  $(x-\error[x])+(y-\error[y]) = x+y - (\error[x],\error[y])$.

* $x^\ast + y^\ast - x^\ast \cdot y^\ast \in (x + y - x \cdot y)  \pm \error[x] + \error[y] + x \cdot \error[y] + y \cdot \error[x] + \error[x]\cdot\error[y]$: This case combines case 2 and case 3.

* $\max(x^\ast,y^\ast) \in \max(x,y) \pm \max(\error[x],\error[y])$: Clearly, $\max(x,y) + \max(\error[x],\error[y])$ is the largest value the term can attain. Since $\error[x],\error[y] \geq 0$,   $\max(x,y) - \max(\error[x],\error[y])$ is the smallest value the term can attain. Thus, the biggest error from the maximal value is given by $\max(\error[x],\error[y])$. [Using assumptions  on the distribution of the error, more precise estimates are possible.]

* $\min(x^\ast,y^\ast) \in \min(x,y) \pm \max(\error[x],\error[y])$: Clearly, $\min(x,y) - \max(\error[x],\error[y])$ is the smallest value the term can attain. Since $\error[x],\error[y] \geq 0$,    $\min(x,y) + \max(\error[x],\error[y])$ is the largest value the term can attain. Thus, the biggest error from the minimal value is given by $\max(\error[x],\error[y])$.fn:assumptions

The result of theo:pac then follows from a straightforward induction on the structure of the tree.

Missing 'biblatex' package
The bibliography requires the 'biblatex' package.

booktitle2019 19th International Conference on Application of Concurrency to System Design (ACSD)
titleParametric analyses of attack-fault trees

titleTime-Dependent Analysis of Attacks

booktitleComputer Security Foundations Symposium (CSF)
titleQuantitative Verification and Synthesis of Attack-Defence Scenarios

booktitleInternational Workshop on Smart Grid Security
titleDetermining the probability of smart grid attacks by combining attack tree and attack graph analysis

Washington, DC, USA

IEEE Computer Society

booktitleQuantitative Evaluation of Systems (QEST)
seriesQEST '06
titleUPPAAL 4.0

journaltitleData in Brief
titleApplication of the ARIMA model on the COVID-2019 epidemic dataset

booktitleTools and Algorithms for the Construction and Analysis of Systems (TACAS)
titleJANI: quantitative model and tool interaction

journaltitleComputers & Security
titleAttribute evaluation on attack trees with incomplete information

booktitleProceeding of the IASK International Conferences
titleA Delphi-based approach to fraud detection using attack trees and fuzzy numbers

booktitleProceedings of the international infrastructure survivability workshop
titleThe use of attack trees in assessing vulnerabilities in SCADA systems

[American Statistical Association, Taylor $\&$ Francis, Ltd.]

journaltitleJournal of Business $\&$ Economic Statistics
titleCalculating Interval Forecasts

booktitleTools and Algorithms for the Construction and Analysis of Systems (TACAS)
titlePRISM-games: A Model Checker for Stochastic Multi-Player Games

journaltitleIEEE Transactions on Power Systems
titleARIMA models to predict next-day electricity prices

booktitle2019 27th Telecommunications Forum (TELFOR)
titleAttack tree Model for Potential Attacks Against the SCADA System

booktitleInternational Conference on Computer Aided Verification
titleA storm is coming: A modern probabilistic model checker

booktitleInternational Conference on Quantitative Evaluation of Systems
titleExpected Cost Analysis of Attack-Defense Trees

booktitleInternational Workshop on Graphical Models for Security
titleAttack–defense trees for abusing optical power meters: A case study and the OSEAD tool experience report

booktitleThe Practice of Enterprise Modeling (IFIP)
titleUsing Attack-Defense Trees to Analyze Threats and Countermeasures in an ATM: A Case Study

booktitleQuantitative Evaluation of Systems (QEST)
titleAttack Trees for Practical Security Assessment: Ranking of Attack Scenarios with ADTool 2.0

journaltitleIEEE TRANSACTIONS ON SOFTWARE ENGINEERING
titleA Technique for Drawing Directed Graphs

booktitleTools and Algorithms for the Construction and Analysis of Systems (TACAS)
seriesLecture Notes in Computer Science
titleThe Modest Toolset: An Integrated Environment for Quantitative Modelling and Verification

booktitlePrinciples of Security and Trust (POST)
titleThe Value of Attack-Defence Diagrams

journaltitleInternational Journal of Electrical & Computer Engineering (2088-8708)
titleA risk and security assessment of VANET availability using attack tree concept.

Oxford University Press

titleMeasurements and their uncertainties: a practical guide to modern error analysis

booktitleIFIP International Information Security and Privacy Conference
titleAttack trees with sequential conjunction

BioMed Central

journaltitleBMC Medical Informatics and Decision Making
titleRisk management-based security evaluation model for telemedicine systems

booktitleAutomotive Cyber Security
titleSecurity and Privacy in Intelligent Autonomous Vehicles

titleDAG-Based Attack and Defense Modeling: Don't Miss the Forest for the Attack Trees

Springer International Publishing

booktitlePrinciples of Security and Trust (POST)
titleOn Quantitative Analysis of Attack–Defense Trees with Repeated Labels

Pisa, Italy

booktitleProceedings of the 7th International Conference on Formal Aspects of Security and Trust
titleFoundations of Attack-Defense Trees

Technology Publications, Lda

booktitleProceedings of the 14th International Conference on Evaluation of Novel Approaches to Software Engineering
titleA New Model-based Framework for Testing Security of IoT Systems in Smart Cities using Attack Trees and Price Timed Automata

booktitleFormal Modeling and Analysis of Timed Systems (FORMATS)
titleQuantitative Attack Tree Analysis via Priced Timed Automata

booktitleHigh Assurance Systems Engineering (HASE)
titleQuantitative Security and Safety Analysis with Attack-Fault Trees

booktitleProc. 23rd International Conference on Computer Aided Verification (CAV'11)
titlePRISM 4.0: Verification of Probabilistic Real-time Systems

booktitleProceedings of the 7th International Conference on Information Warfare and Security
titleUsing Attack Trees to Assess Security Controls for Supervisory Control and Data Acquisition Systems (SCADA)

journaltitleIEEE Transactions on Dependable and Secure Computing
titleEfficient and generic algorithms for quantitative attack tree analysis

Seoul, Korea

booktitleProceedings of the 8th International Conference on Information Security and Cryptology
titleFoundations of Attack Trees
attack trees,semantics,threat analysis

MCB UP Ltd

journaltitleJournal of Property Valuation and Investment
titleForecasting commercial rental values using ARIMA models

Washington, DC, USA

IEEE Computer Society

booktitleHawaii International Conference on System Sciences (HICSS)
seriesHICSS '06
titleQuantitative Cyber Risk Reduction Estimation Methodology for a Small SCADA Control System

Inderscience Publishers

journaltitleInternational Journal of Electronic Business
titleCombining attack trees and fuzzy numbers in a multi-agent approach to fraud detection

RTO Technical Report TR-IST-049, Research
Technology Organisation of NATO

titleImproving Common Security Risk Analysis

journaltitlearXiv preprint arXiv:2005.09535
titleBackstabber's Knife Collection: A Review of Open Source Software Supply Chain Attacks

booktitleInternational Workshop on Graphical Models for Security
titleQuantitative Attack Tree Analysis: Stochastic Bounds and Numerical Analysis

IOS Press

journaltitleSecurity and Privacy in the Internet of Things: Challenges and Solutions
titleAssessing Vulnerabilities in IoT-Based Ambient Assisted Living Systems

titleModel-based Cybersecurity Engineering for Connected and Automated Vehicles: The FLOURISH Project

International Journal of Emerging Technology in Learning

journaltitleInternational Journal of Emerging Technologies in Learning (iJET)
titleImpersonation Attack-Defense Tree

booktitle2017 Annual Reliability and Maintainability Symposium (RAMS)
titleUniform analysis of fault trees through model transformations

booktitleInternational Joint Conference on Electronic Voting
titleEffective Cybersecurity Awareness Training for Election Officials

Università Ca'Foscari Venezia

titleSecure deployment of HTTPS: Analysis and open challenges
typeB.S. thesis

booktitle2007 IEEE Power Engineering Society General Meeting
titleVulnerability assessment of cybersecurity for SCADA systems using attack trees

ACM New York, NY, USA

journaltitleACM Computing Surveys (CSUR)
titleBeyond 2014: Formal Methods for Attack Tree–based Security Modeling

issn1559-7067 1009-6124
journaltitleJournal of Systems Science and Complexity
titleA multiscale modeling approach incorporating ARIMA and anns for financial market volatility forecasting