QuADTool: Attack-Defense-Tree Synthesis, Analysis and Bridge to Verification
Extracted source text · arXiv 2406.15605
% !TeX spellcheck = en_US
\documentclass[conference]{llncs}
%\IEEEoverridecommandlockouts
\input{packages}
\input{tikz-defs}
\input{commands}
% IEEE only
% \theoremstyle{definition}
% \newtheorem{example}{Example}
% \newtheorem{definition}{Definition}
% \theoremstyle{plain}
% \newtheorem{theorem}{Theorem}
\newcounter{MYtempeqncnt}
\title{QuADTool: Attack-Defense-Tree Synthesis, Analysis and Bridge to Verification%\thanks{This research was funded in part by the German Research Foundation (DFG) project No.~427755713 \emph{GOPro} and the MUNI Award in Science and Humanities {MUNI/I/1757/2021} of the Grant Agency of Masaryk University.}
}
%\author{\IEEEauthorblockN{Florian
% Dorfhuber} \IEEEauthorblockA{Faculty of Computer Science \\
% Technical University of Munich \\ Munich, Germany \\ ...}
% \and \IEEEauthorblockN{Julia
% Eisentraut} \IEEEauthorblockA{Faculty of Computer Science \\
% Technical University of Munich \\ Munich, Germany \\
% https://orcid.org/0000-0002-7735-8751} \and
% \IEEEauthorblockN{Katharina Klioba}\IEEEauthorblockA{Faculty of ... \\
% Hamburg University of Technology \\ Hamburg, Germany \\ ...} \
% and \IEEEauthorblockN{Jan K\vret\'insk\'y}\IEEEauthorblockA{Faculty of Computer Science \\
% Technical University of Munich \\ Munich, Germany \\
% ...}}%
\author{Florian Dorfhuber\inst{1,2} \Letter \email{florian.dorfhuber@in.tum.de}
\orcidID{0000-0003-3755-7171}
\and \\ Julia Eisentraut\inst{2,3} \email{julia.eisentraut@posteo.de} \orcidID{0000-0002-7735-8751}
\and \\ Katharina Klioba\inst{4} \email{katharina.klioba@tuhh.de} \orcidID{0009-0002-7946-917X}
\and \\ Jan K\v{r}et\'{i}nsk\'{y}\inst{1,2} \email{jan.kretinsky@fi.muni.cz}
\orcidID{0000-0002-8122-2881}
}
\institute{Masaryk University, Brno, Czech Republic \and Technical University of Munich, Munich, Germany
\and State Parliament of Northrhine-Westfalia, Germany \and Technical University of Hamburg, Hamburg, Germany}
\newcommand{\todo}[1]{{\color{red}\bf[#1]}}
%\newcommand{\todo}[1]{}
\newcommand{\para}[1]{\medskip\noindent\textbf{#1}}
%\usepackage{amsthm}
%\theoremstyle{theorem}
%\newtheorem{example}{Example}
%\theoremstyle{definition}
%\newtheorem{example}{Example}
\newcommand{\qee}{\hfill$\triangle$}
\addbibresource{bibliography.bib}
\addbibresource{applications-attack-trees.bib}
\addbibresource{attack-trees.bib}
\addbibresource{fault-trees.bib}
\addbibresource{model-checkers.bib}
\addbibresource{time-series-analysis.bib}
% \setlength{\textfloatsep}{0.2\textfloatsep} % Space below/above a float if its [t]
% \setlength{\intextsep}{0.2\intextsep} % Space below/above a float if its [h]
% \setlength{\floatsep}{0.5\floatsep} % Space between floats
% \setlength{\abovecaptionskip}{0.2\abovecaptionskip}
% \setlength{\belowcaptionskip}{0.2\belowcaptionskip}
%%%%%%% PROLONG AS MUCH AS YOU WANT
% \renewcommand{\baselinestretch}{1} % >=0.97
% \advance\textwidth4mm % <= 5mm
% \advance\hoffset-2mm
% \advance\textheight4mm
% \advance\voffset-2mm
%\usepackage[firstpage]{draftwatermark}
%\SetWatermarkText{%
% \hspace*{5.5in}% moves the badge left/right
% \raisebox{4.2in}% moves the badge up/down
% {\includegraphics[scale=0.6]{aec-badge-qest_formats}}%
%}
%\SetWatermarkAngle{0}
\begin{document}
\maketitle
\pagestyle{plain}
\begin{abstract}
% $\quadtool$ is a tool to model and analyze (quantitative)
% attack-defense trees, a widespread formalism for security
% assessment
%
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 \emph{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 \emph{precise}
quantitative inputs (probabilities, timing, or costs of attacks),
which are rarely available.
Instead, only statistical, imprecise information is typically available, leaving us with \emph{probably approximately correct} (\PAC{})
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.
% Finally, we introduce a
% benchmark suite~\atbest{} consisting of 42 previously published
% attack-defense trees and 636 randomly generated models, on which we validate our method and our tool.
% Since the support for the analysis of these models is scattered
% over various tools and differs in the model features allowed, we
% provide a unifying GUI framework interfacing with the other tools
% as well as our own analysis algorithms. Most interestingly, we
% provide a ``PAC-input'' quantitative analysis. While standard
% quantitative analyses may distinguish likely from unlikely
% vulnerabilities, they rely on \emph{precise} quantitative inputs
% (probabilities, timing, or costs of attacks), which are rarely
% available. In contrast, previous experience may provide enough
% data for a \emph{probably approximately correct} estimate of the
% real quantity.
%
% The imprecision and uncertainty of the input quantities are thus
% bounded and propagated during our PAC-input quantitative analysis,
% bounding the imprecision and uncertainty of the final result of
% the analysis. Moreover, the tool provides support for accurate
% modelling of the PAC inputs as well as the corresponding analysis,
% incurring virtually no overhead. Finally, the tool comes also
% with a benchmark suite, on which we demonstrate its effectivity.
\end{abstract}
% \begin{IEEEkeywords}
% attack trees, attack-defense trees, machine learning, time series
% analysis, probably approximately correct, quantitative model
% checking
% \end{IEEEkeywords}
\input{introduction}
\input{at-examples}
\input{functionality}
\input{pac}
%\input{risqflan}
\input{experimental-results}
\input{conclusion}
\appendix
\input{appendix-full}
\newpage
\addcontentsline{toc}{chapter}{Bibliography}
\printbibliography
\end{document}
%Language and Font
\usepackage[english]{babel}
\usepackage{cancel} % different strike out with \cancel{}
% Command Definition
\usepackage{xifthen}
\usepackage{xparse}
\usepackage{biblatex}
% needs to be loaded before biblatex, otherwise broken :D
\PassOptionsToPackage{hyphens}{url}\usepackage{hyperref}
%\usepackage[style=ACM-Reference-Format,backend=bibtex]{biblatex}
%Font-Einstellungen mit XeLaTeX
%\usepackage{euler}
%
%\usepackage{xltxtra,fontspec,xunicode,chngcntr}
% \usepackage[T1]{fontenc}
%\usepackage[utf8]{inputenc}
\usepackage{footmisc}
%Math Symbols
\usepackage{amsmath}
\usepackage[misc]{ifsym}
\usepackage{amssymb}
\usepackage{pifont}% http://ctan.org/pkg/pifont
\newcommand{\cmark}{\ding{51}}%
\newcommand{\xmark}{\ding{55}}%
\usepackage{mathtools}
\usepackage{proof}
% defines command \infer[name]{conclusion}{premises lists separated by &; }
% \infer= uses two lines for inference rule, \infer* uses three dots
% \deduce uses <-> from premise to conclusion
\usepackage{stmaryrd} %Semantikklammern
\usepackage{upgreek} % nicer rho
\usepackage{stackengine}
\usepackage{adjustbox}
\usepackage{enumitem}
\usepackage{float}
% Figures
\usepackage{tikz}
\usepackage[plain]{fancyref}
% easier references, especially no breaks
% between Figure, Section etc. and number
\usepackage{float}
\usepackage{subcaption}
\captionsetup{compatibility=false}
\usepackage{wrapfig}
%to include graphics
\usepackage{graphicx}
% PDF Display Options
\usepackage{fancyhdr}
\usepackage{marginfix} % comments in margin
\usepackage{microtype}
\usepackage{pdflscape} % allows to use landscape mode
%\usepackage{geometry}
\usepackage{totpages}
% Tables
\usepackage{longtable}
\usepackage{tabularx}
\usepackage{multirow}
\usepackage{booktabs}
\usepackage{adjustbox}
\usepackage{array}
%Compact Lists
\usepackage{multicol} %Definition von mehrspaltigen Abschnitten
\usepackage{enumitem}
%Code
\usepackage{listings}
\usepackage{algorithm}
\usepackage[noend]{algpseudocode}
\MakeRobust{\Call}
%%% Local Variables:
%%% mode: latex
%%% TeX-engine: xetex
%%% TeX-master: "main"
%%% End:
\usetikzlibrary{%
arrows,%
calc,%
shapes.misc,%
shapes.arrows,%
chains,%
matrix,%
positioning,%
scopes,%
decorations.pathmorphing,%
decorations.pathreplacing,%
shadows,%
er,%
trees,%
shapes,%
automata,%
patterns%
}
\pgfdeclarelayer{edgelayer}
\pgfdeclarelayer{nodelayer}
\pgfsetlayers{edgelayer,nodelayer,main}
\tikzset{initial text={}}
\tikzstyle{none}=[inner sep=0pt]
\tikzstyle{gate}=[rectangle,draw=black, inner sep=5pt,outer sep=1pt]
\tikzstyle{and}=[gate]
\tikzstyle{or}=[gate]
\tikzstyle{seq}=[gate]
\tikzstyle{neg}=[gate]
\tikzstyle{fail}=[gate]
\tikzstyle{cost}=[gate, minimum height=2.5em, rectangle split, rectangle split parts=2, rectangle split draw splits=false, inner sep=3pt]
\tikzstyle{trigger}=[gate]
\tikzstyle{costguard}=[above,font=\scriptsize]
\tikzstyle{smallgate}=[gate,inner sep=4pt]
\tikzstyle{urgent}=[font={\scriptsize{\sf \textcolor{Dimgray}{U}}}, inner sep=0pt]
\tikzstyle{state-circle}=[circle,draw=black,inner sep=2pt,minimum size=0.35cm,outer sep=2pt]
\tikzstyle{state}=[ellipse,draw=black,inner sep=2pt,outer sep=2pt]
\tikzstyle{state-box}=[rectangle,draw=black,inner sep=2pt,minimum size=0.35cm,outer sep=2pt]
\tikzstyle{probability-state}=[circle,fill=black,draw=black,inner sep=0pt,minimum size=1pt]
\tikzstyle{BETrig}=[regular polygon,regular polygon sides=3,draw=black, inner sep=0pt, outer sep=1pt,minimum width=0.85cm]
\tikzstyle{reset}=[rectangle,draw=black, inner sep=5pt]
\tikzstyle{nodename}=[text width=1.8cm, align=center]
\tikzstyle{bename}=[nodename, below=0.3]
\tikzstyle{gatename}=[nodename, above=0.3]
\tikzstyle{costname}=[nodename, above=0.4]
\tikzstyle{update}=[font=\scriptsize]
%\tikzstyle{false}=[color={Red!70!black}]
\tikzstyle{false}=[color={ACMRed!70!black}]
%\tikzstyle{true}=[color={Green!70!black}]
\tikzstyle{true}=[color={ACMGreen!70!black}]
\tikzstyle{undefined}=[color={black!70}]
\tikzstyle{tt}=[defender]
\tikzstyle{ff}=[attacker]
\tikzstyle{uu}=[neutral]
%\tikzstyle{attacker}=[fill={Red!30},postaction={pattern=horizontal lines,pattern color=Red!60}]
\tikzstyle{attacker}=[fill={ACMRed!30},postaction={pattern=horizontal lines,pattern color=ACMRed!60}]
%\tikzstyle{defender}=[fill={Green!30},postaction={pattern=vertical lines,pattern color=Green!60}]
\tikzstyle{defender}=[fill={ACMGreen!50},postaction={pattern=vertical lines,pattern color=ACMGreen!80}]
%\tikzstyle{neutral}=[fill={gray!30},postaction={pattern=crosshatch dots,pattern color=gray!80},font=\bf]
\tikzstyle{neutral}=[fill={gray!30},postaction={pattern=crosshatch dots,pattern color=gray!80},font=\bf]
\tikzstyle{nothing}=[]
\tikzstyle{arrow-urgent}=[-latex,draw=black]
\tikzstyle{arrow-non-urgent}=[-latex,draw=black,dashed]
\tikzstyle{arrow-simple}=[-latex,draw=black]
\tikzstyle{arrow-reset}=[-latex,dashed]
\tikzstyle{arrow-trigger}=[-latex,decoration={snake,segment length=4,amplitude=.6, post=lineto,post length=2pt},decorate]
\tikzstyle{arrow-segment-after-probabilities}=[-latex,draw=black]
\tikzstyle{markovian}=[->,draw=black,postaction={decorate},decoration={markings,mark=at position .5 with {\arrow{>}}}]
\tikzstyle{arrow-segment-before-probabilities-immediate}=[-,draw=black]
\tikzstyle{arrow-segment-before-probabilities-timed}=[-,draw=black]
\tikzstyle{stateText}=[rectangle,fill=White,draw=black, inner sep=5pt, minimum height=0pt]
\tikzstyle{non-urgent}=[densely dashed]
%%% Local Variables:
%%% mode: latex
%%% TeX-engine: xetex
%%% TeX-master: "main"
%%% End:
% Format
%-----------------------------------------------------------------------------
\newcommand{\highlight}[1]{\textsf{\textbf{#1}}}
% Fancyref
%-----------------------------------------------------------------------------
%Appendix
\newcommand*{\fancyrefapplabelprefix}{app}
\fancyrefaddcaptions{english}{%
\providecommand*{\frefappname}{appendix}%
\providecommand*{\Frefappname}{Appendix}%
}
\frefformat{plain}{\fancyrefapplabelprefix}{\frefappname\fancyrefdefaultspacing#1}
\Frefformat{plain}{\fancyrefapplabelprefix}{\Frefappname\fancyrefdefaultspacing#1}
\frefformat{vario}{\fancyrefapplabelprefix}{%
\frefappname\fancyrefdefaultspacing#1#3%
}
\Frefformat{vario}{\fancyrefapplabelprefix}{%
\Frefappname\fancyrefdefaultspacing#1#3%
}
%Line in Algorithm
\newcommand*{\fancyreflinelabelprefix}{line}
\fancyrefaddcaptions{english}{%
\providecommand*{\freflinename}{line}%
\providecommand*{\Freflinename}{Line}%
}
\frefformat{plain}{\fancyreflinelabelprefix}{\freflinename\fancyrefdefaultspacing#1}
\Frefformat{plain}{\fancyreflinelabelprefix}{\Freflinename\fancyrefdefaultspacing#1}
\frefformat{vario}{\fancyreflinelabelprefix}{%
\freflinename\fancyrefdefaultspacing#1#3%
}
\Frefformat{vario}{\fancyreflinelabelprefix}{%
\Freflinename\fancyrefdefaultspacing#1#3%
}
%Table
% \newcommand*{\fancyreftablabelprefix}{tab}
% \fancyrefaddcaptions{english}{%
% \providecommand*{\freftabname}{table}%
% \providecommand*{\Freftabname}{Table}%
% }
% \frefformat{plain}{\fancyreftablabelprefix}{\freftabname\fancyrefdefaultspacing#1}
% \Frefformat{plain}{\fancyreftablabelprefix}{\Freftabname\fancyrefdefaultspacing#1}
% \frefformat{vario}{\fancyreftablabelprefix}{%
% \freftabname\fancyrefdefaultspacing#1#3%
% }
% \Frefformat{vario}{\fancyreftablabelprefix}{%
% \Freftabname\fancyrefdefaultspacing#1#3%
% }
%Example
\newcommand*{\fancyrefexlabelprefix}{ex}
\fancyrefaddcaptions{english}{%
\providecommand*{\frefexname}{example}%
\providecommand*{\Frefexname}{Example}%
}
\frefformat{plain}{\fancyrefexlabelprefix}{\frefexname\fancyrefdefaultspacing#1}
\Frefformat{plain}{\fancyrefexlabelprefix}{\Frefexname\fancyrefdefaultspacing#1}
\frefformat{vario}{\fancyrefexlabelprefix}{%
\frefexname\fancyrefdefaultspacing#1#3%
}
\Frefformat{vario}{\fancyrefexlabelprefix}{%
\Frefexname\fancyrefdefaultspacing#1#3%
}
%Definition
\newcommand*{\fancyrefdeflabelprefix}{def}
\fancyrefaddcaptions{english}{%
\providecommand*{\frefdefname}{definition}%
\providecommand*{\Frefdefname}{Definition}%
}
\frefformat{plain}{\fancyrefdeflabelprefix}{\frefdefname\fancyrefdefaultspacing#1}
\Frefformat{plain}{\fancyrefdeflabelprefix}{\Frefdefname\fancyrefdefaultspacing#1}
\frefformat{vario}{\fancyrefdeflabelprefix}{%
\frefdefname\fancyrefdefaultspacing#1#3%
}
\Frefformat{vario}{\fancyrefdeflabelprefix}{%
\Frefdefname\fancyrefdefaultspacing#1#3%
}
%Theorem
\newcommand*{\fancyreftheolabelprefix}{theo}
\fancyrefaddcaptions{english}{%
\providecommand*{\freftheoname}{theorem}%
\providecommand*{\Freftheoname}{Theorem}%
}
\frefformat{plain}{\fancyreftheolabelprefix}{\freftheoname\fancyrefdefaultspacing#1}
\Frefformat{plain}{\fancyreftheolabelprefix}{\Freftheoname\fancyrefdefaultspacing#1}
\frefformat{vario}{\fancyreftheolabelprefix}{%
\freftheoname\fancyrefdefaultspacing#1#3%
}
\Frefformat{vario}{\fancyreftheolabelprefix}{%
\Freftheoname\fancyrefdefaultspacing#1#3%
}
%Algorithm
\newcommand*{\fancyrefalglabelprefix}{alg}
\fancyrefaddcaptions{english}{%
\providecommand*{\frefalgname}{algorithm}%
\providecommand*{\Frefalgname}{Algorithm}%
}
\frefformat{plain}{\fancyrefalglabelprefix}{\frefalgname\fancyrefdefaultspacing#1}
\Frefformat{plain}{\fancyrefalglabelprefix}{\Frefalgname\fancyrefdefaultspacing#1}
\frefformat{vario}{\fancyrefalglabelprefix}{%
\frefalgname\fancyrefdefaultspacing#1#3%
}
\Frefformat{vario}{\fancyrefalglabelprefix}{%
\Frefalgname\fancyrefdefaultspacing#1#3%
}
%Lemma
\newcommand*{\fancyreflemlabelprefix}{lem}
\fancyrefaddcaptions{english}{%
\providecommand*{\freflemname}{lemma}%
\providecommand*{\Freflemname}{Lemma}%
}
\frefformat{plain}{\fancyreflemlabelprefix}{\freflemname\fancyrefdefaultspacing#1}
\Frefformat{plain}{\fancyreflemlabelprefix}{\Freflemname\fancyrefdefaultspacing#1}
\frefformat{vario}{\fancyreflemlabelprefix}{%
\freflemname\fancyrefdefaultspacing#1#3%
}
\Frefformat{vario}{\fancyreflemlabelprefix}{%
\Freflemname\fancyrefdefaultspacing#1#3%
}
%Corollary
\newcommand*{\fancyrefcorlabelprefix}{cor}
\fancyrefaddcaptions{english}{%
\providecommand*{\frefcorname}{corollary}%
\providecommand*{\Frefcorname}{Corollary}%
}
\frefformat{plain}{\fancyrefcorlabelprefix}{\frefcorname\fancyrefdefaultspacing#1}
\Frefformat{plain}{\fancyrefcorlabelprefix}{\Frefcorname\fancyrefdefaultspacing#1}
\frefformat{vario}{\fancyrefcorlabelprefix}{%
\frefcorname\fancyrefdefaultspacing#1#3%
}
\Frefformat{vario}{\fancyrefcorlabelprefix}{%
\Frefcorname\fancyrefdefaultspacing#1#3%
}
%Corollary
\newcommand*{\fancyrefsubseclabelprefix}{subsec}
\fancyrefaddcaptions{english}{%
\providecommand*{\frefsubsecname}{subsection}%
\providecommand*{\Frefsubsecname}{Subsection}%
}
\frefformat{plain}{\fancyrefsubseclabelprefix}{\frefsubsecname\fancyrefdefaultspacing#1}
\Frefformat{plain}{\fancyrefsubseclabelprefix}{\Frefsubsecname\fancyrefdefaultspacing#1}
\frefformat{vario}{\fancyrefsubseclabelprefix}{%
\frefsubsecname\fancyrefdefaultspacing#1#3%
}
\Frefformat{vario}{\fancyrefsubseclabelprefix}{%
\Frefsubsecname\fancyrefdefaultspacing#1#3%
}
%Review
\newcommand*{\fancyrefreviewlabelprefix}{rev}
\fancyrefaddcaptions{english}{%
\providecommand*{\frefreviewname}{review}%
\providecommand*{\Frefreviewname}{Review}%
}
\frefformat{plain}{\fancyrefreviewlabelprefix}{\frefreviewname\fancyrefdefaultspacing#1}
\Frefformat{plain}{\fancyrefreviewlabelprefix}{\Frefreviewname\fancyrefdefaultspacing#1}
\frefformat{vario}{\fancyrefreviewlabelprefix}{%
\frefreviewname\fancyrefdefaultspacing#1#3%
}
\Frefformat{vario}{\fancyrefreviewlabelprefix}{%
\Frefreviewname\fancyrefdefaultspacing#1#3%
}
% Redefining Commands
%-----------------------------------------------------------------------------
\renewcommand{\phi}{\upvarphi}
\renewcommand{\psi}{\uppsi}
\renewcommand{\multicolsep}{0pt}
\renewcommand{\rho}{\upvarrho}
\renewcommand{\upsilon}{\upupsilon}
\renewcommand{\chi}{\upchi}
\renewcommand{\circ}{\bigcirc}
\renewcommand{\max}{\mathop{\mathsf{max}}}
\renewcommand{\min}{\mathop{\mathsf{min}}}
\renewcommand{\sup}{\mathop{\mathsf{sup}}}
\renewcommand{\inf}{\mathop{\mathsf{inf}}}
% Abbreviations
%-----------------------------------------------------------------------------
\newcommand{\formattool}[1]{\textsf{#1}}
\newcommand{\formatstandard}[1]{\textsf{#1}}
\newcommand{\formatnames}[1]{\textsl{#1}}
\newcommand{\adt}{\formatnames{ADT}}
\newcommand{\PAC}{\formatnames{PAC}}
\newcommand{\DOT}{\formatstandard{DOT}}
\newcommand{\XML}{\formatstandard{XML}}
\newcommand{\UPPAAL}{\formattool{UPPAAL}}
\newcommand{\prism}{\formattool{PRISM}}
\newcommand{\quadtool}{\formattool{QuADTool}}
\newcommand{\quadtoolURL}{\url{https://gitlab.com/live-lab/software/add-tool/-/blob/main/release/latest.jar}}
\newcommand{\modest}{\formattool{MODEST}}
\newcommand{\storm}{\formattool{STORM}}
\newcommand{\prismgames}{\formattool{PRISM-games}}
\newcommand{\jani}{\formatstandard{JANI}}
\newcommand{\adtool}{\formattool{ADTool}}
\newcommand{\adtoolURL}{\url{https://gitlab.com/live-lab/software/add-tool/-/blob/main/release/latest.jar}}
\newcommand{\atbest}{\formatstandard{ATBEST}}
\newcommand{\atbestURL}{\url{https://www.model.in.tum.de/~kraemerj/upload/}}
\newcommand{\artifactURL}{\url{https://cryptpad.fr/drive/\#/2/drive/view/c1GxWgaefmODN76p1NQ-F0Q-I4FDvBDXo5xaGVDpmmw/}}
\newcommand{\risqflan}{\formattool{RisQFLan}}
\newcommand{\attop}{\formattool{ATTop}}
\newcommand{\WYSIWYG}{\formattool{WYSIWYG}}
\newcommand{\MultiVeStA}{\formattool{MultiVeStA}}
\newcommand{\GeneticA}{\textsf{GA}}
\newcommand{\Logistic}{\textsf{LR}}
\newcommand{\aont}{attack-defense trees}
\newcommand{\aot}{attack trees}
\newcommand{\seqt}{sequential attack trees}
\newcommand{\orcidID}[1]{{\href{https://orcid.org/#1}{\protect\raisebox{3.25pt}{\protect\includegraphics{orcid_color}}}}}
% Comments
%-----------------------------------------------------------------------------
% \newcommand{\julia}[1]{{\footnotesize{\textcolor{Green}{\textsf{\textbf{julia:
% #1}}}}}}
% \newcommand{\katharina}[1]{{\footnotesize{\textcolor{Blue}{\textsf{\textbf{katharina: #1}}}}}}
% \newcommand{\jan}[1]{{\footnotesize{\textcolor{Red}{\textsf{\textbf{jan: #1}}}}}}
\newcommand{\julia}[1]{}
\newcommand{\jan}[1]{}
\newcommand{\katharina}[1]{}
% Environments
%-----------------------------------------------------------------------------
\newenvironment{lemma*}[1]{\medskip\noindent\textbf{Recap of Lemma\ifthenelse{\isempty{#1}}{}{~#1}.}}{}
\newenvironment{theorem*}[1]{\medskip\noindent\textbf{Recap of Theorem\ifthenelse{\isempty{#1}}{}{~#1}.}}{}
\newenvironment{proofoutline}{\medskip\noindent\emph{Proof
Outline.}}{\hfill$\square$\smallskip}
% \newenvironment{observation}[1]{\medskip\noindent\textbf{Definition~\ifthenelse{\isempty{#1}}{}{(#1)}.}}{\hfill$\triangle$\smallskip}
\newtheorem{observation}{Observation}
% Logic
%-----------------------------------------------------------------------------
% \newcommand{\land}{\wedge}
% \newcommand{\lor}{\vee}
\newcommand{\limpl}{\Rightarrow}
\newcommand{\lequiv}{\Leftrightarrow}
\newcommand{\lxor}{\oplus}
\newcommand{\swp}{\mathop{\neg_\mathsf{swp}}}
\newcommand{\true}{\mathsf{tt}}
\newcommand{\false}{\mathsf{ff}}
\newcommand{\undecided}{\mathsf{uu}}
\newcommand{\truthvalue}[1][{}]{\mathsf{tv}_{#1}}
\DeclareDocumentCommand{\variable}{O{} D<>{}}{\mathsf{v}_{#1}^{#2}}
\DeclareDocumentCommand{\variables}{O{} D<>{}}{\mathcal{V}_{#1}^{#2}}
\newcommand{\logic}{\mathcal{L}}
% Sets
% -----------------------------------------------------------------------------
\newcommand{\set}[1]{\{#1\}}
\newcommand{\powerset}[1]{2^{#1}}
\newcommand{\disjointUnion}{\mathop{\dot{\cup}}}
\newcommand{\setcomplement}[1]{\overline{#1}}
\newcommand{\NN}{\mathbb{N}}
\newcommand{\BB}{\mathbb{B}}
\newcommand{\ZZ}{\mathbb{Z}}
\newcommand{\QQ}{\mathbb{Q}}
\newcommand{\RR}{\mathbb{R}}
\DeclareDocumentCommand{\anySet}{O{} D<>{}}{\mathcal{X}_{#1}^{#2}}
\newcommand{\setValues}{\set{\true,\undecided,\false}}
\newcommand{\setAgents}{\set{\attacker,\defender}}
\newcommand{\setCDFs}{\mathsf{CDFs}}
\newcommand{\fset}{\mathsf{N}}
% Functions
% ---------------------------------------------%
%\newcommand{\undefined}{\mathsf{undef}}
\newcommand{\pto}{\hookrightarrow}
% \DeclareMathOperator*{\argmax}{arg\,max}
% \DeclareMathOperator*{\argmin}{arg\,min}
\newcommand{\convolution}{\mathsf{conv}}
% Complexity
%-----------------------------------------------------------------------------
\newcommand{\np}{\textsl{NP}}
\newcommand{\conp}{\textsl{co-NP}}
\newcommand{\pspace}{\textsl{PSPACE}}
\newcommand{\expspace}{\textsl{EXPSPACE}}
%\newcommand{\p}{\textsl{P}}
\DeclareDocumentCommand{\alg}{O{} D<>{} D(){}}{\mathcal{A}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
% Probability Theory
%-----------------------------------------------------------------------------
\DeclareDocumentCommand{\distribution}{O{} D<>{} D(){}}{\mu_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\newcommand{\distributions}{\mathcal{D}}
\DeclareDocumentCommand{\probability}{O{} D<>{} D(){}}{\mathbb{P}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{\big(#3\big)}}
\DeclareDocumentCommand{\expectation}{O{} D<>{} D(){}}{\mathbb{E}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{[#3]}}
\DeclareDocumentCommand{\support}{O{} D<>{} D(){}}{\mathsf{Supp}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\newcommand{\dirac}[1]{\delta_{#1}}
\DeclareDocumentCommand{\cylinder}{O{} D<>{} D(){}}{\mathsf{Cyl}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{\big(#3\big)}}
\DeclareDocumentCommand{\algebra}{O{} D<>{} D(){}}{\mathcal{F}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{\big(#3\big)}}
\DeclareDocumentCommand{\probspace}{O{} D<>{}}{\big(\Omega_{#1}^{#2},\mathcal{F}_{#1}^{#2},\probability\big)}
\DeclareDocumentCommand{\density}{O{} D<>{} D(){}}{\mathsf{f}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\randomVariable}{O{} D<>{} D(){} D(){}}{\mathsf{C}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}\ifthenelse{\isempty{#4}}{}{(#4)}}
% Attack Defence Diagrams - Operators
%-----------------------------------------------------------------------------
\newcommand{\opformat}[1]{\mathbin{\mathtt{#1}}}
\newcommand{\opAnd}{\opformat{AND}}
\newcommand{\opOr}{\opformat{OR}}
\newcommand{\opSand}{\opformat{SAND}}
\newcommand{\opSor}{\opformat{SOR}}
\newcommand{\opIf}{\opformat{IF}}
\newcommand{\opIfNot}{\opformat{IFN}}
\newcommand{\opReset}{\opformat{RE}}
\newcommand{\opTrigger}{\opformat{TR}}
\newcommand{\opNeg}{\opformat{NOT}}
\newcommand{\opIvr}{\opformat{NAT}}% Attack Fault Trees - Operators
\newcommand{\opFail}{\opformat{FAIL}}
\newcommand{\opWHO}{\opformat{WHO}}
\newcommand{\opXOR}{\opformat{XOR}}
\newcommand{\opCost}{\opformat{COST}}
\newcommand{\opFDEP}{\opformat{FDEP}}
\newcommand{\logicOperators}{\set{\opAnd,\opOr,\opNeg}}
% Attack Fault Trees - Operators
%-----------------------------------------------------------------------------
\DeclareDocumentCommand{\opVot}{O{k/n}}{\opformat{VOT}(#1)}
\DeclareDocumentCommand{\opSpare}{}{\opformat{SPARE}}
% Attack Fault Trees - Graphs and Graph Predicates
%-----------------------------------------------------------------------------
\DeclareDocumentCommand{\graph}{O{} D<>{}}{\mathsf{G}_{#1}^{#2}}
\DeclareDocumentCommand{\vertex}{O{} D<>{}}{\mathsf{v}_{#1}^{#2}}
\DeclareDocumentCommand{\othervertex}{O{} D<>{}}{\mathsf{u}_{#1}^{#2}}
\DeclareDocumentCommand{\vertices}{O{} D<>{}}{\mathsf{V}_{#1}^{#2}}
\DeclareDocumentCommand{\edge}{O{} D<>{}}{\mathsf{e}_{#1}^{#2}}
\DeclareDocumentCommand{\edges}{O{} D<>{}}{\mathsf{E}_{#1}^{#2}}
\DeclareDocumentCommand{\inp}{O{} D<>{} D(){}}{\mathsf{in}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\exampleGraph}{O{} D<>{}}{\graph[#1]<#2>=(\vertices[#1]<#2>, \edges[#1]<#2>)}
% Attack Fault Diagrams - ADD Names
%-----------------------------------------------------------------------------
\DeclareDocumentCommand{\AFT}{O{} D<>{}}{\mathsf{AFT}_{#1}^{#2}}
\DeclareDocumentCommand{\ADT}{O{} D<>{}}{\mathsf{ADT}_{#1}^{#2}}
\DeclareDocumentCommand{\ADD}{O{} D<>{}}{\mathsf{ADT}_{#1}^{#2}}
\DeclareDocumentCommand{\AT}{O{} D<>{}}{\mathsf{AT}_{#1}^{#2}}
\DeclareDocumentCommand{\aft}{}{\emph{AFT}}
\DeclareDocumentCommand{\topGoal}{O{} D<>{}}{\mathsf{g}_{#1}^{#2}}
\newcommand{\attacker}{\mathsf{\color{red}A}}
\newcommand{\defender}{\mathsf{\color{green}D}}
\newcommand{\timedriven}{\mathsf{\color{gray}T}}
\newcommand{\topAtt}{\texttt{\color{red}Att}}
% Attack Fault Trees - Syntax
%-----------------------------------------------------------------------------
\DeclareDocumentCommand{\operator}{O{} D<>{} D(){}}{\mathsf{op}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\operators}{O{} D<>{} D(){}}{\mathsf{O}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\basicEvent}{O{} D<>{}}{\mathsf{be}_{#1}^{#2}}
\DeclareDocumentCommand{\basicEvents}{O{} D<>{}}{\mathsf{BE}_{#1}^{#2}}
\DeclareDocumentCommand{\basicComponent}{O{} D<>{}}{\mathsf{bc}_{#1}^{#2}}
\DeclareDocumentCommand{\basicComponents}{O{} D<>{}}{\mathsf{BC}_{#1}^{#2}}
\DeclareDocumentCommand{\basicAttack}{O{} D<>{}}{\mathsf{ba}_{#1}^{#2}}
\DeclareDocumentCommand{\basicAttacks}{O{} D<>{}}{\mathsf{BA}_{#1}^{#2}}
\DeclareDocumentCommand{\basicDefense}{O{} D<>{}}{\mathsf{bd}_{#1}^{#2}}
\DeclareDocumentCommand{\basicDefenses}{O{} D<>{}}{\mathsf{BD}_{#1}^{#2}}
\DeclareDocumentCommand{\probabilityFunction}{O{} D<>{} D(){}}{\mathsf{Pr}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\delayFunction}{O{} D<>{} D(){}}{\mathsf{Delay}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\costFunction}{O{} D<>{} D(){}}{\mathsf{Cost}_{E}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\distributionFunction}{O{} D<>{} D(){}}{\mathsf{Dist}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\costDelayFunction}{O{} D<>{} D(){}}{\mathsf{Cost}_{D}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\newcommand{\gates}{\mathsf{G}}
\newcommand{\gate}{\mathsf{g}}
\newcommand{\subscript}[2]{$#1 _ #2$}
\DeclareDocumentCommand{\triggerTransitions}{O{} D<>{}}{\mathsf{TEdge}_{#1}^{#2}}
\DeclareDocumentCommand{\triggerBE}{O{} D<>{}}{\basicEvents[\opTrigger\ifthenelse{\isempty{#1}}{}{,#1}]<#2>}
\DeclareDocumentCommand{\resetTransitions}{O{} D<>{}}{\mathsf{REdge}_{#1}^{#2}}
\DeclareDocumentCommand{\resetBE}{O{} D<>{}}{\basicEvents[\opReset\ifthenelse{\isempty{#1}}{}{,#1}]<#2>}
\DeclareDocumentCommand{\typeFunction}{O{} D<>{} D(){}}{\mathsf{t}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\exampleAFT}{O{} D<>{}}{\AFT[#1]<#2>=(\vertices[#1]<#2>,
\edges[#1]<#2>, \typeFunction[#1]<#2>,
\triggerTransitions[#1]<#2>)}
\DeclareDocumentCommand{\exampleADD}{O{} D<>{}}{\ADT[#1]<#2>=(\vertices[#1]<#2>,
\edges[#1]<#2>, \typeFunction[#1]<#2>)} %\distributionFunction[#1]<#2>,
% \triggerTransitions[#1]<#2>, \resetTransitions[#1]<#2>)}
\DeclareDocumentCommand{\exampleAT}{O{} D<>{}}{\AT[#1]<#2>=(\vertices[#1]<#2>,
\edges[#1]<#2>, \typeFunction[#1]<#2>)} %\distributionFunction[#1]<#2>,
% \triggerTransitions[#1]<#2>, \resetTransitions[#1]<#2>)}
\DeclareDocumentCommand{\labellingFunction}{O{} D<>{} D(){}}{\ell_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
% Attack Fault Trees - Semantics
%-----------------------------------------------------------------------------
\DeclareDocumentCommand{\type}{O{} D<>{} D(){}}{\mathsf{T}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\randomVariable}{O{} D<>{} D(){}}{\mathsf{X}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\val}{O{} D<>{} D(){}}{\mathsf{v}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\metric}{O{} D<>{} D(){}}{\mathsf{d}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\error}{O{} D<>{} D(){}}{\epsilon_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\prob}{O{} D<>{} D(){}}{\delta_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\interpretation}{O{} D<>{} D(){}D(){}}{\mathsf{I}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}\ifthenelse{\isempty{#4}}{}{(#4)}}
\DeclareDocumentCommand{\pac}{O{} D<>{} D||{} D(){}}{\mathsf{pac}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}\ifthenelse{\isempty{#4}}{}{(#4)}}
\DeclareDocumentCommand{\values}{O{} D<>{} D(){}}{\mathsf{val}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\valuesBE}{O{\basicEvents} D<>{} D(){}}{\mathsf{val}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\vector}{O{} D<>{} D(){}}{\avector{\alpha}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\matrix}{O{} D<>{} D(){}}{\ifstrequal{#1}{1}{\amatrix{A}}{\ifstrequal{#1}{2}{\amatrix{B}}{\amatrix{A}}}_{\ifstrequal{#1}{1}{}{\ifstrequal{#1}{2}{}{#1}}}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\aph}{O{} D<>{} D(){}}{\ensuremath{\mathsf{APH}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}}
\DeclareDocumentCommand{\setAPH}{O{} D<>{} D(){}}{\mathcal{APH}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\exampleAPH}{O{} D<>{} D(){}}{\aph[#1]<#2> = (\vector[#1]<#2>,\matrix[#1]<#2>)\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\norm}{m O{} D<>{}}{\left\lVert#1\right\rVert_{#2}^{#3}}
% Attack Defence Diagrams - Full
%-----------------------------------------------------------------------------
\DeclareDocumentCommand{\probabilityFunction}{O{} D<>{} D(){}}{\mathsf{Pr}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\costFunction}{O{} D<>{} D(){}}{\mathsf{Cost}_{E}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\distributionFunction}{O{} D<>{} D(){}}{\mathsf{Dist}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\costDelayFunction}{O{} D<>{} D(){}}{\mathsf{Cost}_{D}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\cost}{O{} D<>{} D(){}}{\mathsf{C}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\costVars}{O{} D<>{} D(){}}{\mathsf{CVars}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\bounds}{O{} D<>{} D(){}}{\mathcal{B}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\operatorCost}{O{} D<>{} D(){}}{\mathop{\mathsf{op}}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\totNumAttacks}{O{} D<>{} D(){}}{\mathsf{A}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\totNumBlocks}{O{} D<>{} D(){}}{\mathsf{B}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\frequency}{O{} D<>{} D(){}}{\mathsf{F}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
% Attack Defence Diagrams - Success Probability
%-----------------------------------------------------------------------------
\DeclareDocumentCommand{\successProbability}{O{} D<>{} D(){}}{\mathsf{V}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
% New Column Types for tabularx
%-----------------------------------------------------------------------------
\newcolumntype{L}[1]{>{\hsize=#1\hsize\raggedright\arraybackslash}X}%
\newcolumntype{R}[1]{>{\hsize=#1\hsize\raggedleft\arraybackslash}X}%
\newcolumntype{C}[1]{>{\hsize=#1\hsize\centering\arraybackslash}X}%
\newcolumntype{R}[2]{%
>{\adjustbox{angle=#1,lap=\width-(#2)}\bgroup}%
l%
<{\egroup}%
}
\DeclareDocumentCommand{\bijection}{O{} D<>{} D(){}}{\mathsf{bi}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\newcommand{\DAG}{\textsf{DAG}}
\newcommand{\Id}{\ensuremath{\mathop{\mathsf{Id}}}}
\newenvironment{mymatrix}%
{%
\begingroup % keep the change local
\setlength\arraycolsep{1ex}
\begin{bmatrix}
}%
{%
\end{bmatrix}
\endgroup
}%
\newcommand{\amatrix}[1]{\mathbf{#1}}
\newcommand{\avector}[1]{\boldsymbol{#1}}
\newcommand{\lastcol}[1]{\overline{#1}}
\newcommand{\fillit}[1]{\quad #1\quad}
\newcommand{\nodeAsText}[1]{
\resizebox{1em}{!}{
\begin{tikzpicture}[font={\footnotesize},yscale=0.25,xscale=0.19]
\node[BETrig, #1] at(0,0) {};
\end{tikzpicture}}
}
% Learning
%-----------------------------------------------------------------------------
\DeclareDocumentCommand{\trace}{O{} D<>{} D(){}}{\mathsf{tr}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\traces}{O{} D<>{} D(){}}{\mathsf{Tr}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\execution}{O{} D<>{} D(){}}{\mathsf{ex}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\executions}{O{} D<>{} D(){}}{\mathsf{Ex}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\valuation}{O{} D<>{} D(){}}{\mathsf{eval}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\sensitivity}{O{} D<>{} D(){}}{\mathsf{Sens}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\specificity}{O{} D<>{} D(){}}{\mathsf{Spec}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\ppv}{O{} D<>{} D(){}}{\mathsf{PPV}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\weight}{O{} D<>{} D(){}}{\mathsf{w}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\quantile}{O{} D<>{} D(){}}{\mathsf{q}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\fitness}{O{} D<>{} D(){}}{\mathsf{F}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\generations}{O{} D<>{} D(){}}{\mathsf{Gen}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\generationwidth}{O{} D<>{} D(){}}{\mathsf{GenW}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\mutationrate}{O{} D<>{} D(){}}{\mathsf{mutr}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\trainingrate}{O{} D<>{} D(){}}{\mathsf{trainr}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\actions}{O{} D<>{} D(){}}{\mathsf{Act}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\variableAlg}{m O{} D<>{} D(){}}{\mathsf{#1}_{#2}^{#3}\ifthenelse{\isempty{#4}}{}{(#4)}}
\DeclareDocumentCommand{\operator}{O{} D<>{} D(){}}{\mathsf{op}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\newcommand{\opname}[1]{\textsc{#1}}
\newcommand{\opSwitch}{\opname{switch}}
\newcommand{\opChange}{\opname{change}}
\newcommand{\opChangeS}{\opname{seqChange}}
\newcommand{\opAddIvr}{\opname{addNat}}
\newcommand{\opRemoveIvr}{\opname{removeNat}}
\newcommand{\opSwap}{\opname{swap}}
\newcommand{\labels}{\mathsf{L}}
\DeclareDocumentCommand{\labelfunction}{O{} D<>{} D(){}}{\mathsf{c}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\newcommand{\valuations}{\mathsf{K}}
\DeclareDocumentCommand{\signatureFunction}{O{} D<>{} D(){}}{\mathsf{s}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\newcommand{\crossoverfunction}{\mathsf{cv}}
\DeclareDocumentCommand{\randmod}{O{} D<>{} D(){}}{\mathsf{\epsilon}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\mean}{O{} D<>{} D(){}}{\mathsf{\mu}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
\DeclareDocumentCommand{\sd}{O{} D<>{} D(){}}{\mathsf{\sigma}_{#1}^{#2}\ifthenelse{\isempty{#3}}{}{(#3)}}
%pseudocode
\newcommand{\pool}{\mathsf{pool}}
\newcommand{\pearson}{r_{\mathit{Pearson}}}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% End:
\section{Introduction}
\label{sec:introduction}
\emph{Attack trees}, e.g., ~\cite{kordy2013,widel2019}, and their extensions are a widespread formalism for threat modeling and risk assessment. Their applications range from analyzing attacks on smart grids~\cite{beckers2014}, ATMs~\cite{fraile2016}, optical power meters~\cite{fila2019}, SCADA control systems~\cite{byres2004,mcqueen2006,ten2007,lopez2012,al2019} or software supply chains~\cite{ohm2020} to intelligent autonomous vehicles and vehicular networks~\cite{houmer2020,kim2020,roblesmodel}, secure deployment of HTTPS~\cite{soligo2020} or cybersecurity awareness trainings for election officials~\cite{schurmann2020}. Moreover, attack trees are particularly useful for meta-modeling threats, combining several risk analyses together, e.g., in telemedicine~\cite{kim2020b,ramos2020}, impersonation attacks in e-learning~\cite{rosmansyah2020} or IoT systems~\cite{krichen2019}. Besides these individual usages, attack trees are generally recommended as a means to identify the point of the weakest resistance according to the \emph{OWASP CISO AppSec Guide},\footnote{\url{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 \emph{Improving Common Security Risk Analysis} report~\cite{nato2008}.
In practice, there are not enough resources to fix every single vulnerability found in security assessment. Hence, the need to rank their importance arises. \emph{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.~\cite{kumar2015,hermanns2016,aslanyan2016,pekergin2016,kumar2017,kordy2018,eisentraut2019}, there are two main hindrances to practical use. Firstly, it is the very \textit{limited tool support} for convenient quantitative modeling and analysis. Secondly, it is the \textit{uncertainty and imprecision of the quantitative input} information, arising in this domain even more than elsewhere. Indeed, apart from standard questions like \emph{What is the actual failure rate of the security camera?}, we may need to ask \emph{What is the probability of guessing a password using a database of the most common passwords and one year of CPU time?} or \emph{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 \emph{tool}, which also features quantitative analysis capable of rigorously reflecting the \emph{uncertainty and imprecision of the quantitative inputs}. To this end, we formalize such models as \emph{\PAC{}-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 \PAC{}-input quantitative analysis we create a benchmark suite~\atbest{} of $\ADT$ found in literature and ones generated randomly. %\atbest{} consists of attack-defense tree models published in the last two decades as well ask randomly generated models.
We make all models available to the public.\footnote{For review, all models are in our artifact at \url{https://zenodo.org/records/11090469}.\label{fn:artifact}}
\para{Tool.} We provide~\quadtool{}, a tool for the whole modeling-analysis workflow. The tool can import trees in the \DOT{} format and \XML{} format of \adtool{}~\cite{gadyatskaya2016}. The graphical interface allows for convenient creating, editing, and combining trees and generating \PAC{}-quantities directly from provided data. Further, the tool translates the trees to formats of model checkers \UPPAAL{}~\cite{behrmann2006}, \prism{}~\cite{kwiatkowska2011}, \prismgames{}~\cite{chen2013}, \modest{}~\cite{hartmanns2014}, and \storm{}~\cite{dehnert2017} (via \jani{}~\cite{budde2017} export of \modest{}). Consequently, the GUI effectively interfaces with other available analyses (such as~\cite{gadyatskaya2016,ruijters2017}) and to our new \PAC{}-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.
\para{\PAC{}-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.
%We rather collect measurements of costs and probabilities.
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 \emph{probably approximately correct (\PAC{})}, i.e., with a given probability in a given interval around the estimate. We demonstrate how easily such trees can be obtained, relying on \emph{statistics} or \emph{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 \PAC{} uncertainty resulting from the input quantities' \PAC{} 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.
\medskip
To summarize, our contribution is threefold:
\begin{itemize}[noitemsep,nosep]
\item Our tool~\quadtool{} addresses practical needs in attack-defense tree modeling and analysis, including a GUI and a CLI for editing and analyzing \adt{}. It also gives feedback on suitable exports for further analyses.
% \begin{itemize}
% \item GUI editing of attack trees and a rich range of their extensions, interfacing analyzers together with helpful feedback,
% \item estimating quantities in the models from data and extending analyses to rigorously reflect the uncertainty in the resulting \PAC{} models (at almost no additional cost).
% \end{itemize}
\item The tool features a novel quantitative analysis of \PAC{}-attack-defense trees, the first extensions of attack-defense trees reflecting the data inaccuracy.
%\item an extension to the traditional bottom-up analyses to bound the final \PAC{} uncertainty resulting from the input quantities' \PAC{} uncertainty
\item The tool comes equipped with \emph{AT BEnchmark SuiTe} (\atbest{}), collecting benchmarks from literature as well as randomly generated ones.
\end{itemize}
\para{Organization.} The paper is organized as follows. After exemplifying the framework of attack-defense trees in \Fref{sec:attack-defense-trees}, the tool functionality is presented in
\Fref{sec:functionality}. We describe our \PAC{}-input analysis in \Fref{sec:pac}.
\Fref{sec:experiments} evaluates our contributions experimentally and \Fref{sec:conclusion} concludes. We provide an artifact with the tool and models\footref{fn:artifact}.
\medskip
\para{Related work.}
Besides two industrial tools dedicated to attack-defense tree analysis\footnote{see \url{http://www.amenaza.com} and \url{http://www.isograph.com/software/}}, which neither support more complex attack-defense tree structures such as~\cite{hermanns2016}, nor export to standard model checking tools, there are three dedicated (and up-to-date) \emph{quantitative} attack-defense tree analysis tools:
\begin{itemize}[nosep]
\item \adtool{}~\cite{gadyatskaya2016} 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, \adtool{} does not support \PAC{}-input analysis. Additionally, one cannot add \PAC{}-input analysis to \adtool{} as a `custom' domain since multi-parameter attack-defense trees are not supported. We compare the performance of the bottom-up analysis using \adtool{} and \quadtool{} in \Fref{sec:experiments}.
\item \attop{}~\cite{ruijters2017} is a software bridging tool, which provides various horizontal and vertical model transformations to the \adtool{}~2.0 input format or to the model checker UPPAAL, however not to \prism{} or \modest{}. \PAC{} models and \PAC{} analysis are not supported.
\item \risqflan{}\cite{ter2021quantitative} allows specifying attack-defense trees with quantitative constraints using a dedicated probabilistic language (XTEXT grammar)\footnote{While the XTEXT files get compiled to dot-files for graphical display, these are currently not entirely compatible with the \quadtool{} import.}. Statistical model checking and precise analysis using \storm{} and \prism{} are supported. However, \risqflan{} neither supports \PAC{}-inputs nor continuous-time. Additionally, exports to \storm{} and \prism{} rely on discrete-time Markov chains rather than games or stochastic timed automata. Stochastic model checking in \risqflan{} relies on \MultiVeStA{}\cite{sebastio2013multivesta}. Hence \risqflan{} does not allow synthesizing optimal attack and defense strategies. However, \risqflan{} allows assigning detection-rates to inner nodes and to separate defenses from countermeasures (which we do not feature). Hence, a complete performance comparision between \risqflan{} and \quadtool{} is not possible.
\end{itemize}
All these quantitative analyses have precise inputs and outputs (rather than \PAC{} 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 \PAC{} 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~\cite{buoni2010,mezei2011,pekergin2016}.
%For similar formalisms, most importantly fault trees~\cite{vesely1981}, uncertainty is limited to fuzzy approaches~\cite{ruijters2015}.
Buldas et al.~\cite{buldas2020} 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 \emph{impossibility of reflecting the data accuracy, which is the main contribution of this paper}.
In \cite{lopuhaa2022efficient} 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.
%%% Local Variables:
%%% mode: latex
%%% TeX-engine: xetex
%%% TeX-master: "main"
%%% End:
\section{Attack-Defense Trees}
\label{sec:attack-defense-trees}
In this section, we briefly recall the notion of \emph{attack-defense trees} (\adt), e.g.,~\cite{kordy2011,hermanns2016}. 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 \emph{basic events} (denoted $\basicEvents$), unique observable happenings in
the real world. They are partitioned into \emph{basic attack steps} and \emph{basic defense steps}.
\begin{definition}[Attack-Defense Trees~\cite{hermanns2016}]
\label{def:add}
An \emph{attack-defense tree}\footnote{In literature, \adt{} 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
\begin{itemize}
\item $\left (\vertices, \edges \right)$ is a \emph{directed acyclic graph}, with a designated \emph{goal} sink vertex~$\topGoal$ for the attacker. The source vertices $\basicEvents \subseteq \vertices$ are called \emph{basic events}. All other vertices, \mbox{$\gates \coloneqq \vertices \setminus \basicEvents$}, are called \emph{gates}; direct predecessors w.r.t. $(\vertices,\edges)$ of each gate are called its \emph{inputs}.
\item 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.
\item $\typeFunction{} \colon\ \gates \to \operators$ is the \emph{type function} assigning an operator to each gate.
\item $\triggerTransitions \subseteq \set{\vertex \in \gates \mid \typeFunction(\vertex) = \opTrigger} \times \basicEvents$ are \emph{trigger} edges from $\opTrigger$ gates to BE;
\item
$\resetTransitions \subseteq \set{\vertex \in \gates \mid \typeFunction(\vertex) = \opReset}\times \basicEvents$ are \emph{reset} edges from $\opReset$ gates to BE;
\end{itemize}
\end{definition}
\begin{figure*}[htbp]
\centering
\includegraphics[width=\textwidth]{toyexample.png}
\caption{The $\ADT{}$ from \cite{fila2019} represents ways to gain access to a power meter. We will use this model also in \Fref{sec:pacanalysis}. In \Fref{sec:experiments} we evaluate our tool on more complex attack-defense trees. }
\label{fig:toyexample}
\end{figure*}
%\begin{figure*}[htbp]
% \centerline{\includegraphics[width=0.75\linewidth]{case-study.png}}
% \caption{This attack tree represents how to gain access to an exemplary computer system. We use this toy model as a running example.
% %More complex examples found in the literature are provided at our benchmark suite \atbest{} (see \Fref{sec:atbest}).
% In \Fref{sec:experiments} we evaluate our tool on more complex attack-defense trees. \todo{replace with clean image}}
% \label{fig:case_study}
%\end{figure*}
%\begin{example}
% \label{ex:runningexample}
% In \Fref{fig:case_study}, we present a small attack tree representing an attacker who wants to maliciously gain access to a computer system. The goal node (with a blue border) represents the overall attack goal. All leaves of the tree are basic attack steps (colored red).
%The goal is refined into different subtrees using the operator~$\opOr$, i.e., only one of the subtrees need to be successfully attempted for the overall attack to be successful. The overall attack is successful if, for instance, the victim forgets to lock itself out of the target computer (event~(2)). Two further subtrees are refined using the operator~$\opAnd$ (events~(6) and~(10)). To successfully attempt the subtree rooted in event~(6), the attacker needs to get the PIN (event~(4)) and steal the victim's phone~(event~(5)) to use the smart login function of the target computer.\qee
%\end{example}
\begin{example}
\label{ex:toyexample}
In \Fref{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.%\qee
\end{example}
%The semantics of the trees is as follows. The players may \emph{attempt} their basic events \emph{successfully} or
%\emph{unsuccessfully} (or not at all). Further, the operators define how the successful attempt of a basic event is propagated (bottom-up) through the tree. For instance, the operators~$\opAnd$ and $\opOr$ propagate successful attempts like their logical equivalents: $\opAnd$ propagates successful attempts if all its children are successfully attempted (independently of the order). $\opOr$ propagates a successful attempt if at least one child is successfully attempted.
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.
%Specifically, for $\opSand$ to be successfully attempted, all its children need to be attempted successfully in order (from left to right).
Further, for Trigger~$\opTrigger$, suppose its child is successfully attempted. In that case, several basic events are activated (\emph{triggered}) for attempting (they cannot be attempted earlier than this).
%We say that these basic events are \emph{triggered}, meaning they can be attempted from now on.
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 \Fref{def:powerset} in the Appendix. Formal semantics for the remaining operators are not necessary to follow the paper (They can be found in~\cite{arnold2014,hermanns2016,eisentraut2019}).
%
%Formally, we define attack-defense trees as follows. The set of basic events $\basicEvents \coloneqq \basicEvents[\attacker] \disjointUnion \basicEvents[\defender]$ is partitioned into those belonging to the $\attacker$ttacker and to the $\defender$efender.
% Please note the following differences to other attack-defense tree definitions:
% \begin{itemize}
% \item Vertices (except basic events) are not assigned players (as it is done, for instance, in~\cite{mauw2005,kordy2011}). Thus, we use the operator~$\opNeg$ to include defense mechanisms rather than player swapping and strictly separate events controlled by the defender from countermeasures. Hence, the defender's actions can also be profitable for the attacker, and the attacker's actions can also prevent an attack.
% \item Trigger and reset edges are not part of the set of edges~$\edges$. We only require $(\vertices,\edges)$ to be acyclic (together with trigger edges and reset edges, this does not need to be the case).
% \item In contrast to~\cite{hermanns2016}, we leave out time-driven events (although our tool~\quadtool{} supports them).
% \end{itemize}
%%% Local Variables:
%%% mode: latex
%%% TeX-engine: xetex
%%% TeX-master: "main"
%%% End:
\section{Tool Overview}
\label{sec:functionality}
This section shows the usage of $\quadtool{}$ both in a graphical user interface and direct command-line access. We evaluate our analyses in \Fref{sec:experiments}.
\begin{figure*}[t]
\centering
\makebox[\linewidth]{
\begin{tikzpicture}[auto,node distance=8mm,>=latex,font=\footnotesize]
\node[cost] (s3) {construct or \nodepart{two} import model};
\node[cost,right=7mm of s3] (s4) {use default values or
\nodepart{two} add values from various sources};
\node[cost,right=5mm of s4] (s5) {export to
model checker \nodepart{two} for further analyses};
\node[cost,above=8mm of s4] (s6) {exact or \PAC{}-analysis
\nodepart{two} in tool for costs, delays, probabilities};
\node[above left=3mm and 5mm of s3] (s0) {\DOT{}};
\node[above left=-4mm and 5mm of s3] (s1) {\XML{}};
\node[below left=-4mm and 5mm of s3] (s2) {\formatstandard{GUI}};
\node[below left=3mm and 5mm of s3] (s21) {\atbest{}};
\node[below left=6mm and -10mm of s4] (s11) {iid samples};
\node[below=6mm of s4] (s12) {time series};
\node[below right=6mm and -10mm of s4] (s13) {expert estimates};
\node[above right=0mm and 5mm of s5] (s8) {\prism{}};
\node[right=5mm of s5] (s9) {\modest{}};
\node[below right=0mm and 5mm of s5] (s10) {\UPPAAL{}};
\draw[->] (s5) to node[midway,above,sloped]{} (s8);
\draw[->] (s5) to node[midway,above,sloped]{} (s9);
\draw[->] (s5) to node[midway,below,sloped]{} (s10);
\draw[->] (s0) to node[midway,above,sloped]{} (s3);
\draw[->] (s1) to node[midway,above,sloped]{} (s3);
\draw[->] (s2) to node[midway,below,sloped]{} (s3);
\draw[->] (s21) to node[midway,below,sloped]{} (s3);
\draw[->] (s3) to node[midway,above,sloped]{} (s4);
\draw[->] (s4) to node[midway,above,sloped]{} (s5);
\draw[->] (s4) to node[midway,above,sloped]{} (s6);
\draw[->,dashed] (s6) to node[above left]{refine} (s3);
\draw[->] (s11) to node[midway,above,sloped]{} (s4);
\draw[->] (s12) to node[midway,above,sloped]{} (s4);
\draw[->] (s13) to node[midway,above,sloped]{} (s4);
\end{tikzpicture}
}%End Makebox
\caption{The Workflow with \quadtool{} 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. }
\label{fig:quadtool}
\vspace*{-2.5em}%Figure and subsection add up unneseccary space
\end{figure*}
\subsection{Model Construction}
The workflow using $\quadtool{}$ (see \Fref{fig:quadtool}) starts with
model construction. For convenient modeling, $\quadtool{}$ supports a
dedicated graphical user interface and the following two input
formats:
\begin{itemize}
\item The \DOT{}-format as described in the Graphviz-Tool~\cite{Gansner93atechnique}. We recommend this format as it supports storing all additional parameters like \PAC{}-parameters and simple formatting.
\item The \XML{}-format used in \adtool{}~\cite{gadyatskaya2016}. To ensure compatibility with this tool, our tool only exports strict tree structured $\ADT$ without \PAC{}-values to this format.
\end{itemize}
Our \emph{GUI}, see \Fref{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~\cite{widel2019} for a survey on quantitative attack-defense tree analysis). Hence, $\quadtool{}$ comes with an integrated \emph{feedback system}~(see \Fref{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.
\subsection{\atbest{} Benchmark Collection for Attack-Defense Trees}
\label{sec:atbest}
To support the standardization and benchmark collection among attack-defense tree researchers and practitioners, we bring forth an attack-tree {benchmark collection} \emph{AT BEnchmark SuiTe} (\atbest{}) accessible at~\atbestURL{}. 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,~\cite{mauw2005,ten2007,kordy2011,kordy2013,beckers2014,kumar2015,aslanyan2016,pekergin2016,fraile2016,gadyatskaya2016,hermanns2016,kumar2017,ruijters2017,kordy2018,andre2019,fila2019,krichen2019,rosmansyah2020,buldas2020,houmer2020,kim2020b,ohm2020,schurmann2020,roblesmodel}, which we constructed using \quadtool{}. Additionally, we generated 626 models of various sizes for performance testing. These are binary \adt{} using the gates $\opAnd$ and $\opOr$, created by combining two smaller models with a new root recurrently.
\subsection{Obtaining \PAC{}-Quantities for Attack-Defense Trees}
\label{sec:getpacqadt}
After creating a model, we add default values or estimates to basic events (second step in the workflow (see \Fref{fig:quadtool})). Our \PAC{} (s. \Fref{sec:pac}) assumption is less restrictive than the standard assumption of exact quantities and already applicable to various examples.
%Unfortunately, most real safety- and security-relevant data sets might reveal high-confidential business secrets. Thus, they are not publicly available. Therefore, we illustrate the usage in a more general example. \todo{other toy example}
%\begin{example}[\PAC{}-Quantities for Basic Events]
% We use a crime statistics from the UK \cite{CrimedataUK20} to generate the probability for the event \emph{steal phone}~(see \Fref{fig:case_study}) to take place. The data contains the number of individuals impacted by phone theft (according to police reports) and an estimate of the total individual phone owners in the area. Having this data, we can calculate the probability for a single individual to be a victim of phone theft. % It is only an estimate for the particular basic event, as it is not the probability of a particular phone being successfully stolen. \todo{Should I add: It captures the probability of an individual being chosen for theft and the successful execution}
%\end{example}
To derive \PAC{}-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 (\formatnames{ARIMA}) model~\cite{arimacovid,arimaelectricity,arimafinance,arimapacarticle,arimarental,hughes2010} inside the tool to derive bounds for cases with time-series data.
%
%\begin{example}[\PAC{}-Quantities for Basic Event (Continued)]
% In our example, it is impossible to see the samples as independent as they were drawn from the same population and may influence each other, e.g., a year with high crime rates may lead to more police activity and, therefore, influence the following year. Therefore, an \formatnames{ARIMA} model may better represent the situation, as the data points stem from equally long periods of time.
%\end{example}
%
%Both options -- Gaussian estimates and \formatnames{ARIMA} -- are integrated and directly accessible in $\quadtool$ using a library~\cite{JavaTimeseries19} for automated time-series analysis. It checks every parameter permutations for an \formatnames{ARIMA} model and chooses the version with the lowest Akaike information criterion. \cite{Akaike74} proposed this parameter to allow relative comparability between multiple models in terms of the prediction error (minimizing the prediction error).
%\begin{example}[\PAC{}-Quantities for Basic Event (Continued)]
% Using the time series data from 2009 to 2018 for stolen phones, our analysis using the ARIMA-model returns the estimate of 0.72\% with $\epsilon=0.19\%$ given $\delta=5\%$. The true value 0.69\% for the second half of 2018 until the first half of 2019 lies in these bounds. We ignored the latest data, including the first half of 2020, due to the Corona pandemic.
%\end{example}
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.
\subsection{Analyses}
\label{sec:pacanalysis}
\quadtool{} allows to analyze models using an exact or \PAC{} analysis or using existing model checkers. %A graphical overview can be found in \Fref{tab:overview}.
Like the \adtool{}, $\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 \PAC{}-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: \XML{}, \DOT{}, \prism{}-, \modest{}-, \UPPAAL{}-input-language. For \prism{}, we use the semantics in terms of stochastic turn-based games given in~\cite{eisentraut2019} and for
\modest{} and \UPPAAL{} the semantics in terms of stochastic timed automata given in~\cite{hermanns2016}. \footnote{To use \storm{}, we suggest using the export to \modest{} first and then, use their export to the \jani{}-format.} In the following, we describe the interfaces to other tools and their use in more detail.
\para{Connection to \adtool{} and \attop} These two attack-defense tree tools have a restricted set of features and expect \XML{} inputs. Thus, we cannot analyze every attack-defense tree constructed in \quadtool{} using these tools. For instance, whenever a model has multiple root nodes, our export omits all but one tree. Furthermore, the \adtool{} only supports the operators $\opOr$, $\opAnd$, $\opSand$ and no timed events (with clocks or distributions). % In the current development version (2.2.2)., $\opSand$ trees do not have a domain for minimum costs and success probability; fortunately, we could add custom domains to fill this gap.
\para{Timed Analysis} Analysis involving time can be either done within $\quadtool{}$ or outsourced to \modest{} or \UPPAAL{}.
The translation to \modest{} uses actions for each three-valued logic state, i.e., each basic event can either be undecided, successfully or unsuccessfully attempted. For \UPPAAL{} a similar approach with automata for every state is used. Both approaches can model systems with multiple root nodes and complex operators.
% The strong point of \modest{} lies in basic events that are controlled by time via sampling from a given distribution. While \UPPAAL{} worked in a reasonable amount of time even for large models (s. \Fref{sec:experiments}).
%
% A basic event signals all its successors being successfully attempted by the action \texttt{ttBEPlayerx} (where x is the id of the event). This approach makes it possible to model systems with multiple root nodes and complex operators. Additionally, we can include basic events controlled by time (rather than by players) by sampling from a given distribution. Since \modest{} can be converted to \jani{} and back by the \modest{} toolset~\cite{hahn2013}, all model checkers supporting \jani{} become also available.
%
%Another model checker supported by \quadtool{} is \UPPAAL{}. It has a graphical interface for modeling and simulation~\cite{david2015}. Due to a different synchronization mechanism in \UPPAAL{}, we save each event's value as integers rather than as states of the automaton.
%% Our translation connects all potential goal nodes to an automaton called \emph{Won}, which determines whether the attack is successful or failed. Thus,
% We automatically export the setup to calculate the overall success or failure probability of the attack-defense tree. %During export, our tool creates these two properties automatically.
% However, other custom properties can be added. With \UPPAAL{}, we were able to handle large models in a reasonable amount of time, as presented below. However, this approach does not support games.
\para{Game Analysis} Lastly, $\quadtool{}$ can also export to the \prism{} 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.
\para{Integration} We provide the functionality to send a model directly to \UPPAAL{}~cora, \adtool{}, \prismgames{} and \modest{}~simulator in the GUI, after specifying the Tool location, as seen in \Fref{fig:editor} (right lower panel).
\begin{figure*}[t]
\centerline{\includegraphics[height=6.5cm]{tool.png}}
\caption{$\quadtool$ with the case study from~\cite{fila2019}. 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 \PAC{}-quantities. Below is the result of a model checker (here \adtool{}).}
\label{fig:editor}
\end{figure*}
% \subsection{Comparison of Different Analysis Methods}
% Finally, we use our running example from \Fref{fig:case_study} to discuss different analysis options available by means of an example. % Our running example represents various attacks to gain access to a computer system.
% % Possible attack vectors comprise access to a user's phone and the corresponding pin to use a smart login system. Another option is to wait for the victim to forget logging out of the system. Additionally, one might either find a post-it with the login data or blackmail the user into revealing them. Furthermore, the attacker may use the same train as the target and watch them entering their credentials.
% \begin{itemize}
% \item The export to the \XML{}-format is feasible for this model as it is indeed a tree. If there were countermeasures like \emph{change password}, the export includes them as well. However, additionally including timed events like \emph{wait for server downtime} is not possible.
% % MODEST
% \item Our export to \modest{} has problems with the above model, as it only consists of player-events. \modest{} does not efficiently handle this kind of non-determinism in exact model checking. Additionally, \modest{} does not support this kind of non-determinism in statistical model checking~\cite{bogdoll2012b,hahn2014}. To make the model suitable for \modest{}, one could abstract from player actions using timed basic events. Besides this point, it could be a good choice for models of this structure.
% \item As the model only contains events triggered by a single player \UPPAAL{} is a good fit for this model.
% \item Lastly, \prism{} is the best fit for models that strongly rely on the game characteristics of an \adt{}. On a technical level, the export to \prism{} is available for our case study since it contains no reset nodes. Since we explicitly build the whole game, this export is very inefficient and only supports small trees. We recommend it only for small trees with not more than 30 vertices.
% \end{itemize}
%\begin{table*}[ht!]
% \centering
% \caption{Different Approaches to Attack Defense Tree Analysis
% Support Different Analysis Approaches.}
% \label{tab:overview}
% \begin{tabularx}{6.1in}{|L{8}|C{2}|C{2}|C{2.5}|C{1.5}|C{1.5}|C{2}|C{2}|C{2}|C{4}|C{2.5}|C{2.5}|C{2.5}|}
% \toprule
% & $\opAnd$ & $\opOr$ & $\opSand$ & $\opTrigger$ & $\opReset$ &
% $\opNeg$ & $\opIvr$ & $\opCost$ & 2-player & time & cost & \PAC{} \\
%
% \midrule
% \highlight{modeling with \quadtool{}} & \checkmark & \checkmark & \checkmark &
% \checkmark & \checkmark & \checkmark & \checkmark & \checkmark &
% \checkmark & \checkmark & \checkmark & \checkmark \\
%
% \midrule
%
% \highlight{translation to} &&&&&&&&&&&&\\
%
% \modest{} & \checkmark & \checkmark & \checkmark & \checkmark &
% \checkmark & \checkmark & \checkmark & \checkmark & (\checkmark)
% & \checkmark & \checkmark & \texttimes \\
%
% \UPPAAL{} & \checkmark & \checkmark & \checkmark & \checkmark &
% \checkmark & \checkmark & \checkmark & \checkmark & (\checkmark)
% & (\checkmark) & \texttimes & \texttimes\\
%
% \prism{} & \checkmark & \checkmark & \checkmark & \checkmark &
% \texttimes & \checkmark & \checkmark & \texttimes & \checkmark
% & \texttimes & \checkmark & \texttimes\\
%
% \XML{} for \adtool{} & \checkmark & \checkmark & \texttimes &
% \texttimes & \texttimes & \checkmark & \texttimes &\texttimes
% & \checkmark & \checkmark & \checkmark & \texttimes\\
%
% \midrule
% \highlight{analysis on tree} &&&&&&&&&&&&\\
%
% probabilities & \checkmark & \checkmark & \texttimes &
% \checkmark & \texttimes & \checkmark & \texttimes &
% \texttimes & \checkmark & \texttimes & \texttimes & \checkmark\\
%
% delay & \checkmark & \checkmark & \texttimes &
% \checkmark & \texttimes & \checkmark & \texttimes &
% \texttimes & \texttimes & \checkmark & \texttimes & \checkmark\\
%
% cost & \checkmark & \checkmark & \texttimes &
% \checkmark & \texttimes & \checkmark & \texttimes &
% \texttimes & \texttimes & \texttimes & \checkmark & \checkmark\\
%
% \midrule
% \highlight{dedicated game analysis}&&&&&&&&&&&&\\
%
% probabities exact &\checkmark & \checkmark & \checkmark &
% \checkmark & \texttimes & \checkmark & \checkmark & \texttimes &
% \checkmark & \texttimes & \checkmark & \texttimes \\
% \bottomrule
% \end{tabularx}
%\end{table*}
%%% Local Variables:
%%% mode: latex
%%% TeX-engine: xetex
%%% TeX-master: "main"
%%% End:
\section{\PAC{}-Quantitative \adt{}: Fighting the Uncertainty}
\label{sec:pac}
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~\cite{mauw2005,kordy2011,arnold2014,jhawar2015}. In this section, we augment this analysis to bound the uncertainty resulting from estimating the quantitative values of the basic events.
In \Fref{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~\cite{mauw2005,kordy2011,gadyatskaya2016}. However, standard
bottom-up traversal algorithms are efficient and correct only on
simpler structures than our \adt{} in \Fref{def:add} (for more
details, see~\cite{kordy2018}). In particular, they require a
\emph{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
\adtool{} (attack-defense trees with gates $\opAnd$, $\opOr$ and
$\opNeg$). For reader's convenience, we exclude $\opTrigger$ in this
section but include it in \Fref{app:correctness}. Hence, our analysis also covers
the second domain of the \adtool{}.
\subsection{Quantitative \adt{} and \PAC{}-Quantitative \adt{}}
\para{Quantitative \adt{}.} Given a type $\type$ of the quantitative information, the quantitative \adt{} is an \adt{} equipped with a \emph{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~\cite{gadyatskaya2016}, acylic phase-type distributions may, for instance, represent the likelihood of a successful attack over time~\cite{arnold2014}.
\begin{example}[Type]
For success probabilities, we simply take $\type=[0,1]$. For costs and delays, we take $\type=\RR_{\geq 0}$.
\end{example}
\para{\PAC{}-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 \emph{probably approximately correct} (\PAC{}), if there is an \emph{imprecision bound} $\error$ and an \emph{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:
\begin{definition}[\PAC]
Let $\type$ be a set equipped with a metric~$\metric$. We say that a $\type$-valued random variable $X$ is $(\error,\prob)$-\PAC{} for the true value~$\val$ if the probability\footnote{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)$-\PAC{}.
\end{definition}
\begin{example}[Metric]
For probabilities, costs, and delays, the metric is the standard Euclidean distance (absolute value of their difference).
\end{example}
\para{\PAC{}-Quantitative \adt{}} Given a type $\type$ of the quantitative information, the \PAC{}-quantitative \adt{} is a quantitative \adt{} equipped additionally with \emph{\PAC{}-parameters} $\error[\basicEvent] \in \RR_{\geq 0}$ and $\prob[\basicEvent] \in [0,1]$ for each basic event $\basicEvent\in\basicEvents$.
%\begin{figure*}[!t]
% \normalsize
% \begin{align*}
% \refstepcounter{equation}
% \values(\vertex) = \begin{cases}
% \valuesBE(\vertex) & \text{if $\vertex \in \basicEvents$, and $\vertex$ is non-triggerable.} \\
% f(\values(\inp[1]), \ldots, \values(\inp[n])) &
% \begin{tabular}[t]{@{}l@{}}
% if $\vertex$ is an inner node with operator $\operator$ \\
% and input nodes $\inp[1]$ to $\inp[n]$, and $f = \interpretation(\operator)$.
% \end{tabular}
% \end{cases}
% \end{align*}
% \caption*{Equation \theequation: Valuation of vertices in an \adt{}}
% \label{eq:valuesBE}
%\end{figure*}
%\subsection{Quantitative Bottom-Up Analyses}
%Before giving the generic algorithm for the bottom-up propagation of quantitative values~\cite{mauw2005,kordy2011}, we summarize the following building blocks it relies on:
%
%\begin{itemize}
%\item The algorithm is parametric in the \emph{domain} $\type$ of the quantitative information.
%\item All basic events of an \adt{} need to be given values from $\type$ in order to start the bottom-up propagation. We thus assume a \emph{basic-event valuation} function $\valuesBE: \basicEvents \to \type$ to be given as the input to the procedure.
%\item The algorithm is also parametric in the \emph{interpretation}~$\interpretation$, which maps the \adt{}-operators to operations over $\type$, so that we know how to propagate the values, i.e., $\interpretation(\operator) \in \type<n> \to \type$ for $\operator \in \set{\opNeg, \opAnd, \opOr}$, where $n$ is the arity of $\operator$.
% % \item $\interpretation(\basicEvent) \in\type<2> \to \type$ for triggerable basic events $\basicEvent \in \basicEvents$ allows for reflecting the value of the triggering event into the final value of the trigerable basic event.
% % \end{itemize}
%\end{itemize}
%
%% For technical clarity, we consider only the operators $\opAnd$, $\opOr$, $\opTrigger$, and $\opNeg$ and binary operators in the following.
%
%\para{Bottom-Up Traversal Analysis} Let $\ADT$ be an attack-defense tree with set $\vertices$ of nodes, $\topGoal$ its root, $\type$ a non-empty domain, $\interpretation$ an interpretation, and $\valuesBE$ a basic-events valuation. Then its bottom-up traversal semantics $\values \colon \vertices \to \type$ for $\ADT$ is defined recursively as in Equation 1. The valuation of $\ADT{}$ is defined as the value of its root node $\values(\topGoal)$.
%
%\begin{example}[Probabilistic \adt{}] \label{def:prob} 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:
% \begin{itemize}
% \item
% $\displaystyle{\interpretation(\vertex) (x_1,x_2)= x_1 \cdot x_2}$, if % $\vertex$ is a triggerable basic event \emph{or}
% $\typeFunction(\vertex)=\opAnd$
% \item
% $\displaystyle{\interpretation(\vertex)(x_1,x_2)= x_1 + x_2 - x_1 \cdot x_2}$ for $\typeFunction(\vertex)=\opOr$
% \item $\displaystyle{\interpretation(\opNeg)(x)=1-x}$
% \end{itemize}
%\end{example}
%
%Similar examples for the domain of Cost and Probability can be found in \Fref{app:examplesBottomUp}
%\begin{example}[Valuations for Probabilities, Costs, and Delays]
% The algorithm in \Fref{eq:valuesBE} together with the interpretation in the previous example yield the probability bottom-up traversal semantics, denoted by $\val<\probabilityFunction>$. We denote the minimal cost bottom-up traversal semantics by $\val<\costFunction,\min>$ and the maximal cost bottom-up traversal semantics by $\val<\costFunction,\max>$. We denote the minimal delay bottom-up traversal semantics by $\val<\delayFunction,\min>$ and the maximal cost bottom-up traversal semantics by $\val<\delayFunction,\max>$
%\end{example}
\subsection{\PAC{}-Input Extension of Bottom-Up Analyses}
Before giving the generic algorithm for the bottom-up propagation of quantitative values~\cite{mauw2005,kordy2011}, we will give a short introduction to bottom-up analyses.
\para{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 \adt{}-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)$.
\begin{example}[Probabilistic \adt{}] \label{def:prob} 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 \Fref{app:examplesBottomUp})
\begin{itemize}
\item
$\displaystyle{\interpretation(\vertex) (x_1,x_2)= x_1 \cdot x_2}$, if % $\vertex$ is a triggerable basic event \emph{or}
$\typeFunction(\vertex)=\opAnd$
\item
$\displaystyle{\interpretation(\vertex)(x_1,x_2)= x_1 + x_2 - x_1 \cdot x_2}$ for $\typeFunction(\vertex)=\opOr$
\item $\displaystyle{\interpretation(\opNeg)(x)=1-x}$
\end{itemize}
\end{example}
\para{Extension to PAC-Values} In the following, we devise an algorithmic approach that allows us to derive a \PAC{}-aware variant from almost any bottom-up traversal analysis (according to its previous definition)\footnote{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 \emph{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]]$\footnote{For success probabilities, we set $x_i \pm \error[i] \coloneqq
[\max(0,x_i-\error[i]),\min(x_i+\error[i],1)]$}.
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 \PAC{}-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.
\para{\PAC{}-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])$-\PAC{}, the uncertainty of
\begin{enumerate}[label=(\subscript{R}{{\arabic*}}),itemindent=1em]
\item $1-x_i$ can be bound by $\error = \error[i]$.
\item $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]$.
\item $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]$
\item $\max(x_1,x_2)$ can be bound by $\error=\max(\error[1],\error[2])$
\item $\min(x_1,x_2)$ can be bound by $\error=\max(\error[1],\error[2])$
\end{enumerate}
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.
\medskip\noindent In summary, the result of each of the given operations is $(\error,\prob)$-\PAC{}. Furthermore, each constant~$c \in \RR$ is (0,0)-\PAC{}.
\begin{example}[PAC-Bounds Computation for Probabilities]
Let $\ADT$ be an attack-defense tree with set $\vertices$ of nodes, let $\values[\basicEvents]$ be a \PAC{} probability valuation for basic events, i.e., for every basic event~$\basicEvent \in \basicEvents$, it holds $\values[\basicEvents](\basicEvent)$ is $(\error[\basicEvent],\prob[\basicEvent])$-\PAC{} for some $\error[\basicEvent] \in \RR_{\geq 0}$ and $\prob[\basicEvent] \in [0,1]$. The uncertainty for $\vertex \in \vertices$ is computed as follows:
\begin{enumerate}
\item $\vertex \in \basicEvents$ and $\vertex$ is not triggerable: return $(\error[\basicEvent],\prob[\basicEvent])$.
% \item $\vertex \in \basicEvents$ and $\vertex$ is triggered by $\vertex<\prime>$: recursively compute $(\error[\vertex<\prime>],\prob[\vertex<\prime>])$. Use rule for multiplication, return $\error = \values(\vertex) \cdot \error[\vertex<\prime>] + \values(\vertex<\prime>) \cdot \error[\vertex] + \error[\vertex]\cdot\error[\vertex<\prime>]$ and $\prob = \prob[\vertex] \cdot \prob[\vertex<\prime>]$
\item $\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 \subscript{R}{2}, 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]]) $
\item $\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 \subscript{R}{3}, 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]]) $
\item $\typeFunction(\vertex)=\opNeg$ and $\inp$ is its input: recursively compute $(\error[\inp],\prob[\inp])$. Use rule \subscript{R}{1}, i.e., return $\error= \error[\inp]$ and $\prob = \prob[\inp]$
\end{enumerate}
\end{example}
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 \PAC~interval, is at most the computed $\delta$.
In \quadtool{}, we also provide \PAC{}-aware bottom-up analyses for delays and costs. The proof of correctness can be found in \Fref{app:pac}.
\begin{example}[Propagation of Uncertainty]
In practice, $\delta = 0.05$ or $\delta=0.01$ seem reasonably small uncertainty probabilities for meaningful \PAC{} data (since they are most commonly used significance criteria). As most examples from literature have less than 30 nodes (s. \Fref{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.
\end{example}
%
%\para{Propagation of Uncertainty}
%In practice, $\delta = 0.05$ or $\delta=0.01$ seem reasonably small uncertainty probabilities for meaningful \PAC{} data (since they are most commonly used significance criteria). Binary trees of depth~5 have $2^5-1 = 31$ nodes.\footnote{Most nodes from previously published papers in our benchmark collection~\atbest{} have less than 30 nodes.} Assuming that each of the 16 basic events has uncertainty $\delta=0.05$, the uncertainty probability at the each node
%\begin{itemize}
%\item in level~4 is $(1-(1-0.05)^2)=0.0975$,
%\item in level~3 is $(1-(1-0.0975)^2) \approx 0.19$ and
%\item in level~2 is $(1-(1-0.19)^2) \approx 0.34$.
%\end{itemize}
%
%So, at the root, the uncertainty probability is approximately $(1-(1-0.34)^2) \approx 0.56$, i.e., in less than half of the cases, the true value is covered by the interval we compute. In contrast, for $\delta = 0.01$, we have the uncertainty probability $\delta \approx 0.15$ at the root, i.e., in about 85\% of all cases, the real value is in our interval. These simplified examples show clearly the need for good estimates of quantitative data and uncertainty bounds since the uncertainty in the input data drastically changes the reliability of the result.
\begin{figure*}[t]
\centering
\begin{subfigure}{0.35\linewidth}
\begin{itemize}[label={}]
\item ID 10 $p: 0.4594491$
\item \begin{itemize}[label={}]
\item ID 19 $p: 0.9188982$
\item \begin{itemize}[label={}]
\item ID 4 $p: 0.92818$
\item \begin{itemize}[label={}]
\item ID 1 $p: 0.24$
\item ID 2 $p: 0.65$
\item ID 3 $p: 0.73$
\end{itemize}
\item ID 9 $p: 0.99$
\end{itemize}
\item ID 17 $p: 0.5$
\item \begin{itemize}[label={}]
\item ID 6 $p: 0.5$
\end{itemize}
\end{itemize}
\end{itemize}
\vspace{-1.5em}
\caption{}
\label{fig:subfigB}
\end{subfigure}
\begin{subfigure}{0.64\linewidth}
\begin{itemize}[label={}]
\item ID 10 $p: 0.456463\;\epsilon: 0.130461\;\delta: 0.226219$
\item \begin{itemize}[label={}]
\item ID 19 $p: 0.924015\;\epsilon: 0.193929\;\delta: 0.185494$
\item \begin{itemize}[label={}]
\item ID 4 $p: 0.930528\;\epsilon: 0.1894165\;\delta: 0.142625$
\item \begin{itemize}[label={}]
\item ID 1 $p: 0.233\;\epsilon: 0.026214\;\delta: 0.05$
\item ID 2 $p: 0.667\;\epsilon: 0.029225\;\delta: 0.05$
\item ID 3 $p: 0.728\;\epsilon: 0.027594\;\delta: 0.05$
\end{itemize}
\item ID 9 $p: 0.993\;\epsilon: 0.005170\;\delta: 0.05$
\end{itemize}
\item ID 17 $p: 0.494\;\epsilon: 0.031003\;\delta: 0.05$
\item \begin{itemize}[label={}]
\item ID 6 $p: 0.506\;\epsilon: 0.031003\;\delta: 0.05$
\end{itemize}
\end{itemize}
\end{itemize}
\vspace{-1.5em}
\caption{}
\label{fig:subfigC}
\end{subfigure}
\caption{Example evaluation of the model in \Fref{fig:toyexample} (a) without \PAC{} values and (b) with \PAC{}-values. The \PAC{}-values were generated by sampling from Bernoulli distributions parameterized by the exact value.}
\label{fig:examplevaluation}
\end{figure*}
\subsection{Analysis Example}
We use one of the models introduced by Fila and Widel in \cite{fila2019}(s. \Fref{fig:toyexample}) about manipulating a power meter as example for the analysis workflow with \PAC{} values.
We will use the domain of probability and assign each of the basic events a success probability from the paper (see \Fref{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 \Fref{fig:examplevaluation} (a)). To generate the \PAC{} 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 \PAC{} values using a Gaussian-Estimator.
The propagated values are displayed in \Fref{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 \PAC{}-propagation.
This extended analysis does, however, come with an increased computational effort, which still is inside acceptable bounds (see \Fref{sec:experiments}).
%%% Local Variables:
%%% mode: latex
%%% TeX-engine: xetex
%%% TeX-master: "main"
%%% End:
\section{Experiments}
\label{sec:experiments}
% First, we compare different analysis methods on a small example. Second,
We discuss the performance of~$\quadtool$ on our collection of benchmarks found on \atbest{}.
% \subsection{Performance}
For performance measurements, we used 42 security models, ranging from 5 to 30 nodes, from existing literature (s. \Fref{sec:atbest}), allowing the whole operator set. 17 of them contained operators, that were incompatible with \XML{}. Therefore, they were only used for the remaining formats. We executed the conversion 50 times each on a computer with Intel\textregistered Core\texttrademark i7 processor and 16 GB RAM.
% \begin{figure*}[htbp]
% \centerline{\includegraphics[width=5in]{toolperformance.png}}
% \caption{Model checking times for success-probability on the model checkers \adtool{} and \UPPAAL{}-SMC.}
% \label{fig:tools}
% \end{figure*}
\begin{figure*}[t]
\vspace*{-1em}
\centerline{\includegraphics[width=\textwidth]{Evaluation_times.png}}
\caption{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 \atbest{} contain mostly player nodes, our timed analysis using \modest{} returns stack overflow errors on models of $size \geq 5$. \prismgames{} runtime seems to be more dependent on model composition, rather than just the size. The evaluation time for \quadtool{}, \adtool{} and \UPPAAL{} Cora are all below 1 second.}
\label{fig:tooleval}
\vspace*{-1em}
\end{figure*}
\begin{figure*}[t]
\centerline{\includegraphics[width=\textwidth]{scatterplot_pacNopac.png}}
\caption{Model checking times (mean per size) \PAC{} (red triangles) vs. non-\PAC{} (blue dots) models in \quadtool. The highest execution time was 1.2s for 1355 nodes. }
\label{fig:toolspac}
\vspace*{-1em}
\end{figure*}
%\para{Setup.}
In the next step, we conducted experiments on how long the model checkers \adtool{}, \UPPAAL{}, \prismgames{} and \modest{} need to analyze the \adt{} success and failure probability on the models previously used for conversion. Every execution was repeated five times.
Lastly, we compare the execution time of \PAC{} 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 \PAC{} values.
%\newcommand{\specialcell}[2][c]{%
% \begin{tabular}[#1]{@{}c@{}}#2\end{tabular}}
% \begin{table*}
% \centering
% \caption{\label{tab:table-name}Performance measures for the supported formats. The maximum nodes may depend on the complexity of the model.}
% \begin{tabular}{|c c c c c|}
% \toprule
% \highlight{Format} & \specialcell{Conversion time\\13 nodes (ms)} & \specialcell{Nodes\\(conversion)} & \specialcell{Nodes\\(handling)} & Benefits \\ [0.5ex]
% \midrule\hline
% \prism{} & 759 (\textpm550) & \textasciitilde 30 & \textasciitilde 30 & 2-Player games \\
% \midrule
% \modest{} & 161 (\textpm36) & >1100 & \textasciitilde 10 & timed events, all operators \\
% \midrule
% \UPPAAL{} & 202 (\textpm37) & >1100 & >1100 &large models, player driven \\
% \midrule
% \XML{} & 171 (\textpm13) & >1100 & >1100 & tree structure \\ [1ex]
% \bottomrule
% \end{tabular}
% \end{table*}
\para{Results} are depicted in \Fref{fig:tooleval} and \ref{fig:toolspac}. Our experiments show the following:
\begin{itemize}
% \item The models we collected for our benchmark~\atbest{} tend to be larger
% than 5 nodes but smaller than 30 nodes.
\item Exports to the model checkers
\UPPAAL{}, \modest{}, \prism{} and to the \XML{} format are
feasible for models of sizes commonly found in literature. With all except \prism{} needing less then a second for each model (see \Fref{app:conversionTimes}).
\item Generating the stochastic game explicitly, which the
translation to \prism{} relies on, is time-consuming for models
with more than~30 nodes (see \Fref{app:conversionTimes}). Yet, verification using \prism{} may
still be of use in practice.
\item The execution time may depend more on the model composition
than on the actual size of the underlying tree (see
\Fref{fig:tooleval}, \ref{fig:toolspac}).
\item Verification using the \adtool{} and \UPPAAL{} is faster than using \prismgames{} or \modest{}. If evaluation is possible, the results are returned in less then ten seconds (see \Fref{fig:tooleval}).
\item \UPPAAL{} model checking is useful for more complex objectives, posing an appropriate trade off. % The worst case in \prismgames{} took about 46 minutes which is a reasonable effort considering the beneficial setup for games.
\item For \PAC{} vs.\ non-\PAC{} analysis in \quadtool, the slope of runtime differs roughly by a factor 10. None of the approaches takes more than a few seconds (see \Fref{fig:toolspac}) even for attack-defense trees with more than 1000~vertices.
\item The runtime of \adtool{} and \quadtool{} using bottom-up analysis are in the same order in our experiments (see \Fref{fig:tooleval}).
\end{itemize}
% All results are summarized in \Fref{tab:table-name}.
%%% Local Variables:
%%% mode: latex
%%% TeX-engine: xetex
%%% TeX-master: "main"
%%% End:
\section{Conclusion and Future Work}\label{sec:conclusion}
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 \emph{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, \quadtool{} presents several steps making the $\ADT{}$ framework more applicable in practice.
\para{Future Work.} %There are several ways to be explored to improve the scalability of the analyses.
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.
%
%Finally, the support for modeling could also be improved, for instance, by importing log files of attacks and applying existing approaches to AT learning, thus automatically producing AT models from previous experience.
\para{Acknowledgments.} We want to thank everyone who has contributed case studies to our benchmark collection \atbest{} so far.
This research was funded in part by the German Research Foundation (DFG) project No.~427755713 \emph{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.
%%% Local Variables:
%%% mode: latex
%%% TeX-engine: xetex
%%% TeX-master: "main"
%%% End:
\pagebreak
\section{Quantitative Bottom-Up Analyses for Cost and Delays}
\label{app:examplesBottomUp}
\begin{example}[Delay \adt{}]
\label{def: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
\begin{itemize}
\item
$\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 % $\vertex$ is a triggerable basic event \emph{or}
$\typeFunction(\vertex)=\opAnd$.
\item
$\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$
\item $\displaystyle{\interpretation(\opNeg)(x_1,x_2)=(x_2,x_1)}$
% \item $\displaystyle{\interpretation(\opTrigger)=\Id}$
\end{itemize}
\end{example}
\begin{example}[Cost \adt{}]
\label{def: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.
\begin{itemize}
\item
$\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 % $\vertex$ is a triggerable basic event \emph{or}
if $\typeFunction(\vertex)=\opAnd$
\item
$\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$
\item $\displaystyle{\interpretation(\opNeg)(x_1,x_2)=(x_2,x_1)}$
% \item $\displaystyle{\interpretation(\opTrigger)=\Id}$
\end{itemize}
\end{example}
\section{Conversion Times}
\label{app:conversionTimes}
\begin{figure*}[htbp]
\centerline{\includegraphics[width=\linewidth]{totalfigure.png}}
\caption{Execution times for conversion of \DOT{}-files to the other formats.}
\label{fig:conversion}
\end{figure*}
\section{Correctness of Bottom-Up Traversal Semantics}
\label{app:correctness}
The following section recalls definitions from~\cite{kordy2011} and
adapts them to our attack-defense tree setting. \emph{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~\cite{kordy2011}, we allow
$\opTrigger$ as a restricted variant of $\opSand$\footnote{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 \emph{controlling} an event rather than whether an event
is \emph{useful} or \emph{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~\cite{mauw2005,kordy2011} to a
powerset semantics.
\begin{definition}[Extension of Example~5 -~7]
In each case, $\interpretation(\opTrigger) = \Id$ and
$\interpretation(\basicEvent) = \interpretation(\opAnd)$ for
triggerable basic events $\basicEvent \in \basicEvents$.
\end{definition}
\noindent 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}$.
\begin{definition}[Powerset Attack-Defense Trees]
\label{def:powerset}
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}}$.
\begin{itemize}
\item
$\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 \emph{or} $\typeFunction(\vertex)=\opAnd$
\item
$\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$
\item $\displaystyle{\interpretation(\opNeg)((X_1,X_2))=(X_2,X_1)}$
\item $\displaystyle{\interpretation(\opTrigger)=\Id}$
\end{itemize}
We denote the powerset bottom-up traversal semantics by~$\values<P>$.
\end{definition}
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.
\begin{definition}[Boolean Attack-Defense Trees]
\label{def:boolean}
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
$\type=\set{\true,\false}$
\begin{itemize}
\item
$\displaystyle{\interpretation(\vertex) (x_1,x_2)= \land
}$, if $\vertex$ is a triggerable basic event \emph{or}
$\typeFunction(\vertex)=\opAnd$
\item $\displaystyle{\interpretation(\vertex)=\lor}$ for
$\typeFunction(\vertex)=\opOr$
\item $\displaystyle{\interpretation(\opNeg)=\neg}$
\item $\displaystyle{\interpretation(\opTrigger)=\Id}$
\end{itemize}
We denote the Boolean bottom-up traversal semantics by~$\values<B>$.
\end{definition}
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.
\begin{theorem}[Powerset and Boolean Attack-Defense Trees]
\label{theo:correctness}
Let $\exampleADD$ be an attack-defense tree and let
$\values<P>(\vertex) = (X_1,X_2)$.
\begin{enumerate}
\item $x_1 \in X_1$ iff $\values<B>(\vertex)=\true$
w.r.t. $\values[\basicEvents,x_1]<B>$
\item $x_2 \in X_2$ iff $\values<B>(\vertex)=\false$
w.r.t. $\values[\basicEvents,x_2]<B>$
\end{enumerate}
\end{theorem}
\begin{proof}
Let $\exampleADD$ be an attack-defense tree. We proof both claims
simultaneously by induction on the structure of the attack-defense
tree.
\begin{itemize}
\item $\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.
\item \emph{Induction Hypothesis:} For all subtrees of $\vertex$
rooted in $\vertex<\ast>$ holds:
\begin{enumerate}
\item $x_1 \in X_1$ iff $\values<B>(\vertex<\ast>)=\true$
w.r.t. $\values[\basicEvents,x_1]<B>$
\item $x_2 \in X_2$ iff $\values<B>(\vertex<\ast>)=\false$
w.r.t. $\values[\basicEvents,x_2]<B>$
\end{enumerate}
\item $\typeFunction(\vertex)=\opTrigger$: The claim holds by
induction hypothesis and the definitions of $\values<P>$ and
$\values<B>$ (identity function for vertices labelled by
$\opTrigger$).
\item $\vertex \in \basicEvents$ and triggered by
$\vertex<\ast> \in \vertices$. Let
$\values<P>(\vertex<\ast>)=(X_1^\ast,X_2^\ast)$. We have
$\values[\basicEvents]<P>(\vertex)=(\set{\set{\vertex}},\set{\emptyset})$
and
$\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.
\item $\typeFunction(\vertex)=\opAnd$: Analogously to the proof for
triggerable basic events. However, the induction hypothesis needs
to be used on both subtrees.
\item $\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.
\item $\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.
\end{itemize}
We have proven \Fref{theo:correctness} by induction.
\end{proof}
% \begin{theorem}[Minimal Assignments]
% \label{theo:minimal}
% Let $\exampleADD$ be an attack-defense tree and let
% $Y_1, Y_2 \subsetneq \basicEvents$. Let $\vertex \in \vertices$ and
% $\values<B>(\vertex)=\true$ w.r.t. $\values[\basicEvents|_{\vertex},Y_1]<B>$
% and $\values<B>(\vertex)= \false$
% w.r.t. $\values[\basicEvents|_{\vertex},Y_2]<B>$ . Additionally, let
% $(X_1,X_2)=\values<P>(\vertex)$.
% \begin{enumerate}
% \item If there exists no subset $Y_1^\ast \subsetneq Y_1|_{\vertex}$
% s.t. $\values<B>(\vertex)=\true$
% w.r.t. $\values[\basicEvents,Y_1^\ast]<B>$, then $Y_1 \in X_1$.
% \item If there exists no subset $Y_2^\ast \subsetneq Y_2|_{\vertex}$
% s.t. $\values<B>(\vertex)=\false$
% w.r.t. $\values[\basicEvents,Y_2^\ast]<B>$, then $Y_2 \in X_2$.
% \end{enumerate}
% \end{theorem}
% We call $Y$ such that there exists no subset
% $Y^\ast \subsetneq Y|_{\vertex}$ s.t. $\values<B>(\vertex)=\true$
% w.r.t. $\values[\basicEvents,Y^\ast]<B>$ \emph{minimal}.
% \begin{proof}
% We prove the claims simultaneously by induction on the structure of
% the tree rooted in $\vertex$.
% \begin{itemize}
% \item Let $\vertex$ be a non-triggerable basic event. The claims
% follow by the definition of $\values<P>$ and $\values<B>$ since
% each of the assignments is clearly minimal.
% \item \emph{Induction Hypothesis}: Let
% $\values<P>(\vertex<\ast>)=(X_1,Y_1)$. For all
% subtrees of $\vertex$ in $\vertex<\ast>$, we have
% \begin{enumerate}
% \item If there exists no subset $Y_1^\ast \subsetneq Y_1|_{\vertex<\ast>}$
% s.t. $\values<B>(\vertex<\ast>)=\true$
% w.r.t. $\values[\basicEvents,Y_1^\ast]<B>$, then
% $Y_1 \in X_1$.
% \item If there exists no subset $Y_2^\ast \subsetneq Y_2|_{\vertex<\ast>}$
% s.t. $\values<B>(\vertex<\ast>)=\false$
% w.r.t. $\values[\basicEvents,Y_2^\ast]<B>$, then
% $Y_2 \in X_2$.
% \end{enumerate}
% \item $\typeFunction(\vertex)=\opTrigger$. The claims follow by
% definition of $\values<P>$ and $\values<B>$ and the induction
% hypothesis (since $\opTrigger$ maps to the identity function in
% both cases).
% \item $\vertex$ is a triggerable basic event and triggered by
% vertex~$\vertex<\ast>$ and we assume that there exists no subset
% $Y_1^\ast \subsetneq Y_1|_{\vertex<\ast>}$
% s.t. $\values<B>(\vertex)=\true$
% w.r.t. $\values[\basicEvents,Y_1^\ast]<B>$ and that there exists
% no subset $Y_2^\ast \subsetneq Y_2|_{\vertex<\ast>}$
% s.t. $\values<B>(\vertex<\ast>)=\false$
% w.r.t. $\values[\basicEvents,Y_2^\ast]<B>$.
% \begin{itemize}
% \item Assume there exists a subset
% $Y_1^\prime \subsetneq Y_1|_{\vertex}$
% s.t. $\values<B>(\vertex<\ast>)=\true$
% w.r.t. $\values[\basicEvents,Y_1^\ast|_{\vertex<\ast>}]<B>$. Then,
% $Y_1^\ast \cup \set{\vertex}$ is a satisfying assignment of
% $\vertex$ by definition and \Fref{theo:correctness}. By
% definition of $\values<P>$. $Y_1^\prime \cup \set{\vertex}$
% cannot be in $X_1$, which is a contradiction to our
% assumption. Hence, all minimal satisfying assignments need to
% be in $X_1$.
% \item Assume there exists a subset
% $Y_2^\prime \subsetneq Y_2|_{\vertex}$
% s.t. $\values<B>(\vertex<\ast>)=\false$
% w.r.t. $\values[\basicEvents,Y_2^\ast|_{\vertex<\ast>}]<B>$.
% $Y_2|_{\vertex} \neq \set{\vertex}$ since it would contradict
% our assumption. By definition of $\values<P>$,
% $Y_2|_{\vertex}$ must be an unsatisfying assignment of
% $\vertex<\ast>$. Hence, $Y_2^\prime$ and $Y_2|_{\vertex}$ must
% be unsatisfying assignments of $\vertex<\ast>$ by definition and
% \Fref{theo:correctness}. However, this contradicts the
% induction hypothesis.
% \end{itemize}
% \item $\typeFunction(\vertex)=\opAnd$: Analogously to the proof
% for triggerable basic events. However, the induction hypothesis
% needs to be used on both subtrees.
% \item $\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.
% \item $typeFunction(\vertex)=\opNeg$: Let $\vertex<\ast>$ be the
% input of $\vertex$ and let $\values<P>(\vertex)=(Y_1,Y_2)$. By
% definition, $\values<P>(\vertex<\ast>)=(Y_2,Y_1)$. Assume there
% eixsts a subset Assume there exists a subset
% $Y_1^\prime \subsetneq Y_1|_{\vertex}$
% s.t. $\values<B>(\vertex<\ast>)=\true$
% w.r.t. $\values[\basicEvents,Y_1^\ast|_{\vertex<\ast>}]<B>$. This
% contradicts the induction hypothesis. Assume there exists a
% subset $Y_2^\prime \subsetneq Y_2|_{\vertex}$
% s.t. $\values<B>(\vertex<\ast>)=\false$
% w.r.t. $\values[\basicEvents,Y_2^\ast|_{\vertex<\ast>}]<B>$. Again,
% this contradicts the induction hypothesis.
% \end{itemize}
% We have proven \Fref{theo:minimal} by induction.
% \end{proof}
% \Fref{theo:minimal} applied to $\topGoal$ shows us that every minimal
% satisfying or unsatisfying assignment is in $\vertex<P>(\topGoal)$, respectively.
Let $\exampleADD$ be an attack-defense tree. We say that a
valuation~$\values[\basicEvents] \colon \basicEvents \to
\set{\true,\false}$ is a \emph{successful attack} if
$\val(\topGoal) = \true$, and \emph{unsuccessful attack}
otherwise\footnote{Dually, this can be done for defenses by assigning
the goal~$\topGoal$ to the defender. Since we do not use player
swapping as in~\cite{kordy2011}, 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 \emph{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{definition}[Probabilistic Attack-Defense Trees]
% \label{def:prob}
% We consider the operators $\opAnd$, $\opOr$, $\opTrigger$ and
% $\opNeg$ and let all basic events be in
% $\basicAttacks \disjointUnion \basicDefenses$. We define a
% probabilistic interpretation~$\interpretation$ with $\type=[0,1]$.
% \begin{itemize}
% \item
% $\displaystyle{\interpretation(\vertex) (x_1,x_2)= x_1 \cdot x_2
% }$, if $\vertex$ is a triggerable basic event \emph{or}
% $\typeFunction(\vertex) \in \set{\opAnd,\opSand}$
% \item
% $\displaystyle{\interpretation(\vertex)(x_1,x_2)= x_1 + x_2 - x_1
% \cdot x_2}$ for $\typeFunction(\vertex)=\opOr$
% \item $\displaystyle{\interpretation(\opNeg)(x)=1-x}$
% \item $\displaystyle{\interpretation(\opTrigger)=\Id}$
% \end{itemize}
% We denote the probability bottom-up traversal semantics by $\val<\probabilityFunction>$.
% \end{definition}
% \begin{definition}[Delay Attack-Defense Trees]
% \label{def:delay}
% We consider the operators $\opAnd$, $\opOr$, $\opTrigger$ and
% $\opNeg$ and let all basic events be in
% $\basicAttacks \disjointUnion \basicDefenses$. We define a
% probabilistic interpretation~$\interpretation$ with $\type=\RR_{\geq0}\times\RR_{\geq0}$.
% \begin{itemize}
% \item
% $\displaystyle{\interpretation(\vertex)((x_1,x_2),(y_1,y_2))=
% (\max(x_1,y_1),\min(x_2,y_2))}$ (minimal delay) \newline and
% $(\max(x_1,y_1).\max(x_2,y_2))$ (maximal delay), if $\vertex$ is a
% triggerable basic event \emph{or} if
% $\typeFunction(\vertex)=\opAnd$.
% \item $\displaystyle{\interpretation(\vertex)((x_1,x_2),(y_1,y_2))= (\min(x_1,y_1),\max(x_2,y_2))}$ for
% the 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 the
% maximal delay (if events cannot fail) if
% $\typeFunction(\vertex)=\opOr$
% \item $\displaystyle{\interpretation(\opNeg)(x_1,x_2)=(x_2,x_1)}$
% \item $\displaystyle{\interpretation(\opTrigger)=\Id}$
% \end{itemize}
% We denote the minimal delay bottom-up traversal semantics by
% $\val<\delayFunction,\min>$ and the maximal cost bottom-up traversal
% semantics by $\val<\delayFunction,\max>$
% \end{definition}
% \begin{definition}[Cost Attack-Defense Trees]
% \label{def:delay}
% We consider the operators $\opAnd$, $\opOr$, $\opTrigger$ and
% $\opNeg$ and let all basic events be in
% $\basicAttacks \disjointUnion \basicDefenses$. We define a
% probabilistic interpretation~$\interpretation$ with $\type=\RR_{\geq
% 0}\times \RR_{\geq0}$.
% \begin{itemize}
% \item
% $\displaystyle{\interpretation(\vertex)((x_1,x_2),(y_1,y_2))=
% (x_1+y_1, \min(x_2,y_2))}$ (minimal delay) and
% $(x_1+y_1,\max(x_2,y_2))$ (maximal delay), if $\vertex$ is a
% triggerable basic event \emph{or} if
% $\typeFunction(\vertex)=\opAnd$
% \item $\displaystyle{\interpretation(\vertex)((x_1,x_2),(y_1,y_2))=(\min(x_1,y_1),x_2+y_2)}$ for
% the minimal cost and \newline
% $\displaystyle{\interpretation(\vertex)((x_1,x_2),(y_1,y_2))= (\max(x_1,y_1),x_2,+y_2)}$ for the
% maximal cost (if events cannot fail) if
% $\typeFunction(\vertex)=\opOr$
% \item $\displaystyle{\interpretation(\opNeg)(x_1,x_2)=(x_2,x_1)}$
% \item $\displaystyle{\interpretation(\opTrigger)=\Id}$
% \end{itemize}
% We denote the minimal cost bottom-up traversal semantics by
% $\val<\costFunction,\min>$ and the maximal cost bottom-up traversal
% semantics by $\val<\costFunction,\max>$
% \end{definition}
% We use
% $\values<\costFunction>[\basicEvents](\basicEvent) =
% (\costFunction,0)$ and
% $\values<\delayFunction>[\basicEvents](\basicEvent)=(\delayFunction,0)$. Cost
% and delays just occur if basic events are successfully attempted in an
% attack.
\begin{figure*}[!t]
% ensure that we have normalsize text
\normalsize
% Store the current equation number.
\setcounter{MYtempeqncnt}{\value{equation}}
% Set the equation number to one less than the one
\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}
% Restore the current equation number.
\setcounter{equation}{\value{MYtempeqncnt}}
% The IEEE uses as a separator
\hrulefill
% The spacer can be tweaked to stop underfull vboxes.
\vspace*{4pt}
\end{figure*}
\begin{theorem}[Correctness w.r.t. Boolean Semantics]
\label{theo:correctnessplain}
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 \Fref{eq:powerset} hold.
\end{theorem}
\begin{proof}
We prove all claims by an induction on the tree structure.
\begin{itemize}
\item $\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
definition.
\item \emph{Induction Hypothesis:} For subtrees rooted in a
vertex~$\vertex<\ast>$, which are predecessors of the
vertex~$\vertex$ , the equations in \Fref{eq:powerset} hold where
$\vertex$ is instantiated with the specific~$\vertex<\ast>$.
\item $\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).
\item $\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
\begin{itemize}
\item
$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)$.
\item
$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)$
\end{itemize}
\item $\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>$.
\begin{itemize}
\item 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).
\item Analogously, we can prove the claims for
$\values<\costFunction,\max>$, $\values<\delayFunction,\min>$
and $\values<\delayFunction,\max>$
\item
$\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, \newline
$\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)}$ \newline 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)) =
1-(1-\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.
\end{itemize}
\item $\typeFunction(\vertex)=\opAnd$: Analogously to the proof for
triggerable basic events. However, the induction hypothesis needs
to be used on both subtrees.
\item $\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.
\end{itemize}
\end{proof}
\pagebreak
\section{Correctness of PAC Analysis}
\label{app:pac}
\begin{theorem}[Correctness of \PAC{} Analysis]
\label{theo:pac}
\noindent Let $\exampleADD$ be an attack-defense tree and let $\values[\basicEvents]$ be a \PAC{} valuation for basic events, i.e., for every basic event~$\basicEvent \in \basicEvents$, it holds $\values[\basicEvents](\basicEvent)$ is $(\error[\basicEvent],\prob[\basicEvent])$-\PAC{} 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 \mbox{$\values<\ast>(\topGoal) \in \values(\topGoal) \pm
\error$}.
\end{theorem}
\begin{proof}
% Please note again: \emph{We cut off operations at 0 for all quantitative domains and at 1 for success probabilities for all computations with $\error$. Thus, if $x- \error[x]{} <0$, we replace the actual result with 0. If $x+ \error[x]{} >1$ (and we compute success probabilities), we replace the actual result by 1. We do not explicitly mention this in the following. This remark is essential for the cases on $\max$ and $\min$!}
Instead of proving the claim directly, we show that for any two \PAC{} 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
\begin{enumerate}
\item $(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]$.
\item
$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]$.\footnote{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.}
\item $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])$.
\item $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.
\item
$\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])$. \footnote{Using assumptions on the distribution of the error, more precise estimates are possible.\label{fn:assumptions}}
\item
$\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])$.\footref{fn:assumptions}
\end{enumerate}
The result of \Fref{theo:pac} then follows from a straightforward induction on the structure of the tree.
\end{proof}
%\enlargethispage{5cm}
% \begin{figure*}[!t]
% % ensure that we have normalsize text
% \normalsize
% % Store the current equation number.
% \setcounter{MYtempeqncnt}{\value{equation}}
% % Set the equation number to one less than the one
% \begin{equation*}
% \label{eq:proofpowerset}
% \begin{aligned}
% \end{aligned}
% \end{equation*}
% % Restore the current equation number.
% \setcounter{equation}{\value{MYtempeqncnt}}
% % The IEEE uses as a separator
% \hrulefill
% % The spacer can be tweaked to stop underfull vboxes.
% \vspace*{4pt}
% \end{figure*}
%%% Local Variables:
%%% mode: latex
%%% TeX-engine: xetex
%%% TeX-master: "main"
%%% End:
% $ biblatex auxiliary file $
% $ biblatex bbl format version 3.2 $
% Do not modify the above lines!
%
% This is an auxiliary file used by the 'biblatex' package.
% This file may safely be deleted. It will be recreated by
% biber as required.
%
\begingroup
\makeatletter
\@ifundefined{ver@biblatex.sty}
{\@latex@error
{Missing 'biblatex' package}
{The bibliography requires the 'biblatex' package.}
\aftergroup\endinput}
{}
\endgroup
\refsection{0}
\datalist[entry]{nty/global//global/global}
\entry{andre2019}{inproceedings}{}
\name{author}{4}{}{%
{{hash=932f6019fd954416b7cba978f1929175}{%
family={André},
familyi={A\bibinitperiod},
given={Étienne},
giveni={É\bibinitperiod}}}%
{{hash=f22328b422093d53c1c889e08452d416}{%
family={Lime},
familyi={L\bibinitperiod},
given={Didier},
giveni={D\bibinitperiod}}}%
{{hash=b1d0ce2ebe5236a1dfc89b85fedddfe2}{%
family={Ramparison},
familyi={R\bibinitperiod},
given={Mathias},
giveni={M\bibinitperiod}}}%
{{hash=1de27df00ec03386445460a544abaf31}{%
family={Stoelinga},
familyi={S\bibinitperiod},
given={Mariëlle},
giveni={M\bibinitperiod}}}%
}
\list{organization}{1}{%
{IEEE}%
}
\strng{namehash}{7e3d58285e40ba352bae96454d25607e}
\strng{fullhash}{829d64d5aed8acdedc57993a6bc3acd8}
\strng{bibnamehash}{7e3d58285e40ba352bae96454d25607e}
\strng{authorbibnamehash}{7e3d58285e40ba352bae96454d25607e}
\strng{authornamehash}{7e3d58285e40ba352bae96454d25607e}
\strng{authorfullhash}{829d64d5aed8acdedc57993a6bc3acd8}
\field{sortinit}{A}
\field{sortinithash}{2f401846e2029bad6b3ecc16d50031e2}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{booktitle}{2019 19th International Conference on Application of Concurrency to System Design (ACSD)}
\field{title}{Parametric analyses of attack-fault trees}
\field{year}{2019}
\field{pages}{33\bibrangedash 42}
\range{pages}{10}
\endentry
\entry{arnold2014}{inproceedings}{}
\name{author}{4}{}{%
{{hash=3877d198ce57a275dc840fe6a459f7ff}{%
family={Arnold},
familyi={A\bibinitperiod},
given={F.},
giveni={F\bibinitperiod}}}%
{{hash=7b1999eb5c41ecc522af7bfd4091c577}{%
family={Hermanns},
familyi={H\bibinitperiod},
given={H.},
giveni={H\bibinitperiod}}}%
{{hash=216d332b41674ed2974592b3ac1c4300}{%
family={Pulungan},
familyi={P\bibinitperiod},
given={R.},
giveni={R\bibinitperiod}}}%
{{hash=eb8add136d456c3e6a238f7c70e7d663}{%
family={M.I.A.\bibnamedelimi Stoelinga},
familyi={M\bibinitperiod\bibinitdelim S\bibinitperiod}}}%
}
\list{publisher}{1}{%
{Springer}%
}
\strng{namehash}{75ec313d06686bc006f3c7c6df66de41}
\strng{fullhash}{874ac630ece53140d296114fe7ee1e41}
\strng{bibnamehash}{75ec313d06686bc006f3c7c6df66de41}
\strng{authorbibnamehash}{75ec313d06686bc006f3c7c6df66de41}
\strng{authornamehash}{75ec313d06686bc006f3c7c6df66de41}
\strng{authorfullhash}{874ac630ece53140d296114fe7ee1e41}
\field{sortinit}{A}
\field{sortinithash}{2f401846e2029bad6b3ecc16d50031e2}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{booktitle}{{POST}}
\field{series}{LNCS}
\field{title}{Time-Dependent Analysis of Attacks}
\field{volume}{8414}
\field{year}{2014}
\field{pages}{285\bibrangedash 305}
\range{pages}{21}
\endentry
\entry{aslanyan2016}{inproceedings}{}
\name{author}{3}{}{%
{{hash=3f76c0a8bf93e5d3632cc89788351b62}{%
family={Aslanyan},
familyi={A\bibinitperiod},
given={Zaruhi},
giveni={Z\bibinitperiod}}}%
{{hash=a4a1d0b12b1b99c1c382e8addbc40e96}{%
family={Nielson},
familyi={N\bibinitperiod},
given={Flemming},
giveni={F\bibinitperiod}}}%
{{hash=85aa04746604480ce47f280e167052ff}{%
family={Parker},
familyi={P\bibinitperiod},
given={David},
giveni={D\bibinitperiod}}}%
}
\strng{namehash}{db0710e9bae7d44b756fa0e0cf406499}
\strng{fullhash}{db0710e9bae7d44b756fa0e0cf406499}
\strng{bibnamehash}{db0710e9bae7d44b756fa0e0cf406499}
\strng{authorbibnamehash}{db0710e9bae7d44b756fa0e0cf406499}
\strng{authornamehash}{db0710e9bae7d44b756fa0e0cf406499}
\strng{authorfullhash}{db0710e9bae7d44b756fa0e0cf406499}
\field{sortinit}{A}
\field{sortinithash}{2f401846e2029bad6b3ecc16d50031e2}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{booktitle}{Computer Security Foundations Symposium (CSF)}
\field{title}{Quantitative Verification and Synthesis of Attack-Defence Scenarios}
\field{year}{2016}
\field{pages}{105\bibrangedash 119}
\range{pages}{15}
\verb{doi}
\verb 10.1109/CSF.2016.15
\endverb
\verb{urlraw}
\verb https://doi.org/10.1109/CSF.2016.15
\endverb
\verb{url}
\verb https://doi.org/10.1109/CSF.2016.15
\endverb
\endentry
\entry{beckers2014}{inproceedings}{}
\name{author}{6}{}{%
{{hash=bf2c93e65eca541dbf3a50c4995ef5bf}{%
family={Beckers},
familyi={B\bibinitperiod},
given={Kristian},
giveni={K\bibinitperiod}}}%
{{hash=6ed87753fe0803227b91cbec79f895b4}{%
family={Heisel},
familyi={H\bibinitperiod},
given={Maritta},
giveni={M\bibinitperiod}}}%
{{hash=4e50c32df2952e776fd5129a88241b53}{%
family={Krautsevich},
familyi={K\bibinitperiod},
given={Leanid},
giveni={L\bibinitperiod}}}%
{{hash=88dd87552427dca0e6263e2960769fc9}{%
family={Martinelli},
familyi={M\bibinitperiod},
given={Fabio},
giveni={F\bibinitperiod}}}%
{{hash=1d5cc7b575a5aea8e3402eb0a303129b}{%
family={Meis},
familyi={M\bibinitperiod},
given={Rene},
giveni={R\bibinitperiod}}}%
{{hash=f6843e34dee1caccf59e8d54ada871db}{%
family={Yautsiukhin},
familyi={Y\bibinitperiod},
given={Artsiom},
giveni={A\bibinitperiod}}}%
}
\list{organization}{1}{%
{Springer}%
}
\strng{namehash}{ed5a8044ac1713cf5d063c2a0b6b9a7d}
\strng{fullhash}{614af9fff9c1acb3e6e1221cddc1b4b7}
\strng{bibnamehash}{ed5a8044ac1713cf5d063c2a0b6b9a7d}
\strng{authorbibnamehash}{ed5a8044ac1713cf5d063c2a0b6b9a7d}
\strng{authornamehash}{ed5a8044ac1713cf5d063c2a0b6b9a7d}
\strng{authorfullhash}{614af9fff9c1acb3e6e1221cddc1b4b7}
\field{sortinit}{B}
\field{sortinithash}{d7095fff47cda75ca2589920aae98399}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{booktitle}{International Workshop on Smart Grid Security}
\field{title}{Determining the probability of smart grid attacks by combining attack tree and attack graph analysis}
\field{year}{2014}
\field{pages}{30\bibrangedash 47}
\range{pages}{18}
\endentry
\entry{ter2021quantitative}{article}{}
\name{author}{4}{}{%
{{hash=6a581ac4130e7903a20c0566acfe145d}{%
family={Beek},
familyi={B\bibinitperiod},
given={Maurice\bibnamedelima H},
giveni={M\bibinitperiod\bibinitdelim H\bibinitperiod},
prefix={ter},
prefixi={t\bibinitperiod}}}%
{{hash=0fabf3660126ac9e07707dbfb289fd2e}{%
family={Legay},
familyi={L\bibinitperiod},
given={Axel},
giveni={A\bibinitperiod}}}%
{{hash=6da55768265515548c9c9d2fdd5842b3}{%
family={Lafuente},
familyi={L\bibinitperiod},
given={Alberto\bibnamedelima Lluch},
giveni={A\bibinitperiod\bibinitdelim L\bibinitperiod}}}%
{{hash=bab0dce7b8a11d35b0ff0c1ec86243ca}{%
family={Vandin},
familyi={V\bibinitperiod},
given={Andrea},
giveni={A\bibinitperiod}}}%
}
\list{publisher}{1}{%
{Elsevier}%
}
\strng{namehash}{ffa6cb580dd92f20b3a442566394025b}
\strng{fullhash}{36aeb6837cfe76a4585eae7e13b4ce76}
\strng{bibnamehash}{ffa6cb580dd92f20b3a442566394025b}
\strng{authorbibnamehash}{ffa6cb580dd92f20b3a442566394025b}
\strng{authornamehash}{ffa6cb580dd92f20b3a442566394025b}
\strng{authorfullhash}{36aeb6837cfe76a4585eae7e13b4ce76}
\field{sortinit}{B}
\field{sortinithash}{d7095fff47cda75ca2589920aae98399}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{journaltitle}{computers \& security}
\field{title}{Quantitative security risk modeling and analysis with RisQFLan}
\field{volume}{109}
\field{year}{2021}
\field{pages}{102381}
\range{pages}{1}
\endentry
\entry{behrmann2006}{inproceedings}{}
\name{author}{7}{}{%
{{hash=19555d20a6131c7144fe0272b2f6e266}{%
family={Behrmann},
familyi={B\bibinitperiod},
given={Gerd},
giveni={G\bibinitperiod}}}%
{{hash=e6abba6779334d14a008ecfff8fcbbeb}{%
family={David},
familyi={D\bibinitperiod},
given={Alexandre},
giveni={A\bibinitperiod}}}%
{{hash=1d74b0c6afa306c62f868ed08f077ddd}{%
family={Larsen},
familyi={L\bibinitperiod},
given={Kim\bibnamedelima G.},
giveni={K\bibinitperiod\bibinitdelim G\bibinitperiod}}}%
{{hash=8c1f0a97e37044615db6a539b31730f4}{%
family={Hakansson},
familyi={H\bibinitperiod},
given={John},
giveni={J\bibinitperiod}}}%
{{hash=2240bbc048eea2f02be6f96a0da4962b}{%
family={Petterson},
familyi={P\bibinitperiod},
given={Paul},
giveni={P\bibinitperiod}}}%
{{hash=b6332f8573feb048f5907824e6a19030}{%
family={Yi},
familyi={Y\bibinitperiod},
given={Wang},
giveni={W\bibinitperiod}}}%
{{hash=727e323991caac57472af2a58ce848e7}{%
family={Hendriks},
familyi={H\bibinitperiod},
given={Martijn},
giveni={M\bibinitperiod}}}%
}
\list{location}{1}{%
{Washington, DC, USA}%
}
\list{publisher}{1}{%
{IEEE Computer Society}%
}
\strng{namehash}{6751215b6a9ce3a12897d0edc8e57ffb}
\strng{fullhash}{ab1f52222103c3283d4153eb8a225bec}
\strng{bibnamehash}{6751215b6a9ce3a12897d0edc8e57ffb}
\strng{authorbibnamehash}{6751215b6a9ce3a12897d0edc8e57ffb}
\strng{authornamehash}{6751215b6a9ce3a12897d0edc8e57ffb}
\strng{authorfullhash}{ab1f52222103c3283d4153eb8a225bec}
\field{sortinit}{B}
\field{sortinithash}{d7095fff47cda75ca2589920aae98399}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{booktitle}{Quantitative Evaluation of Systems (QEST)}
\field{isbn}{0-7695-2665-9}
\field{series}{QEST '06}
\field{title}{UPPAAL 4.0}
\field{year}{2006}
\field{pages}{125\bibrangedash 126}
\range{pages}{2}
\verb{doi}
\verb 10.1109/QEST.2006.59
\endverb
\verb{urlraw}
\verb http://dx.doi.org/10.1109/QEST.2006.59
\endverb
\verb{url}
\verb http://dx.doi.org/10.1109/QEST.2006.59
\endverb
\endentry
\entry{arimacovid}{article}{}
\name{author}{5}{}{%
{{hash=d6c694cbce92c97f754b054e0cd85cc9}{%
family={Benvenuto},
familyi={B\bibinitperiod},
given={Domenico},
giveni={D\bibinitperiod}}}%
{{hash=c014c8f004710aac5b66f5415c8fd655}{%
family={Giovanetti},
familyi={G\bibinitperiod},
given={Marta},
giveni={M\bibinitperiod}}}%
{{hash=2abd034f37a92ad22b99a9af032395c0}{%
family={Vassallo},
familyi={V\bibinitperiod},
given={Lazzaro},
giveni={L\bibinitperiod}}}%
{{hash=81d064bfb4e0fe200ff0a29d8ba411fe}{%
family={Angeletti},
familyi={A\bibinitperiod},
given={Silvia},
giveni={S\bibinitperiod}}}%
{{hash=533b31fabafdfa31f32ecd6a23882155}{%
family={Ciccozzi},
familyi={C\bibinitperiod},
given={Massimo},
giveni={M\bibinitperiod}}}%
}
\strng{namehash}{fd7e1327dd8359583aac061fb5851e10}
\strng{fullhash}{ba1b9371eb42db2b5d1e300270723cd1}
\strng{bibnamehash}{fd7e1327dd8359583aac061fb5851e10}
\strng{authorbibnamehash}{fd7e1327dd8359583aac061fb5851e10}
\strng{authornamehash}{fd7e1327dd8359583aac061fb5851e10}
\strng{authorfullhash}{ba1b9371eb42db2b5d1e300270723cd1}
\field{sortinit}{B}
\field{sortinithash}{d7095fff47cda75ca2589920aae98399}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{issn}{2352-3409}
\field{journaltitle}{Data in Brief}
\field{title}{Application of the ARIMA model on the COVID-2019 epidemic dataset}
\field{volume}{29}
\field{year}{2020}
\verb{doi}
\verb 10.1016/j.dib.2020.105340
\endverb
\verb{urlraw}
\verb http://dx.doi.org/10.1016/j.dib.2020.105340
\endverb
\verb{url}
\verb http://dx.doi.org/10.1016/j.dib.2020.105340
\endverb
\endentry
\entry{budde2017}{inproceedings}{}
\name{author}{6}{}{%
{{hash=ed94d773d693a01aa6ee5a7592095934}{%
family={Budde},
familyi={B\bibinitperiod},
given={Carlos\bibnamedelima E},
giveni={C\bibinitperiod\bibinitdelim E\bibinitperiod}}}%
{{hash=5e63f298766caafb7f8f711ccd248a4a}{%
family={Dehnert},
familyi={D\bibinitperiod},
given={Christian},
giveni={C\bibinitperiod}}}%
{{hash=0e4be134f864fd66777835ea8f0fbe99}{%
family={Hahn},
familyi={H\bibinitperiod},
given={Ernst\bibnamedelima Moritz},
giveni={E\bibinitperiod\bibinitdelim M\bibinitperiod}}}%
{{hash=5ee8e32c129a82f9fe67944701c268bf}{%
family={Hartmanns},
familyi={H\bibinitperiod},
given={Arnd},
giveni={A\bibinitperiod}}}%
{{hash=29202fc00e502e6a06092a566a4d041e}{%
family={Junges},
familyi={J\bibinitperiod},
given={Sebastian},
giveni={S\bibinitperiod}}}%
{{hash=c09e9de37c78c61294b9d525ef42cbcb}{%
family={Turrini},
familyi={T\bibinitperiod},
given={Andrea},
giveni={A\bibinitperiod}}}%
}
\list{organization}{1}{%
{Springer}%
}
\strng{namehash}{5c2a279935cd2d82bc43d2ffb85ddc50}
\strng{fullhash}{ef9cd99076f9796dc3268829cdbce79a}
\strng{bibnamehash}{5c2a279935cd2d82bc43d2ffb85ddc50}
\strng{authorbibnamehash}{5c2a279935cd2d82bc43d2ffb85ddc50}
\strng{authornamehash}{5c2a279935cd2d82bc43d2ffb85ddc50}
\strng{authorfullhash}{ef9cd99076f9796dc3268829cdbce79a}
\field{sortinit}{B}
\field{sortinithash}{d7095fff47cda75ca2589920aae98399}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{booktitle}{Tools and Algorithms for the Construction and Analysis of Systems (TACAS)}
\field{title}{JANI: quantitative model and tool interaction}
\field{year}{2017}
\field{pages}{151\bibrangedash 168}
\range{pages}{18}
\endentry
\entry{buldas2020}{article}{}
\name{author}{5}{}{%
{{hash=87b7dee907083dadab476651e38953f0}{%
family={Buldas},
familyi={B\bibinitperiod},
given={Ahto},
giveni={A\bibinitperiod}}}%
{{hash=e8c9851b54b17fa6ab7290158c810f1e}{%
family={Gadyatskaya},
familyi={G\bibinitperiod},
given={Olga},
giveni={O\bibinitperiod}}}%
{{hash=49d653146234688cc53f00fbee90001c}{%
family={Lenin},
familyi={L\bibinitperiod},
given={Aleksandr},
giveni={A\bibinitperiod}}}%
{{hash=07d4e3cd2ae1cce77c8a3fb46c665f02}{%
family={Mauw},
familyi={M\bibinitperiod},
given={Sjouke},
giveni={S\bibinitperiod}}}%
{{hash=14c979d652d68786f1cb43ce43e71489}{%
family={Trujillo-Rasua},
familyi={T\bibinithyphendelim R\bibinitperiod},
given={Rolando},
giveni={R\bibinitperiod}}}%
}
\list{publisher}{1}{%
{Elsevier}%
}
\strng{namehash}{5a067aae3a4fc34ea5d2f63a2a279bba}
\strng{fullhash}{8ddcbbb7f2e8f131e6c6cd74058ac52c}
\strng{bibnamehash}{5a067aae3a4fc34ea5d2f63a2a279bba}
\strng{authorbibnamehash}{5a067aae3a4fc34ea5d2f63a2a279bba}
\strng{authornamehash}{5a067aae3a4fc34ea5d2f63a2a279bba}
\strng{authorfullhash}{8ddcbbb7f2e8f131e6c6cd74058ac52c}
\field{sortinit}{B}
\field{sortinithash}{d7095fff47cda75ca2589920aae98399}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{journaltitle}{Computers \& Security}
\field{title}{Attribute evaluation on attack trees with incomplete information}
\field{volume}{88}
\field{year}{2020}
\field{pages}{101630}
\range{pages}{1}
\endentry
\entry{buoni2010}{inproceedings}{}
\name{author}{3}{}{%
{{hash=42373a785c20ce7ef88005f3a40ed4fd}{%
family={Buoni},
familyi={B\bibinitperiod},
given={Alessandro},
giveni={A\bibinitperiod}}}%
{{hash=5587e03dd357f9cc8220665037cc24a0}{%
family={Fedrizzi},
familyi={F\bibinitperiod},
given={Mario},
giveni={M\bibinitperiod}}}%
{{hash=9d4a6164a0484350870ada45ac6822a2}{%
family={Mezei},
familyi={M\bibinitperiod},
given={József},
giveni={J\bibinitperiod}}}%
}
\strng{namehash}{1d1c3c6a723ba19a77aa49513f70c9b7}
\strng{fullhash}{1d1c3c6a723ba19a77aa49513f70c9b7}
\strng{bibnamehash}{1d1c3c6a723ba19a77aa49513f70c9b7}
\strng{authorbibnamehash}{1d1c3c6a723ba19a77aa49513f70c9b7}
\strng{authornamehash}{1d1c3c6a723ba19a77aa49513f70c9b7}
\strng{authorfullhash}{1d1c3c6a723ba19a77aa49513f70c9b7}
\field{sortinit}{B}
\field{sortinithash}{d7095fff47cda75ca2589920aae98399}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{booktitle}{Proceeding of the IASK International Conferences}
\field{title}{A Delphi-based approach to fraud detection using attack trees and fuzzy numbers}
\field{year}{2010}
\field{pages}{21\bibrangedash 28}
\range{pages}{8}
\endentry
\entry{byres2004}{inproceedings}{}
\name{author}{3}{}{%
{{hash=578eb36259c2cc68137cd70d15575202}{%
family={Byres},
familyi={B\bibinitperiod},
given={Eric\bibnamedelima J},
giveni={E\bibinitperiod\bibinitdelim J\bibinitperiod}}}%
{{hash=b8aaff998fa508affee626c17b633275}{%
family={Franz},
familyi={F\bibinitperiod},
given={Matthew},
giveni={M\bibinitperiod}}}%
{{hash=f8bddd06ace11e32a6a2d9a0c5f083fa}{%
family={Miller},
familyi={M\bibinitperiod},
given={Darrin},
giveni={D\bibinitperiod}}}%
}
\list{organization}{1}{%
{Citeseer}%
}
\strng{namehash}{9aa0cccafd2ef879d2503034e5c662ba}
\strng{fullhash}{9aa0cccafd2ef879d2503034e5c662ba}
\strng{bibnamehash}{9aa0cccafd2ef879d2503034e5c662ba}
\strng{authorbibnamehash}{9aa0cccafd2ef879d2503034e5c662ba}
\strng{authornamehash}{9aa0cccafd2ef879d2503034e5c662ba}
\strng{authorfullhash}{9aa0cccafd2ef879d2503034e5c662ba}
\field{sortinit}{B}
\field{sortinithash}{d7095fff47cda75ca2589920aae98399}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{booktitle}{Proceedings of the international infrastructure survivability workshop}
\field{title}{The use of attack trees in assessing vulnerabilities in SCADA systems}
\field{year}{2004}
\field{pages}{3\bibrangedash 10}
\range{pages}{8}
\endentry
\entry{arimapacarticle}{article}{}
\name{author}{1}{}{%
{{hash=7060a66f87c89de0ed44bff8e3124265}{%
family={Chatfield},
familyi={C\bibinitperiod},
given={Chris},
giveni={C\bibinitperiod}}}%
}
\list{publisher}{1}{%
{[American Statistical Association, Taylor $\&$ Francis, Ltd.]}%
}
\strng{namehash}{7060a66f87c89de0ed44bff8e3124265}
\strng{fullhash}{7060a66f87c89de0ed44bff8e3124265}
\strng{bibnamehash}{7060a66f87c89de0ed44bff8e3124265}
\strng{authorbibnamehash}{7060a66f87c89de0ed44bff8e3124265}
\strng{authornamehash}{7060a66f87c89de0ed44bff8e3124265}
\strng{authorfullhash}{7060a66f87c89de0ed44bff8e3124265}
\field{sortinit}{C}
\field{sortinithash}{4d103a86280481745c9c897c925753c0}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{journaltitle}{Journal of Business $\&$ Economic Statistics}
\field{number}{2}
\field{title}{Calculating Interval Forecasts}
\field{volume}{11}
\field{year}{1993}
\field{pages}{121\bibrangedash 135}
\range{pages}{15}
\verb{urlraw}
\verb http://www.jstor.org/stable/1391361
\endverb
\verb{url}
\verb http://www.jstor.org/stable/1391361
\endverb
\endentry
\entry{chen2013}{inproceedings}{}
\name{author}{5}{}{%
{{hash=17541c65107086b7d7dd596d7ad81405}{%
family={Chen},
familyi={C\bibinitperiod},
given={T.},
giveni={T\bibinitperiod}}}%
{{hash=c21bdb8ff500b8270c8b61fc26c96c15}{%
family={Forejt},
familyi={F\bibinitperiod},
given={V.},
giveni={V\bibinitperiod}}}%
{{hash=44f96ce7a6edd0d0f29170daeee1d90f}{%
family={Kwiatkowska},
familyi={K\bibinitperiod},
given={M.},
giveni={M\bibinitperiod}}}%
{{hash=8f917e59f9bcb671f7f68671bf759fe7}{%
family={Parker},
familyi={P\bibinitperiod},
given={D.},
giveni={D\bibinitperiod}}}%
{{hash=eac108b33aa9537f197544778ed8067b}{%
family={Simaitis},
familyi={S\bibinitperiod},
given={A.},
giveni={A\bibinitperiod}}}%
}
\name{editor}{2}{}{%
{{hash=e5f61d738a073f73e4fb10c06df86356}{%
family={Piterman},
familyi={P\bibinitperiod},
given={N.},
giveni={N\bibinitperiod}}}%
{{hash=1e135edf6af030953529f063c9130c8f}{%
family={Smolka},
familyi={S\bibinitperiod},
given={S.},
giveni={S\bibinitperiod}}}%
}
\list{publisher}{1}{%
{Springer}%
}
\strng{namehash}{97d371540f094c82bcf673670dba6c7d}
\strng{fullhash}{f382ab8e9a8c37c8925cb5fa89a03065}
\strng{bibnamehash}{97d371540f094c82bcf673670dba6c7d}
\strng{authorbibnamehash}{97d371540f094c82bcf673670dba6c7d}
\strng{authornamehash}{97d371540f094c82bcf673670dba6c7d}
\strng{authorfullhash}{f382ab8e9a8c37c8925cb5fa89a03065}
\strng{editorbibnamehash}{e15753e433e3c623acd9a00d862b5d0c}
\strng{editornamehash}{e15753e433e3c623acd9a00d862b5d0c}
\strng{editorfullhash}{e15753e433e3c623acd9a00d862b5d0c}
\field{sortinit}{C}
\field{sortinithash}{4d103a86280481745c9c897c925753c0}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{booktitle}{Tools and Algorithms for the Construction and Analysis of Systems (TACAS)}
\field{series}{LNCS}
\field{title}{{PRISM-games}: A Model Checker for Stochastic Multi-Player Games}
\field{volume}{7795}
\field{year}{2013}
\field{pages}{185\bibrangedash 191}
\range{pages}{7}
\endentry
\entry{arimaelectricity}{article}{}
\name{author}{4}{}{%
{{hash=462c2a19535582f75d1cbf49bdafba13}{%
family={{Contreras}},
familyi={C\bibinitperiod},
given={J.},
giveni={J\bibinitperiod}}}%
{{hash=99cdac16e1534210deb920478aa4e0ba}{%
family={{Espinola}},
familyi={E\bibinitperiod},
given={R.},
giveni={R\bibinitperiod}}}%
{{hash=9cd58cde28880b6339cab8dffe924049}{%
family={{Nogales}},
familyi={N\bibinitperiod},
given={F.\bibnamedelimi J.},
giveni={F\bibinitperiod\bibinitdelim J\bibinitperiod}}}%
{{hash=4283ec126a1c20ad3825b0d487fb2d80}{%
family={{Conejo}},
familyi={C\bibinitperiod},
given={A.\bibnamedelimi J.},
giveni={A\bibinitperiod\bibinitdelim J\bibinitperiod}}}%
}
\strng{namehash}{6ef848731eb0310b6f3e4a2717fdb9c1}
\strng{fullhash}{e0f926351f71e60a09dbba37199dbc63}
\strng{bibnamehash}{6ef848731eb0310b6f3e4a2717fdb9c1}
\strng{authorbibnamehash}{6ef848731eb0310b6f3e4a2717fdb9c1}
\strng{authornamehash}{6ef848731eb0310b6f3e4a2717fdb9c1}
\strng{authorfullhash}{e0f926351f71e60a09dbba37199dbc63}
\field{sortinit}{C}
\field{sortinithash}{4d103a86280481745c9c897c925753c0}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{journaltitle}{IEEE Transactions on Power Systems}
\field{number}{3}
\field{title}{ARIMA models to predict next-day electricity prices}
\field{volume}{18}
\field{year}{2003}
\field{pages}{1014\bibrangedash 1020}
\range{pages}{7}
\endentry
\entry{al2019}{inproceedings}{}
\name{author}{2}{}{%
{{hash=0867cf4b451830db6805b35f3485768b}{%
family={AL-Dahasi},
familyi={A\bibinithyphendelim D\bibinitperiod},
given={A\bibnamedelima Ezaz\bibnamedelima Mohammed},
giveni={A\bibinitperiod\bibinitdelim E\bibinitperiod\bibinitdelim M\bibinitperiod}}}%
{{hash=febdd5c515715917fbe486c8701f02be}{%
family={Saqib},
familyi={S\bibinitperiod},
given={B\bibnamedelima Nazar\bibnamedelima Abbas},
giveni={B\bibinitperiod\bibinitdelim N\bibinitperiod\bibinitdelim A\bibinitperiod}}}%
}
\list{organization}{1}{%
{IEEE}%
}
\strng{namehash}{caff7138cfe519a5a928282d9d6ccc7e}
\strng{fullhash}{caff7138cfe519a5a928282d9d6ccc7e}
\strng{bibnamehash}{caff7138cfe519a5a928282d9d6ccc7e}
\strng{authorbibnamehash}{caff7138cfe519a5a928282d9d6ccc7e}
\strng{authornamehash}{caff7138cfe519a5a928282d9d6ccc7e}
\strng{authorfullhash}{caff7138cfe519a5a928282d9d6ccc7e}
\field{sortinit}{D}
\field{sortinithash}{6f385f66841fb5e82009dc833c761848}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{booktitle}{2019 27th Telecommunications Forum (TELFOR)}
\field{title}{Attack tree Model for Potential Attacks Against the SCADA System}
\field{year}{2019}
\field{pages}{1\bibrangedash 4}
\range{pages}{4}
\endentry
\entry{dehnert2017}{inproceedings}{}
\name{author}{4}{}{%
{{hash=5e63f298766caafb7f8f711ccd248a4a}{%
family={Dehnert},
familyi={D\bibinitperiod},
given={Christian},
giveni={C\bibinitperiod}}}%
{{hash=29202fc00e502e6a06092a566a4d041e}{%
family={Junges},
familyi={J\bibinitperiod},
given={Sebastian},
giveni={S\bibinitperiod}}}%
{{hash=392d5825b15ef7f81f68632c7a49fdef}{%
family={Katoen},
familyi={K\bibinitperiod},
given={Joost-Pieter},
giveni={J\bibinithyphendelim P\bibinitperiod}}}%
{{hash=ac49976e229e5180f7f8ba6acbfab71b}{%
family={Volk},
familyi={V\bibinitperiod},
given={Matthias},
giveni={M\bibinitperiod}}}%
}
\list{organization}{1}{%
{Springer}%
}
\strng{namehash}{7df1ccca870052f119e5cfb10b3131dc}
\strng{fullhash}{384e4ec4e83e48a9c25f21290f7add4e}
\strng{bibnamehash}{7df1ccca870052f119e5cfb10b3131dc}
\strng{authorbibnamehash}{7df1ccca870052f119e5cfb10b3131dc}
\strng{authornamehash}{7df1ccca870052f119e5cfb10b3131dc}
\strng{authorfullhash}{384e4ec4e83e48a9c25f21290f7add4e}
\field{sortinit}{D}
\field{sortinithash}{6f385f66841fb5e82009dc833c761848}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{booktitle}{International Conference on Computer Aided Verification}
\field{title}{A storm is coming: A modern probabilistic model checker}
\field{year}{2017}
\field{pages}{592\bibrangedash 600}
\range{pages}{9}
\endentry
\entry{eisentraut2019}{inproceedings}{}
\name{author}{2}{}{%
{{hash=d0d5b4ba6588029dff0b922ee5e7c74a}{%
family={Eisentraut},
familyi={E\bibinitperiod},
given={Julia},
giveni={J\bibinitperiod}}}%
{{hash=7f4f842042226213d5638f2046a5e40a}{%
family={Křetínskỳ},
familyi={K\bibinitperiod},
given={Jan},
giveni={J\bibinitperiod}}}%
}
\list{organization}{1}{%
{Springer}%
}
\strng{namehash}{8445e4aee1a6b8c9dbb4766f6434ccab}
\strng{fullhash}{8445e4aee1a6b8c9dbb4766f6434ccab}
\strng{bibnamehash}{8445e4aee1a6b8c9dbb4766f6434ccab}
\strng{authorbibnamehash}{8445e4aee1a6b8c9dbb4766f6434ccab}
\strng{authornamehash}{8445e4aee1a6b8c9dbb4766f6434ccab}
\strng{authorfullhash}{8445e4aee1a6b8c9dbb4766f6434ccab}
\field{sortinit}{E}
\field{sortinithash}{8da8a182d344d5b9047633dfc0cc9131}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{booktitle}{International Conference on Quantitative Evaluation of Systems}
\field{title}{Expected Cost Analysis of Attack-Defense Trees}
\field{year}{2019}
\field{pages}{203\bibrangedash 221}
\range{pages}{19}
\endentry
\entry{fila2019}{inproceedings}{}
\name{author}{2}{}{%
{{hash=1efa860d3d32836b9d17dc9d9d67efab}{%
family={Fila},
familyi={F\bibinitperiod},
given={Barbara},
giveni={B\bibinitperiod}}}%
{{hash=e016db57ad3c74fc0222ca4cc6e027af}{%
family={Wide{ł}},
familyi={W\bibinitperiod},
given={Wojciech},
giveni={W\bibinitperiod}}}%
}
\list{organization}{1}{%
{Springer}%
}
\strng{namehash}{d3a636089088f7afc88f054ed076835b}
\strng{fullhash}{d3a636089088f7afc88f054ed076835b}
\strng{bibnamehash}{d3a636089088f7afc88f054ed076835b}
\strng{authorbibnamehash}{d3a636089088f7afc88f054ed076835b}
\strng{authornamehash}{d3a636089088f7afc88f054ed076835b}
\strng{authorfullhash}{d3a636089088f7afc88f054ed076835b}
\field{sortinit}{F}
\field{sortinithash}{2638baaa20439f1b5a8f80c6c08a13b4}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{booktitle}{International Workshop on Graphical Models for Security}
\field{title}{Attack--defense trees for abusing optical power meters: A case study and the OSEAD tool experience report}
\field{year}{2019}
\field{pages}{95\bibrangedash 125}
\range{pages}{31}
\endentry
\entry{fraile2016}{inproceedings}{}
\name{author}{6}{}{%
{{hash=c50e487238e5cc8e48c034a24e0be7e2}{%
family={Fraile},
familyi={F\bibinitperiod},
given={Marlon},
giveni={M\bibinitperiod}}}%
{{hash=dededcc2317695be64dfc14fbfef1740}{%
family={Ford},
familyi={F\bibinitperiod},
given={Margaret},
giveni={M\bibinitperiod}}}%
{{hash=e8c9851b54b17fa6ab7290158c810f1e}{%
family={Gadyatskaya},
familyi={G\bibinitperiod},
given={Olga},
giveni={O\bibinitperiod}}}%
{{hash=5dbaee2bd1f68bfb2185d56f91e4b038}{%
family={Kumar},
familyi={K\bibinitperiod},
given={Rajesh},
giveni={R\bibinitperiod}}}%
{{hash=1de27df00ec03386445460a544abaf31}{%
family={Stoelinga},
familyi={S\bibinitperiod},
given={Mariëlle},
giveni={M\bibinitperiod}}}%
{{hash=14c979d652d68786f1cb43ce43e71489}{%
family={Trujillo-Rasua},
familyi={T\bibinithyphendelim R\bibinitperiod},
given={Rolando},
giveni={R\bibinitperiod}}}%
}
\strng{namehash}{1e9a20584df57935388c7986ff465dfd}
\strng{fullhash}{0e1ba96c067f5927935c236942b122cc}
\strng{bibnamehash}{1e9a20584df57935388c7986ff465dfd}
\strng{authorbibnamehash}{1e9a20584df57935388c7986ff465dfd}
\strng{authornamehash}{1e9a20584df57935388c7986ff465dfd}
\strng{authorfullhash}{0e1ba96c067f5927935c236942b122cc}
\field{sortinit}{F}
\field{sortinithash}{2638baaa20439f1b5a8f80c6c08a13b4}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{booktitle}{The Practice of Enterprise Modeling (IFIP)}
\field{title}{Using Attack-Defense Trees to Analyze Threats and Countermeasures in an {ATM:} {A} Case Study}
\field{year}{2016}
\field{pages}{326\bibrangedash 334}
\range{pages}{9}
\verb{doi}
\verb 10.1007/978-3-319-48393-1\_24
\endverb
\verb{urlraw}
\verb https://doi.org/10.1007/978-3-319-48393-1\_24
\endverb
\verb{url}
\verb https://doi.org/10.1007/978-3-319-48393-1%5C_24
\endverb
\endentry
\entry{gadyatskaya2016}{inbook}{}
\name{author}{6}{}{%
{{hash=e8c9851b54b17fa6ab7290158c810f1e}{%
family={Gadyatskaya},
familyi={G\bibinitperiod},
given={Olga},
giveni={O\bibinitperiod}}}%
{{hash=bd2e8acb930faac9b15c053984a2a326}{%
family={Jhawar},
familyi={J\bibinitperiod},
given={Ravi},
giveni={R\bibinitperiod}}}%
{{hash=0c3f0b43ca33bfb49bda4d847983cc80}{%
family={Kordy},
familyi={K\bibinitperiod},
given={Piotr},
giveni={P\bibinitperiod}}}%
{{hash=1b32b78856519a7c22ee84dec118f486}{%
family={Lounis},
familyi={L\bibinitperiod},
given={Karim},
giveni={K\bibinitperiod}}}%
{{hash=07d4e3cd2ae1cce77c8a3fb46c665f02}{%
family={Mauw},
familyi={M\bibinitperiod},
given={Sjouke},
giveni={S\bibinitperiod}}}%
{{hash=14c979d652d68786f1cb43ce43e71489}{%
family={Trujillo-Rasua},
familyi={T\bibinithyphendelim R\bibinitperiod},
given={Rolando},
giveni={R\bibinitperiod}}}%
}
\list{location}{1}{%
{Cham}%
}
\list{publisher}{1}{%
{Springer}%
}
\strng{namehash}{5acbb4abae9283f815bf3b23dda65652}
\strng{fullhash}{3d312e5d9492c9766458ef312f6ec617}
\strng{bibnamehash}{5acbb4abae9283f815bf3b23dda65652}
\strng{authorbibnamehash}{5acbb4abae9283f815bf3b23dda65652}
\strng{authornamehash}{5acbb4abae9283f815bf3b23dda65652}
\strng{authorfullhash}{3d312e5d9492c9766458ef312f6ec617}
\field{sortinit}{G}
\field{sortinithash}{32d67eca0634bf53703493fb1090a2e8}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{booktitle}{Quantitative Evaluation of Systems {(QEST)}}
\field{isbn}{978-3-319-43425-4}
\field{title}{Attack Trees for Practical Security Assessment: Ranking of Attack Scenarios with ADTool 2.0}
\field{year}{2016}
\field{pages}{159\bibrangedash 162}
\range{pages}{4}
\verb{doi}
\verb 10.1007/978-3-319-43425-4_10
\endverb
\verb{urlraw}
\verb http://dx.doi.org/10.1007/978-3-319-43425-4_10
\endverb
\verb{url}
\verb http://dx.doi.org/10.1007/978-3-319-43425-4_10
\endverb
\endentry
\entry{Gansner93atechnique}{article}{}
\name{author}{4}{}{%
{{hash=52408687e58093ee09b57f27106d74a4}{%
family={Gansner},
familyi={G\bibinitperiod},
given={Emden\bibnamedelima R.},
giveni={E\bibinitperiod\bibinitdelim R\bibinitperiod}}}%
{{hash=c50bf772f00bd5d0fe133a2d300bf385}{%
family={Koutsofios},
familyi={K\bibinitperiod},
given={Eleftherios},
giveni={E\bibinitperiod}}}%
{{hash=e7d5663193f713798fee1607a93ea3db}{%
family={North},
familyi={N\bibinitperiod},
given={Stephen\bibnamedelima C.},
giveni={S\bibinitperiod\bibinitdelim C\bibinitperiod}}}%
{{hash=f094021c8996ca16414379d94d97c3f3}{%
family={Vo},
familyi={V\bibinitperiod},
given={Kiem-phong},
giveni={K\bibinithyphendelim p\bibinitperiod}}}%
}
\strng{namehash}{7d107bd26d5e59d696976d645d650be3}
\strng{fullhash}{1384843b36a39d67e59cca40cb8fa874}
\strng{bibnamehash}{7d107bd26d5e59d696976d645d650be3}
\strng{authorbibnamehash}{7d107bd26d5e59d696976d645d650be3}
\strng{authornamehash}{7d107bd26d5e59d696976d645d650be3}
\strng{authorfullhash}{1384843b36a39d67e59cca40cb8fa874}
\field{sortinit}{G}
\field{sortinithash}{32d67eca0634bf53703493fb1090a2e8}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{journaltitle}{IEEE TRANSACTIONS ON SOFTWARE ENGINEERING}
\field{number}{3}
\field{title}{A Technique for Drawing Directed Graphs}
\field{volume}{19}
\field{year}{1993}
\field{pages}{214\bibrangedash 230}
\range{pages}{17}
\endentry
\entry{hartmanns2014}{inproceedings}{}
\name{author}{2}{}{%
{{hash=5ee8e32c129a82f9fe67944701c268bf}{%
family={Hartmanns},
familyi={H\bibinitperiod},
given={Arnd},
giveni={A\bibinitperiod}}}%
{{hash=b396735e2150877fec4cee61d80d5430}{%
family={Hermanns},
familyi={H\bibinitperiod},
given={Holger},
giveni={H\bibinitperiod}}}%
}
\name{editor}{2}{}{%
{{hash=7fc119e72e6191c643f4e5da5c618c76}{%
family={Ábrahám},
familyi={Á\bibinitperiod},
given={Erika},
giveni={E\bibinitperiod}}}%
{{hash=447759174db1a0695b8fbcfef2e61570}{%
family={Havelund},
familyi={H\bibinitperiod},
given={Klaus},
giveni={K\bibinitperiod}}}%
}
\list{publisher}{1}{%
{Springer}%
}
\strng{namehash}{8dd4c0c9ef28396159be361f38c7afec}
\strng{fullhash}{8dd4c0c9ef28396159be361f38c7afec}
\strng{bibnamehash}{8dd4c0c9ef28396159be361f38c7afec}
\strng{authorbibnamehash}{8dd4c0c9ef28396159be361f38c7afec}
\strng{authornamehash}{8dd4c0c9ef28396159be361f38c7afec}
\strng{authorfullhash}{8dd4c0c9ef28396159be361f38c7afec}
\strng{editorbibnamehash}{e5c303b9034b0da49c14d5c51acec57d}
\strng{editornamehash}{e5c303b9034b0da49c14d5c51acec57d}
\strng{editorfullhash}{e5c303b9034b0da49c14d5c51acec57d}
\field{sortinit}{H}
\field{sortinithash}{23a3aa7c24e56cfa16945d55545109b5}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{booktitle}{Tools and Algorithms for the Construction and Analysis of Systems (TACAS)}
\field{series}{Lecture Notes in Computer Science}
\field{title}{The Modest Toolset: An Integrated Environment for Quantitative Modelling and Verification}
\field{volume}{8413}
\field{year}{2014}
\field{pages}{593\bibrangedash 598}
\range{pages}{6}
\verb{doi}
\verb 10.1007/978-3-642-54862-8\_51
\endverb
\verb{urlraw}
\verb https://doi.org/10.1007/978-3-642-54862-8\_51
\endverb
\verb{url}
\verb https://doi.org/10.1007/978-3-642-54862-8%5C_51
\endverb
\endentry
\entry{hermanns2016}{inproceedings}{}
\name{author}{4}{}{%
{{hash=b396735e2150877fec4cee61d80d5430}{%
family={Hermanns},
familyi={H\bibinitperiod},
given={Holger},
giveni={H\bibinitperiod}}}%
{{hash=ecf130790601f82e902c829ad7570274}{%
family={Krämer},
familyi={K\bibinitperiod},
given={Julia},
giveni={J\bibinitperiod}}}%
{{hash=a2bb16bdae14674186dd61f61d716fff}{%
family={Krcál},
familyi={K\bibinitperiod},
given={Jan},
giveni={J\bibinitperiod}}}%
{{hash=1de27df00ec03386445460a544abaf31}{%
family={Stoelinga},
familyi={S\bibinitperiod},
given={Mariëlle},
giveni={M\bibinitperiod}}}%
}
\strng{namehash}{87c8f268928fb1f3e241e0df9763efa9}
\strng{fullhash}{460caba6cb58f3938a828eed6c48f8fe}
\strng{bibnamehash}{87c8f268928fb1f3e241e0df9763efa9}
\strng{authorbibnamehash}{87c8f268928fb1f3e241e0df9763efa9}
\strng{authornamehash}{87c8f268928fb1f3e241e0df9763efa9}
\strng{authorfullhash}{460caba6cb58f3938a828eed6c48f8fe}
\field{sortinit}{H}
\field{sortinithash}{23a3aa7c24e56cfa16945d55545109b5}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{booktitle}{Principles of Security and Trust {(POST)}}
\field{title}{{The Value of Attack-Defence Diagrams}}
\field{year}{2016}
\field{pages}{163\bibrangedash 185}
\range{pages}{23}
\verb{doi}
\verb 10.1007/978-3-662-49635-0\_9
\endverb
\verb{urlraw}
\verb http://dx.doi.org/10.1007/978-3-662-49635-0\_9
\endverb
\verb{url}
\verb http://dx.doi.org/10.1007/978-3-662-49635-0%5C_9
\endverb
\endentry
\entry{houmer2020}{article}{}
\name{author}{2}{}{%
{{hash=d9fac79f18d8a1bbb04eeede73a4478c}{%
family={Houmer},
familyi={H\bibinitperiod},
given={Meriem},
giveni={M\bibinitperiod}}}%
{{hash=41d5a0d54a358ea8d7c1497cdd8634af}{%
family={Hasnaoui},
familyi={H\bibinitperiod},
given={Moulay\bibnamedelima Lahcen},
giveni={M\bibinitperiod\bibinitdelim L\bibinitperiod}}}%
}
\strng{namehash}{17086e5bd5b9a72c7f4fd1940b62080b}
\strng{fullhash}{17086e5bd5b9a72c7f4fd1940b62080b}
\strng{bibnamehash}{17086e5bd5b9a72c7f4fd1940b62080b}
\strng{authorbibnamehash}{17086e5bd5b9a72c7f4fd1940b62080b}
\strng{authornamehash}{17086e5bd5b9a72c7f4fd1940b62080b}
\strng{authorfullhash}{17086e5bd5b9a72c7f4fd1940b62080b}
\field{sortinit}{H}
\field{sortinithash}{23a3aa7c24e56cfa16945d55545109b5}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{journaltitle}{International Journal of Electrical \& Computer Engineering (2088-8708)}
\field{number}{6}
\field{title}{A risk and security assessment of VANET availability using attack tree concept.}
\field{volume}{10}
\field{year}{2020}
\endentry
\entry{hughes2010}{book}{}
\name{author}{2}{}{%
{{hash=a7f6ea810c92e923e7b12ce8748bc904}{%
family={Hughes},
familyi={H\bibinitperiod},
given={Ifan},
giveni={I\bibinitperiod}}}%
{{hash=1ae4d38d473221b1dfa3cb416a29ebb5}{%
family={Hase},
familyi={H\bibinitperiod},
given={Thomas},
giveni={T\bibinitperiod}}}%
}
\list{publisher}{1}{%
{Oxford University Press}%
}
\strng{namehash}{e861172396e70b8edde933cbddf791f8}
\strng{fullhash}{e861172396e70b8edde933cbddf791f8}
\strng{bibnamehash}{e861172396e70b8edde933cbddf791f8}
\strng{authorbibnamehash}{e861172396e70b8edde933cbddf791f8}
\strng{authornamehash}{e861172396e70b8edde933cbddf791f8}
\strng{authorfullhash}{e861172396e70b8edde933cbddf791f8}
\field{sortinit}{H}
\field{sortinithash}{23a3aa7c24e56cfa16945d55545109b5}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{title}{Measurements and their uncertainties: a practical guide to modern error analysis}
\field{year}{2010}
\endentry
\entry{jhawar2015}{inproceedings}{}
\name{author}{5}{}{%
{{hash=bd2e8acb930faac9b15c053984a2a326}{%
family={Jhawar},
familyi={J\bibinitperiod},
given={Ravi},
giveni={R\bibinitperiod}}}%
{{hash=5832da64bd42a134ab4cf82336226ba5}{%
family={Kordy},
familyi={K\bibinitperiod},
given={Barbara},
giveni={B\bibinitperiod}}}%
{{hash=07d4e3cd2ae1cce77c8a3fb46c665f02}{%
family={Mauw},
familyi={M\bibinitperiod},
given={Sjouke},
giveni={S\bibinitperiod}}}%
{{hash=c1e8495a0f610edca69daa1bd2701119}{%
family={Radomirović},
familyi={R\bibinitperiod},
given={Saša},
giveni={S\bibinitperiod}}}%
{{hash=14c979d652d68786f1cb43ce43e71489}{%
family={Trujillo-Rasua},
familyi={T\bibinithyphendelim R\bibinitperiod},
given={Rolando},
giveni={R\bibinitperiod}}}%
}
\list{organization}{1}{%
{Springer}%
}
\strng{namehash}{3c77c90b0c13e0ef9b65b83d4e08aab6}
\strng{fullhash}{d1c9359d3da06096fb5c8efca4978ed0}
\strng{bibnamehash}{3c77c90b0c13e0ef9b65b83d4e08aab6}
\strng{authorbibnamehash}{3c77c90b0c13e0ef9b65b83d4e08aab6}
\strng{authornamehash}{3c77c90b0c13e0ef9b65b83d4e08aab6}
\strng{authorfullhash}{d1c9359d3da06096fb5c8efca4978ed0}
\field{sortinit}{J}
\field{sortinithash}{b2f54a9081ace9966a7cb9413811edb4}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{booktitle}{IFIP International Information Security and Privacy Conference}
\field{title}{Attack trees with sequential conjunction}
\field{year}{2015}
\field{pages}{339\bibrangedash 353}
\range{pages}{15}
\endentry
\entry{kim2020b}{article}{}
\name{author}{3}{}{%
{{hash=4a86c7192c3f9848ecdd935b4fcad324}{%
family={Kim},
familyi={K\bibinitperiod},
given={Dong-won},
giveni={D\bibinithyphendelim w\bibinitperiod}}}%
{{hash=fae0d31185283f62cb25ac0cf4ca76ac}{%
family={Choi},
familyi={C\bibinitperiod},
given={Jin-young},
giveni={J\bibinithyphendelim y\bibinitperiod}}}%
{{hash=b841db0f7b6d5a9fa69d5cf59a85c4d1}{%
family={Han},
familyi={H\bibinitperiod},
given={Keun-hee},
giveni={K\bibinithyphendelim h\bibinitperiod}}}%
}
\list{publisher}{1}{%
{BioMed Central}%
}
\strng{namehash}{31ef18c4f6e9aad24107f3a0dcfeb9fd}
\strng{fullhash}{31ef18c4f6e9aad24107f3a0dcfeb9fd}
\strng{bibnamehash}{31ef18c4f6e9aad24107f3a0dcfeb9fd}
\strng{authorbibnamehash}{31ef18c4f6e9aad24107f3a0dcfeb9fd}
\strng{authornamehash}{31ef18c4f6e9aad24107f3a0dcfeb9fd}
\strng{authorfullhash}{31ef18c4f6e9aad24107f3a0dcfeb9fd}
\field{sortinit}{K}
\field{sortinithash}{c02bf6bff1c488450c352b40f5d853ab}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{journaltitle}{BMC Medical Informatics and Decision Making}
\field{number}{1}
\field{title}{Risk management-based security evaluation model for telemedicine systems}
\field{volume}{20}
\field{year}{2020}
\field{pages}{1\bibrangedash 14}
\range{pages}{14}
\endentry
\entry{kim2020}{incollection}{}
\name{author}{2}{}{%
{{hash=1b2a9fece4f141830ed4a8879977d01c}{%
family={Kim},
familyi={K\bibinitperiod},
given={Shiho},
giveni={S\bibinitperiod}}}%
{{hash=84f49486ce3c0340e6c102086fd6845d}{%
family={Shrestha},
familyi={S\bibinitperiod},
given={Rakesh},
giveni={R\bibinitperiod}}}%
}
\list{publisher}{1}{%
{Springer}%
}
\strng{namehash}{ed1a2b4d3ae8f1dfeeef0398f3b05096}
\strng{fullhash}{ed1a2b4d3ae8f1dfeeef0398f3b05096}
\strng{bibnamehash}{ed1a2b4d3ae8f1dfeeef0398f3b05096}
\strng{authorbibnamehash}{ed1a2b4d3ae8f1dfeeef0398f3b05096}
\strng{authornamehash}{ed1a2b4d3ae8f1dfeeef0398f3b05096}
\strng{authorfullhash}{ed1a2b4d3ae8f1dfeeef0398f3b05096}
\field{sortinit}{K}
\field{sortinithash}{c02bf6bff1c488450c352b40f5d853ab}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{booktitle}{Automotive Cyber Security}
\field{title}{Security and Privacy in Intelligent Autonomous Vehicles}
\field{year}{2020}
\field{pages}{35\bibrangedash 66}
\range{pages}{32}
\endentry
\entry{kordy2013}{article}{}
\name{author}{3}{}{%
{{hash=5832da64bd42a134ab4cf82336226ba5}{%
family={Kordy},
familyi={K\bibinitperiod},
given={Barbara},
giveni={B\bibinitperiod}}}%
{{hash=31e0ae3df94ce637f4c3ba58019187a4}{%
family={Pietre-Cambacedes},
familyi={P\bibinithyphendelim C\bibinitperiod},
given={Ludovic},
giveni={L\bibinitperiod}}}%
{{hash=12ae6ac6dd6cd511a33ca1caa5093ce3}{%
family={Schweitzer},
familyi={S\bibinitperiod},
given={Patrick},
giveni={P\bibinitperiod}}}%
}
\strng{namehash}{efbd5d9777ea6b40b24a6ec2296c9507}
\strng{fullhash}{efbd5d9777ea6b40b24a6ec2296c9507}
\strng{bibnamehash}{efbd5d9777ea6b40b24a6ec2296c9507}
\strng{authorbibnamehash}{efbd5d9777ea6b40b24a6ec2296c9507}
\strng{authornamehash}{efbd5d9777ea6b40b24a6ec2296c9507}
\strng{authorfullhash}{efbd5d9777ea6b40b24a6ec2296c9507}
\field{sortinit}{K}
\field{sortinithash}{c02bf6bff1c488450c352b40f5d853ab}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{journaltitle}{CoRR}
\field{title}{DAG-Based Attack and Defense Modeling: Don't Miss the Forest for the Attack Trees}
\field{volume}{abs/1303.7397}
\field{year}{2013}
\verb{urlraw}
\verb http://arxiv.org/abs/1303.7397
\endverb
\verb{url}
\verb http://arxiv.org/abs/1303.7397
\endverb
\endentry
\entry{kordy2018}{inproceedings}{}
\name{author}{2}{}{%
{{hash=5832da64bd42a134ab4cf82336226ba5}{%
family={Kordy},
familyi={K\bibinitperiod},
given={Barbara},
giveni={B\bibinitperiod}}}%
{{hash=e016db57ad3c74fc0222ca4cc6e027af}{%
family={Wide{ł}},
familyi={W\bibinitperiod},
given={Wojciech},
giveni={W\bibinitperiod}}}%
}
\name{editor}{2}{}{%
{{hash=0fddc2a59cf81f3ad0ba2cfde598ee2a}{%
family={Bauer},
familyi={B\bibinitperiod},
given={Lujo},
giveni={L\bibinitperiod}}}%
{{hash=b7d2dedb64572e046a0efa6112d19545}{%
family={Küsters},
familyi={K\bibinitperiod},
given={Ralf},
giveni={R\bibinitperiod}}}%
}
\list{location}{1}{%
{Cham}%
}
\list{publisher}{1}{%
{Springer International Publishing}%
}
\strng{namehash}{2bb949f04e14073139f03c0e9e3d014e}
\strng{fullhash}{2bb949f04e14073139f03c0e9e3d014e}
\strng{bibnamehash}{2bb949f04e14073139f03c0e9e3d014e}
\strng{authorbibnamehash}{2bb949f04e14073139f03c0e9e3d014e}
\strng{authornamehash}{2bb949f04e14073139f03c0e9e3d014e}
\strng{authorfullhash}{2bb949f04e14073139f03c0e9e3d014e}
\strng{editorbibnamehash}{009b7454ac090d73f8959309cea03041}
\strng{editornamehash}{009b7454ac090d73f8959309cea03041}
\strng{editorfullhash}{009b7454ac090d73f8959309cea03041}
\field{sortinit}{K}
\field{sortinithash}{c02bf6bff1c488450c352b40f5d853ab}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{booktitle}{Principles of Security and Trust (POST)}
\field{isbn}{978-3-319-89722-6}
\field{title}{On Quantitative Analysis of Attack--Defense Trees with Repeated Labels}
\field{year}{2018}
\field{pages}{325\bibrangedash 346}
\range{pages}{22}
\endentry
\entry{kordy2011}{inproceedings}{}
\name{author}{4}{}{%
{{hash=5832da64bd42a134ab4cf82336226ba5}{%
family={Kordy},
familyi={K\bibinitperiod},
given={Barbara},
giveni={B\bibinitperiod}}}%
{{hash=07d4e3cd2ae1cce77c8a3fb46c665f02}{%
family={Mauw},
familyi={M\bibinitperiod},
given={Sjouke},
giveni={S\bibinitperiod}}}%
{{hash=c1e8495a0f610edca69daa1bd2701119}{%
family={Radomirović},
familyi={R\bibinitperiod},
given={Saša},
giveni={S\bibinitperiod}}}%
{{hash=12ae6ac6dd6cd511a33ca1caa5093ce3}{%
family={Schweitzer},
familyi={S\bibinitperiod},
given={Patrick},
giveni={P\bibinitperiod}}}%
}
\list{location}{1}{%
{Pisa, Italy}%
}
\list{publisher}{1}{%
{Springer-Verlag}%
}
\strng{namehash}{9607d2f80e9c7ab3ca4387f158e574e7}
\strng{fullhash}{ca4117e25b52c1785ee8a646e3047929}
\strng{bibnamehash}{9607d2f80e9c7ab3ca4387f158e574e7}
\strng{authorbibnamehash}{9607d2f80e9c7ab3ca4387f158e574e7}
\strng{authornamehash}{9607d2f80e9c7ab3ca4387f158e574e7}
\strng{authorfullhash}{ca4117e25b52c1785ee8a646e3047929}
\field{sortinit}{K}
\field{sortinithash}{c02bf6bff1c488450c352b40f5d853ab}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{booktitle}{Proceedings of the 7th International Conference on Formal Aspects of Security and Trust}
\field{isbn}{978-3-642-19750-5}
\field{series}{FAST'10}
\field{title}{Foundations of Attack-Defense Trees}
\field{year}{2011}
\field{pages}{80\bibrangedash 95}
\range{pages}{16}
\verb{urlraw}
\verb http://dl.acm.org/citation.cfm?id=1964555.1964561
\endverb
\verb{url}
\verb http://dl.acm.org/citation.cfm?id=1964555.1964561
\endverb
\endentry
\entry{krichen2019}{inproceedings}{}
\name{author}{2}{}{%
{{hash=4a5234448d48615df3855750e6f84e71}{%
family={Krichen},
familyi={K\bibinitperiod},
given={Moez},
giveni={M\bibinitperiod}}}%
{{hash=d445b53cd7d79bf04610d0bca0f88693}{%
family={Alroobaea},
familyi={A\bibinitperiod},
given={Roobaea},
giveni={R\bibinitperiod}}}%
}
\list{organization}{2}{%
{SCITEPRESS-Science}%
{Technology Publications, Lda}%
}
\strng{namehash}{8019dbef41dfcda963189a461eb7c2b6}
\strng{fullhash}{8019dbef41dfcda963189a461eb7c2b6}
\strng{bibnamehash}{8019dbef41dfcda963189a461eb7c2b6}
\strng{authorbibnamehash}{8019dbef41dfcda963189a461eb7c2b6}
\strng{authornamehash}{8019dbef41dfcda963189a461eb7c2b6}
\strng{authorfullhash}{8019dbef41dfcda963189a461eb7c2b6}
\field{sortinit}{K}
\field{sortinithash}{c02bf6bff1c488450c352b40f5d853ab}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{booktitle}{Proceedings of the 14th International Conference on Evaluation of Novel Approaches to Software Engineering}
\field{title}{A New Model-based Framework for Testing Security of IoT Systems in Smart Cities using Attack Trees and Price Timed Automata}
\field{year}{2019}
\field{pages}{570\bibrangedash 577}
\range{pages}{8}
\endentry
\entry{kumar2015}{inproceedings}{}
\name{author}{3}{}{%
{{hash=5dbaee2bd1f68bfb2185d56f91e4b038}{%
family={Kumar},
familyi={K\bibinitperiod},
given={Rajesh},
giveni={R\bibinitperiod}}}%
{{hash=195ebb88fb7b5521b58de1a26e9d80ee}{%
family={Ruijters},
familyi={R\bibinitperiod},
given={Enno},
giveni={E\bibinitperiod}}}%
{{hash=1de27df00ec03386445460a544abaf31}{%
family={Stoelinga},
familyi={S\bibinitperiod},
given={Mariëlle},
giveni={M\bibinitperiod}}}%
}
\strng{namehash}{d9b4dc97490c21fb5ad0fc2a1344ea61}
\strng{fullhash}{d9b4dc97490c21fb5ad0fc2a1344ea61}
\strng{bibnamehash}{d9b4dc97490c21fb5ad0fc2a1344ea61}
\strng{authorbibnamehash}{d9b4dc97490c21fb5ad0fc2a1344ea61}
\strng{authornamehash}{d9b4dc97490c21fb5ad0fc2a1344ea61}
\strng{authorfullhash}{d9b4dc97490c21fb5ad0fc2a1344ea61}
\field{sortinit}{K}
\field{sortinithash}{c02bf6bff1c488450c352b40f5d853ab}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{booktitle}{Formal Modeling and Analysis of Timed Systems (FORMATS)}
\field{title}{Quantitative Attack Tree Analysis via Priced Timed Automata}
\field{year}{2015}
\field{pages}{156\bibrangedash 171}
\range{pages}{16}
\verb{doi}
\verb 10.1007/978-3-319-22975-1\_11
\endverb
\verb{urlraw}
\verb https://doi.org/10.1007/978-3-319-22975-1\_11
\endverb
\verb{url}
\verb https://doi.org/10.1007/978-3-319-22975-1%5C_11
\endverb
\endentry
\entry{kumar2017}{inproceedings}{}
\name{author}{2}{}{%
{{hash=5dbaee2bd1f68bfb2185d56f91e4b038}{%
family={Kumar},
familyi={K\bibinitperiod},
given={Rajesh},
giveni={R\bibinitperiod}}}%
{{hash=1de27df00ec03386445460a544abaf31}{%
family={Stoelinga},
familyi={S\bibinitperiod},
given={Mariëlle},
giveni={M\bibinitperiod}}}%
}
\strng{namehash}{76d9398c5e1538bd4e97b88b3d594fa8}
\strng{fullhash}{76d9398c5e1538bd4e97b88b3d594fa8}
\strng{bibnamehash}{76d9398c5e1538bd4e97b88b3d594fa8}
\strng{authorbibnamehash}{76d9398c5e1538bd4e97b88b3d594fa8}
\strng{authornamehash}{76d9398c5e1538bd4e97b88b3d594fa8}
\strng{authorfullhash}{76d9398c5e1538bd4e97b88b3d594fa8}
\field{sortinit}{K}
\field{sortinithash}{c02bf6bff1c488450c352b40f5d853ab}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{booktitle}{High Assurance Systems Engineering (HASE)}
\field{title}{Quantitative Security and Safety Analysis with Attack-Fault Trees}
\field{year}{2017}
\field{pages}{25\bibrangedash 32}
\range{pages}{8}
\verb{doi}
\verb 10.1109/HASE.2017.12
\endverb
\verb{urlraw}
\verb https://doi.org/10.1109/HASE.2017.12
\endverb
\verb{url}
\verb https://doi.org/10.1109/HASE.2017.12
\endverb
\endentry
\entry{kwiatkowska2011}{inproceedings}{}
\name{author}{3}{}{%
{{hash=44f96ce7a6edd0d0f29170daeee1d90f}{%
family={{K}wiatkowska},
familyi={K\bibinitperiod},
given={{M}.},
giveni={M\bibinitperiod}}}%
{{hash=7b8e0ec03ceca0175c0dbf3a93fff279}{%
family={{N}orman},
familyi={N\bibinitperiod},
given={{G}.},
giveni={G\bibinitperiod}}}%
{{hash=8f917e59f9bcb671f7f68671bf759fe7}{%
family={{P}arker},
familyi={P\bibinitperiod},
given={{D}.},
giveni={D\bibinitperiod}}}%
}
\list{publisher}{1}{%
{Springer}%
}
\strng{namehash}{377f3d27cdd43e104070d4b5ded61ee0}
\strng{fullhash}{377f3d27cdd43e104070d4b5ded61ee0}
\strng{bibnamehash}{377f3d27cdd43e104070d4b5ded61ee0}
\strng{authorbibnamehash}{377f3d27cdd43e104070d4b5ded61ee0}
\strng{authornamehash}{377f3d27cdd43e104070d4b5ded61ee0}
\strng{authorfullhash}{377f3d27cdd43e104070d4b5ded61ee0}
\field{sortinit}{K}
\field{sortinithash}{c02bf6bff1c488450c352b40f5d853ab}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{booktitle}{Proc. 23rd International Conference on Computer Aided Verification (CAV'11)}
\field{series}{LNCS}
\field{title}{{PRISM} 4.0: {V}erification of {P}robabilistic {R}eal-time {S}ystems}
\field{volume}{6806}
\field{year}{2011}
\field{pages}{585\bibrangedash 591}
\range{pages}{7}
\endentry
\entry{lopez2012}{inproceedings}{}
\name{author}{4}{}{%
{{hash=184f057e42d50a48f1c7235832cfaddf}{%
family={Lopez},
familyi={L\bibinitperiod},
given={J},
giveni={J\bibinitperiod}}}%
{{hash=ef63b9183fefe09c396cbc20b6f88a1d}{%
family={Nielsen},
familyi={N\bibinitperiod},
given={Jason},
giveni={J\bibinitperiod}}}%
{{hash=1ed1a1ddfe5af141359c100aecf2aa1c}{%
family={Hemmes},
familyi={H\bibinitperiod},
given={Jeffrey},
giveni={J\bibinitperiod}}}%
{{hash=be1f9465338dfb11fe2ff63bc12866c5}{%
family={Humphries},
familyi={H\bibinitperiod},
given={Jeffrey},
giveni={J\bibinitperiod}}}%
}
\strng{namehash}{aeffaa8517b243cc991c6559cefd3a1f}
\strng{fullhash}{6abba4d658e84f81c62ad64acc78cbdb}
\strng{bibnamehash}{aeffaa8517b243cc991c6559cefd3a1f}
\strng{authorbibnamehash}{aeffaa8517b243cc991c6559cefd3a1f}
\strng{authornamehash}{aeffaa8517b243cc991c6559cefd3a1f}
\strng{authorfullhash}{6abba4d658e84f81c62ad64acc78cbdb}
\field{sortinit}{L}
\field{sortinithash}{7c47d417cecb1f4bd38d1825c427a61a}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{booktitle}{Proceedings of the 7th International Conference on Information Warfare and Security}
\field{title}{Using Attack Trees to Assess Security Controls for Supervisory Control and Data Acquisition Systems (SCADA)}
\field{year}{2012}
\field{pages}{166\bibrangedash 177}
\range{pages}{12}
\endentry
\entry{lopuhaa2022efficient}{article}{}
\name{author}{3}{}{%
{{hash=e5e19a7f841e4ddad7f431aa8acf3455}{%
family={Lopuhaä-Zwakenberg},
familyi={L\bibinithyphendelim Z\bibinitperiod},
given={Milan},
giveni={M\bibinitperiod}}}%
{{hash=ed94d773d693a01aa6ee5a7592095934}{%
family={Budde},
familyi={B\bibinitperiod},
given={Carlos\bibnamedelima E},
giveni={C\bibinitperiod\bibinitdelim E\bibinitperiod}}}%
{{hash=1de27df00ec03386445460a544abaf31}{%
family={Stoelinga},
familyi={S\bibinitperiod},
given={Mariëlle},
giveni={M\bibinitperiod}}}%
}
\list{publisher}{1}{%
{IEEE}%
}
\strng{namehash}{19461262aa4269dcabe19b0c727472e2}
\strng{fullhash}{19461262aa4269dcabe19b0c727472e2}
\strng{bibnamehash}{19461262aa4269dcabe19b0c727472e2}
\strng{authorbibnamehash}{19461262aa4269dcabe19b0c727472e2}
\strng{authornamehash}{19461262aa4269dcabe19b0c727472e2}
\strng{authorfullhash}{19461262aa4269dcabe19b0c727472e2}
\field{sortinit}{L}
\field{sortinithash}{7c47d417cecb1f4bd38d1825c427a61a}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{journaltitle}{IEEE Transactions on Dependable and Secure Computing}
\field{title}{Efficient and generic algorithms for quantitative attack tree analysis}
\field{year}{2022}
\endentry
\entry{mauw2005}{inproceedings}{}
\name{author}{2}{}{%
{{hash=07d4e3cd2ae1cce77c8a3fb46c665f02}{%
family={Mauw},
familyi={M\bibinitperiod},
given={Sjouke},
giveni={S\bibinitperiod}}}%
{{hash=9e3c715121c7051b238419e5cbc36e59}{%
family={Oostdijk},
familyi={O\bibinitperiod},
given={Martijn},
giveni={M\bibinitperiod}}}%
}
\list{location}{1}{%
{Seoul, Korea}%
}
\list{publisher}{1}{%
{Springer-Verlag}%
}
\strng{namehash}{3f9d98b490d5571ce162c9a85717e332}
\strng{fullhash}{3f9d98b490d5571ce162c9a85717e332}
\strng{bibnamehash}{3f9d98b490d5571ce162c9a85717e332}
\strng{authorbibnamehash}{3f9d98b490d5571ce162c9a85717e332}
\strng{authornamehash}{3f9d98b490d5571ce162c9a85717e332}
\strng{authorfullhash}{3f9d98b490d5571ce162c9a85717e332}
\field{sortinit}{M}
\field{sortinithash}{4625c616857f13d17ce56f7d4f97d451}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{booktitle}{Proceedings of the 8th International Conference on Information Security and Cryptology}
\field{series}{ICISC'05}
\field{title}{Foundations of Attack Trees}
\field{year}{2006}
\field{pages}{186\bibrangedash 198}
\range{pages}{13}
\verb{doi}
\verb 10.1007/11734727_17
\endverb
\verb{urlraw}
\verb http://dx.doi.org/10.1007/11734727_17
\endverb
\verb{url}
\verb http://dx.doi.org/10.1007/11734727_17
\endverb
\keyw{attack trees,semantics,threat analysis}
\endentry
\entry{arimarental}{article}{}
\name{author}{2}{}{%
{{hash=85a9cbf36165169543dffb148bbf200b}{%
family={McGough},
familyi={M\bibinitperiod},
given={Tony},
giveni={T\bibinitperiod}}}%
{{hash=710d3079a2ff1876c264c14cbd8893d6}{%
family={Tsolacos},
familyi={T\bibinitperiod},
given={Sotiris},
giveni={S\bibinitperiod}}}%
}
\list{publisher}{1}{%
{MCB UP Ltd}%
}
\strng{namehash}{fccd92dab504af166757602d00edec6c}
\strng{fullhash}{fccd92dab504af166757602d00edec6c}
\strng{bibnamehash}{fccd92dab504af166757602d00edec6c}
\strng{authorbibnamehash}{fccd92dab504af166757602d00edec6c}
\strng{authornamehash}{fccd92dab504af166757602d00edec6c}
\strng{authorfullhash}{fccd92dab504af166757602d00edec6c}
\field{sortinit}{M}
\field{sortinithash}{4625c616857f13d17ce56f7d4f97d451}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{journaltitle}{Journal of Property Valuation and Investment}
\field{title}{Forecasting commercial rental values using ARIMA models}
\field{year}{1995}
\endentry
\entry{mcqueen2006}{inproceedings}{}
\name{author}{4}{}{%
{{hash=374927aee2924118563a1b6df19dd651}{%
family={McQueen},
familyi={M\bibinitperiod},
given={Miles\bibnamedelima A.},
giveni={M\bibinitperiod\bibinitdelim A\bibinitperiod}}}%
{{hash=dcde859a157236bc58176228f302a917}{%
family={Boyer},
familyi={B\bibinitperiod},
given={Wayne\bibnamedelima F.},
giveni={W\bibinitperiod\bibinitdelim F\bibinitperiod}}}%
{{hash=424f49cd37402344ad8645cdec63f598}{%
family={Flynn},
familyi={F\bibinitperiod},
given={Mark\bibnamedelima A.},
giveni={M\bibinitperiod\bibinitdelim A\bibinitperiod}}}%
{{hash=4b621a72999b3c379ab8dd849f7708e6}{%
family={Beitel},
familyi={B\bibinitperiod},
given={George\bibnamedelima A.},
giveni={G\bibinitperiod\bibinitdelim A\bibinitperiod}}}%
}
\list{location}{1}{%
{Washington, DC, USA}%
}
\list{publisher}{1}{%
{IEEE Computer Society}%
}
\strng{namehash}{28c219f5ae5b3e1545d7e8451e908050}
\strng{fullhash}{9e591fdc2d3cc2ab9235de6e6dc72625}
\strng{bibnamehash}{28c219f5ae5b3e1545d7e8451e908050}
\strng{authorbibnamehash}{28c219f5ae5b3e1545d7e8451e908050}
\strng{authornamehash}{28c219f5ae5b3e1545d7e8451e908050}
\strng{authorfullhash}{9e591fdc2d3cc2ab9235de6e6dc72625}
\field{sortinit}{M}
\field{sortinithash}{4625c616857f13d17ce56f7d4f97d451}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{booktitle}{Hawaii International Conference on System Sciences (HICSS)}
\field{isbn}{0-7695-2507-5}
\field{series}{HICSS '06}
\field{title}{Quantitative Cyber Risk Reduction Estimation Methodology for a Small SCADA Control System}
\field{year}{2006}
\field{pages}{226\bibrangedash}
\range{pages}{-1}
\verb{doi}
\verb 10.1109/HICSS.2006.405
\endverb
\verb{urlraw}
\verb http://dx.doi.org/10.1109/HICSS.2006.405
\endverb
\verb{url}
\verb http://dx.doi.org/10.1109/HICSS.2006.405
\endverb
\endentry
\entry{mezei2011}{article}{}
\name{author}{1}{}{%
{{hash=653e5e5cc9b4bf980b217ec340613569}{%
family={Mezei},
familyi={M\bibinitperiod},
given={Alessandro\bibnamedelimb Buoni;\bibnamedelimb Mario\bibnamedelimb Fedrizzi;\bibnamedelima Jozsef},
giveni={A\bibinitperiod\bibinitdelim B\bibinitperiod\bibinitdelim M\bibinitperiod\bibinitdelim F\bibinitperiod\bibinitdelim J\bibinitperiod}}}%
}
\list{publisher}{1}{%
{Inderscience Publishers}%
}
\strng{namehash}{653e5e5cc9b4bf980b217ec340613569}
\strng{fullhash}{653e5e5cc9b4bf980b217ec340613569}
\strng{bibnamehash}{653e5e5cc9b4bf980b217ec340613569}
\strng{authorbibnamehash}{653e5e5cc9b4bf980b217ec340613569}
\strng{authornamehash}{653e5e5cc9b4bf980b217ec340613569}
\strng{authorfullhash}{653e5e5cc9b4bf980b217ec340613569}
\field{sortinit}{M}
\field{sortinithash}{4625c616857f13d17ce56f7d4f97d451}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{journaltitle}{International Journal of Electronic Business}
\field{number}{3}
\field{title}{Combining attack trees and fuzzy numbers in a multi-agent approach to fraud detection}
\field{volume}{9}
\field{year}{2011}
\field{pages}{186\bibrangedash 202}
\range{pages}{17}
\endentry
\entry{nato2008}{report}{}
\name{author}{1}{}{%
{{hash=31b48700ac0efac237e148f2e6d55202}{%
family={NATO},
familyi={N\bibinitperiod},
given={RTO},
giveni={R\bibinitperiod}}}%
}
\list{institution}{2}{%
{RTO Technical Report TR-IST-049, Research}%
{Technology Organisation of NATO}%
}
\strng{namehash}{31b48700ac0efac237e148f2e6d55202}
\strng{fullhash}{31b48700ac0efac237e148f2e6d55202}
\strng{bibnamehash}{31b48700ac0efac237e148f2e6d55202}
\strng{authorbibnamehash}{31b48700ac0efac237e148f2e6d55202}
\strng{authornamehash}{31b48700ac0efac237e148f2e6d55202}
\strng{authorfullhash}{31b48700ac0efac237e148f2e6d55202}
\field{sortinit}{N}
\field{sortinithash}{22369a73d5f88983a108b63f07f37084}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{title}{Improving Common Security Risk Analysis}
\field{type}{techreport}
\field{year}{2008}
\endentry
\entry{ohm2020}{article}{}
\name{author}{4}{}{%
{{hash=f03d63f5798bc09f1734e40ffb0d7eda}{%
family={Ohm},
familyi={O\bibinitperiod},
given={Marc},
giveni={M\bibinitperiod}}}%
{{hash=410e602a3d4c75f6f56d51ba0671fe9c}{%
family={Plate},
familyi={P\bibinitperiod},
given={Henrik},
giveni={H\bibinitperiod}}}%
{{hash=7fed674f2ff1cdda2a9f1194513dcffb}{%
family={Sykosch},
familyi={S\bibinitperiod},
given={Arnold},
giveni={A\bibinitperiod}}}%
{{hash=f52c1a7e4268a61272473c0e816dac99}{%
family={Meier},
familyi={M\bibinitperiod},
given={Michael},
giveni={M\bibinitperiod}}}%
}
\strng{namehash}{a541a86f5262256aecbfa4b93ea9b053}
\strng{fullhash}{522a49390aa106694174957008f6b6cc}
\strng{bibnamehash}{a541a86f5262256aecbfa4b93ea9b053}
\strng{authorbibnamehash}{a541a86f5262256aecbfa4b93ea9b053}
\strng{authornamehash}{a541a86f5262256aecbfa4b93ea9b053}
\strng{authorfullhash}{522a49390aa106694174957008f6b6cc}
\field{sortinit}{O}
\field{sortinithash}{2cd7140a07aea5341f9e2771efe90aae}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{journaltitle}{arXiv preprint arXiv:2005.09535}
\field{title}{Backstabber's Knife Collection: A Review of Open Source Software Supply Chain Attacks}
\field{year}{2020}
\endentry
\entry{pekergin2016}{inproceedings}{}
\name{author}{3}{}{%
{{hash=9be42100415e415526382ff183356bf3}{%
family={Pekergin},
familyi={P\bibinitperiod},
given={Nihal},
giveni={N\bibinitperiod}}}%
{{hash=a96a98c72248693687dd78d98fb0b22c}{%
family={Tan},
familyi={T\bibinitperiod},
given={Sovanna},
giveni={S\bibinitperiod}}}%
{{hash=55ebc47d829525a4cd5fc56994c6709b}{%
family={Fourneau},
familyi={F\bibinitperiod},
given={Jean-Michel},
giveni={J\bibinithyphendelim M\bibinitperiod}}}%
}
\list{organization}{1}{%
{Springer}%
}
\strng{namehash}{e56b53fb37cff88fbb9889b8353834e6}
\strng{fullhash}{e56b53fb37cff88fbb9889b8353834e6}
\strng{bibnamehash}{e56b53fb37cff88fbb9889b8353834e6}
\strng{authorbibnamehash}{e56b53fb37cff88fbb9889b8353834e6}
\strng{authornamehash}{e56b53fb37cff88fbb9889b8353834e6}
\strng{authorfullhash}{e56b53fb37cff88fbb9889b8353834e6}
\field{sortinit}{P}
\field{sortinithash}{ff3bcf24f47321b42cb156c2cc8a8422}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{booktitle}{International Workshop on Graphical Models for Security}
\field{title}{Quantitative Attack Tree Analysis: Stochastic Bounds and Numerical Analysis}
\field{year}{2016}
\field{pages}{119\bibrangedash 133}
\range{pages}{15}
\endentry
\entry{ramos2020}{article}{}
\name{author}{2}{}{%
{{hash=4d88a0de1de4a2f9257ca2a23704d2eb}{%
family={Ramos},
familyi={R\bibinitperiod},
given={JLH},
giveni={J\bibinitperiod}}}%
{{hash=1e9497794d01ccbdbd80d9d3da5992fe}{%
family={Skarmeta},
familyi={S\bibinitperiod},
given={A},
giveni={A\bibinitperiod}}}%
}
\list{publisher}{1}{%
{IOS Press}%
}
\strng{namehash}{adfa28f0bc6459958b475c280320d988}
\strng{fullhash}{adfa28f0bc6459958b475c280320d988}
\strng{bibnamehash}{adfa28f0bc6459958b475c280320d988}
\strng{authorbibnamehash}{adfa28f0bc6459958b475c280320d988}
\strng{authornamehash}{adfa28f0bc6459958b475c280320d988}
\strng{authorfullhash}{adfa28f0bc6459958b475c280320d988}
\field{sortinit}{R}
\field{sortinithash}{5e1c39a9d46ffb6bebd8f801023a9486}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{journaltitle}{Security and Privacy in the Internet of Things: Challenges and Solutions}
\field{title}{Assessing Vulnerabilities in IoT-Based Ambient Assisted Living Systems}
\field{volume}{27}
\field{year}{2020}
\field{pages}{94}
\range{pages}{1}
\endentry
\entry{roblesmodel}{article}{}
\name{author}{7}{}{%
{{hash=08048420f422d24a70e66bb146ad7325}{%
family={Robles-Ramirez},
familyi={R\bibinithyphendelim R\bibinitperiod},
given={David},
giveni={D\bibinitperiod}}}%
{{hash=1d2152e394868565623a2b8a35ef184e}{%
family={Tryfonas},
familyi={T\bibinitperiod},
given={Theo},
giveni={T\bibinitperiod}}}%
{{hash=160c05854a5bc310df6b2c64dedcc98e}{%
family={Escamilla-Ambrosio},
familyi={E\bibinithyphendelim A\bibinitperiod},
given={Ponciano\bibnamedelima J},
giveni={P\bibinitperiod\bibinitdelim J\bibinitperiod}}}%
{{hash=96c30860850a74daa5263cf266dc662f}{%
family={Fagade},
familyi={F\bibinitperiod},
given={Tesleem},
giveni={T\bibinitperiod}}}%
{{hash=c784a98e2906c24063b0a6828fac612d}{%
family={Anastasopoulou},
familyi={A\bibinitperiod},
given={Kalliopi},
giveni={K\bibinitperiod}}}%
{{hash=96e27249b5fbe3758d917fd5a5abe645}{%
family={Tassi},
familyi={T\bibinitperiod},
given={Andrea},
giveni={A\bibinitperiod}}}%
{{hash=06d67357ea59eba4ba8fecd5087e1e62}{%
family={Piechocki},
familyi={P\bibinitperiod},
given={Robert},
giveni={R\bibinitperiod}}}%
}
\strng{namehash}{0be670161f27bced9736b83c01699035}
\strng{fullhash}{795377fbbaafa7d6f47f2af4b6c06d56}
\strng{bibnamehash}{0be670161f27bced9736b83c01699035}
\strng{authorbibnamehash}{0be670161f27bced9736b83c01699035}
\strng{authornamehash}{0be670161f27bced9736b83c01699035}
\strng{authorfullhash}{795377fbbaafa7d6f47f2af4b6c06d56}
\field{sortinit}{R}
\field{sortinithash}{5e1c39a9d46ffb6bebd8f801023a9486}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{title}{Model-based Cybersecurity Engineering for Connected and Automated Vehicles: The FLOURISH Project}
\endentry
\entry{rosmansyah2020}{article}{}
\name{author}{3}{}{%
{{hash=a1d42538d4ad05c56fea584907e12303}{%
family={Rosmansyah},
familyi={R\bibinitperiod},
given={Yusep},
giveni={Y\bibinitperiod}}}%
{{hash=f1e900363be36bf3d4b30bb8b4733da5}{%
family={Hendarto},
familyi={H\bibinitperiod},
given={Ignatius},
giveni={I\bibinitperiod}}}%
{{hash=b5d25b77dc9a56dc1a258ce74624ccbc}{%
family={Pratama},
familyi={P\bibinitperiod},
given={Demby},
giveni={D\bibinitperiod}}}%
}
\list{publisher}{1}{%
{International Journal of Emerging Technology in Learning}%
}
\strng{namehash}{0a1166a641c49b7e31fc504b812faeea}
\strng{fullhash}{0a1166a641c49b7e31fc504b812faeea}
\strng{bibnamehash}{0a1166a641c49b7e31fc504b812faeea}
\strng{authorbibnamehash}{0a1166a641c49b7e31fc504b812faeea}
\strng{authornamehash}{0a1166a641c49b7e31fc504b812faeea}
\strng{authorfullhash}{0a1166a641c49b7e31fc504b812faeea}
\field{sortinit}{R}
\field{sortinithash}{5e1c39a9d46ffb6bebd8f801023a9486}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{journaltitle}{International Journal of Emerging Technologies in Learning (iJET)}
\field{number}{19}
\field{title}{Impersonation Attack-Defense Tree}
\field{volume}{15}
\field{year}{2020}
\field{pages}{239\bibrangedash 246}
\range{pages}{8}
\endentry
\entry{ruijters2017}{inproceedings}{}
\name{author}{4}{}{%
{{hash=195ebb88fb7b5521b58de1a26e9d80ee}{%
family={Ruijters},
familyi={R\bibinitperiod},
given={Enno},
giveni={E\bibinitperiod}}}%
{{hash=2e352be67fd13eb4b7657d7fecdfcdaf}{%
family={Schivo},
familyi={S\bibinitperiod},
given={Stefano},
giveni={S\bibinitperiod}}}%
{{hash=1de27df00ec03386445460a544abaf31}{%
family={Stoelinga},
familyi={S\bibinitperiod},
given={Mariëlle},
giveni={M\bibinitperiod}}}%
{{hash=e806b3a37ebff240a48d76891c159b95}{%
family={Rensink},
familyi={R\bibinitperiod},
given={Arend},
giveni={A\bibinitperiod}}}%
}
\list{organization}{1}{%
{IEEE}%
}
\strng{namehash}{44e400599e81e8725f4766c1dedfbee1}
\strng{fullhash}{a56aac8814adafd17c2934badccfeb22}
\strng{bibnamehash}{44e400599e81e8725f4766c1dedfbee1}
\strng{authorbibnamehash}{44e400599e81e8725f4766c1dedfbee1}
\strng{authornamehash}{44e400599e81e8725f4766c1dedfbee1}
\strng{authorfullhash}{a56aac8814adafd17c2934badccfeb22}
\field{sortinit}{R}
\field{sortinithash}{5e1c39a9d46ffb6bebd8f801023a9486}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{booktitle}{2017 Annual Reliability and Maintainability Symposium (RAMS)}
\field{title}{Uniform analysis of fault trees through model transformations}
\field{year}{2017}
\field{pages}{1\bibrangedash 7}
\range{pages}{7}
\endentry
\entry{schurmann2020}{inproceedings}{}
\name{author}{3}{}{%
{{hash=6f42541ef24000345125717bc661dcd2}{%
family={Schürmann},
familyi={S\bibinitperiod},
given={Carsten},
giveni={C\bibinitperiod}}}%
{{hash=1da84b2821f1c4710a3372aac0548b2f}{%
family={Jensen},
familyi={J\bibinitperiod},
given={Lisa\bibnamedelima Hartmann},
giveni={L\bibinitperiod\bibinitdelim H\bibinitperiod}}}%
{{hash=44499608f54cec49538eb22a0082647d}{%
family={Sigbjörnsdóttir},
familyi={S\bibinitperiod},
given={Rósa\bibnamedelima María},
giveni={R\bibinitperiod\bibinitdelim M\bibinitperiod}}}%
}
\list{organization}{1}{%
{Springer}%
}
\strng{namehash}{ee7192c9689f09c2b15017df85b75290}
\strng{fullhash}{ee7192c9689f09c2b15017df85b75290}
\strng{bibnamehash}{ee7192c9689f09c2b15017df85b75290}
\strng{authorbibnamehash}{ee7192c9689f09c2b15017df85b75290}
\strng{authornamehash}{ee7192c9689f09c2b15017df85b75290}
\strng{authorfullhash}{ee7192c9689f09c2b15017df85b75290}
\field{sortinit}{S}
\field{sortinithash}{b164b07b29984b41daf1e85279fbc5ab}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{booktitle}{International Joint Conference on Electronic Voting}
\field{title}{Effective Cybersecurity Awareness Training for Election Officials}
\field{year}{2020}
\field{pages}{196\bibrangedash 212}
\range{pages}{17}
\endentry
\entry{sebastio2013multivesta}{article}{}
\name{author}{2}{}{%
{{hash=0e14de2e58a552518a99cd0892d01227}{%
family={Sebastio},
familyi={S\bibinitperiod},
given={Stefano},
giveni={S\bibinitperiod}}}%
{{hash=bab0dce7b8a11d35b0ff0c1ec86243ca}{%
family={Vandin},
familyi={V\bibinitperiod},
given={Andrea},
giveni={A\bibinitperiod}}}%
}
\list{publisher}{1}{%
{IMT Institute for Advanced Studies Lucca}%
}
\strng{namehash}{12c5554bf1deb74a97437bc0cd402dae}
\strng{fullhash}{12c5554bf1deb74a97437bc0cd402dae}
\strng{bibnamehash}{12c5554bf1deb74a97437bc0cd402dae}
\strng{authorbibnamehash}{12c5554bf1deb74a97437bc0cd402dae}
\strng{authornamehash}{12c5554bf1deb74a97437bc0cd402dae}
\strng{authorfullhash}{12c5554bf1deb74a97437bc0cd402dae}
\field{sortinit}{S}
\field{sortinithash}{b164b07b29984b41daf1e85279fbc5ab}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{title}{MultiVeStA: Statistical model checking for discrete event simulators}
\field{year}{2013}
\endentry
\entry{soligo2020}{thesis}{}
\name{author}{1}{}{%
{{hash=0a8e360dbcf14165afe6c961fc9752db}{%
family={Soligo},
familyi={S\bibinitperiod},
given={Lorenzo},
giveni={L\bibinitperiod}}}%
}
\list{institution}{1}{%
{Università Ca'Foscari Venezia}%
}
\strng{namehash}{0a8e360dbcf14165afe6c961fc9752db}
\strng{fullhash}{0a8e360dbcf14165afe6c961fc9752db}
\strng{bibnamehash}{0a8e360dbcf14165afe6c961fc9752db}
\strng{authorbibnamehash}{0a8e360dbcf14165afe6c961fc9752db}
\strng{authornamehash}{0a8e360dbcf14165afe6c961fc9752db}
\strng{authorfullhash}{0a8e360dbcf14165afe6c961fc9752db}
\field{sortinit}{S}
\field{sortinithash}{b164b07b29984b41daf1e85279fbc5ab}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{title}{Secure deployment of HTTPS: Analysis and open challenges}
\field{type}{{B.S.} thesis}
\field{year}{2020}
\endentry
\entry{ten2007}{inproceedings}{}
\name{author}{3}{}{%
{{hash=14a57227055f28329587149bb8a537b9}{%
family={Ten},
familyi={T\bibinitperiod},
given={Chee-Wooi},
giveni={C\bibinithyphendelim W\bibinitperiod}}}%
{{hash=5047298ccf24b604d8fe9a30b6a7332d}{%
family={Liu},
familyi={L\bibinitperiod},
given={Chen-Ching},
giveni={C\bibinithyphendelim C\bibinitperiod}}}%
{{hash=6ff3870ccabaa01abe54f55fe3c7c769}{%
family={Govindarasu},
familyi={G\bibinitperiod},
given={Manimaran},
giveni={M\bibinitperiod}}}%
}
\list{organization}{1}{%
{IEEE}%
}
\strng{namehash}{bf9eab6c9657cbebf4560634dc1f3119}
\strng{fullhash}{bf9eab6c9657cbebf4560634dc1f3119}
\strng{bibnamehash}{bf9eab6c9657cbebf4560634dc1f3119}
\strng{authorbibnamehash}{bf9eab6c9657cbebf4560634dc1f3119}
\strng{authornamehash}{bf9eab6c9657cbebf4560634dc1f3119}
\strng{authorfullhash}{bf9eab6c9657cbebf4560634dc1f3119}
\field{sortinit}{T}
\field{sortinithash}{9af77f0292593c26bde9a56e688eaee9}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{booktitle}{2007 IEEE Power Engineering Society General Meeting}
\field{title}{Vulnerability assessment of cybersecurity for SCADA systems using attack trees}
\field{year}{2007}
\field{pages}{1\bibrangedash 8}
\range{pages}{8}
\endentry
\entry{widel2019}{article}{}
\name{author}{4}{}{%
{{hash=44022165d0d25a5f85d7bf8b3c0162d1}{%
family={Widel},
familyi={W\bibinitperiod},
given={Wojciech},
giveni={W\bibinitperiod}}}%
{{hash=74a2860abfd95c19047d3a66d9f4b400}{%
family={Audinot},
familyi={A\bibinitperiod},
given={Maxime},
giveni={M\bibinitperiod}}}%
{{hash=1efa860d3d32836b9d17dc9d9d67efab}{%
family={Fila},
familyi={F\bibinitperiod},
given={Barbara},
giveni={B\bibinitperiod}}}%
{{hash=f52457a9c92de5cc318b407b72e931f2}{%
family={Pinchinat},
familyi={P\bibinitperiod},
given={Sophie},
giveni={S\bibinitperiod}}}%
}
\list{publisher}{1}{%
{ACM New York, NY, USA}%
}
\strng{namehash}{50c8b39c68faab6a73315a083900a553}
\strng{fullhash}{27fa213dbabbcdf6f3f5fc795b0a2ca1}
\strng{bibnamehash}{50c8b39c68faab6a73315a083900a553}
\strng{authorbibnamehash}{50c8b39c68faab6a73315a083900a553}
\strng{authornamehash}{50c8b39c68faab6a73315a083900a553}
\strng{authorfullhash}{27fa213dbabbcdf6f3f5fc795b0a2ca1}
\field{sortinit}{W}
\field{sortinithash}{4315d78024d0cea9b57a0c6f0e35ed0d}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{journaltitle}{ACM Computing Surveys (CSUR)}
\field{number}{4}
\field{title}{Beyond 2014: Formal Methods for Attack Tree--based Security Modeling}
\field{volume}{52}
\field{year}{2019}
\field{pages}{1\bibrangedash 36}
\range{pages}{36}
\endentry
\entry{arimafinance}{article}{}
\name{author}{4}{}{%
{{hash=f10eb6ce4aea102a0d4366dcabe22ac1}{%
family={Xiao},
familyi={X\bibinitperiod},
given={Yi},
giveni={Y\bibinitperiod}}}%
{{hash=ed0a66c28238f806193fb6929e1b6e35}{%
family={Xiao},
familyi={X\bibinitperiod},
given={Jin},
giveni={J\bibinitperiod}}}%
{{hash=43b0dce2cc8966238118a2bec6068e52}{%
family={Liu},
familyi={L\bibinitperiod},
given={John},
giveni={J\bibinitperiod}}}%
{{hash=d2e6daf3c7ec646f2e43d76d9f668aff}{%
family={Wang},
familyi={W\bibinitperiod},
given={Shouyang},
giveni={S\bibinitperiod}}}%
}
\strng{namehash}{096ce58948c5b24bcbcf6147b95a1d0f}
\strng{fullhash}{18cded7dda04565877ecd4de5dce59f5}
\strng{bibnamehash}{096ce58948c5b24bcbcf6147b95a1d0f}
\strng{authorbibnamehash}{096ce58948c5b24bcbcf6147b95a1d0f}
\strng{authornamehash}{096ce58948c5b24bcbcf6147b95a1d0f}
\strng{authorfullhash}{18cded7dda04565877ecd4de5dce59f5}
\field{sortinit}{X}
\field{sortinithash}{1965c258adceecf23ce3d67b05113442}
\field{labelnamesource}{author}
\field{labeltitlesource}{title}
\field{issn}{1559-7067 1009-6124}
\field{journaltitle}{Journal of Systems Science and Complexity}
\field{number}{1}
\field{title}{A multiscale modeling approach incorporating ARIMA and anns for financial market volatility forecasting}
\field{volume}{27}
\field{year}{2014}
\field{pages}{225\bibrangedash 236}
\range{pages}{12}
\verb{doi}
\verb 10.1007/s11424-014-3305-4
\endverb
\endentry
\enddatalist
\endrefsection
\endinput