Theory AT
section "Attack Trees"
theory AT
imports MC
begin
text ‹Attack Trees are an intuitive and practical formal method to analyse and quantify
attacks on security and privacy. They are very useful to identify the steps an attacker
takes through a system when approaching the attack goal. Here, we provide
a proof calculus to analyse concrete attacks using a notion of attack validity.
We define a state based semantics with Kripke models and the temporal logic
CTL in the proof assistant Isabelle \<^cite>‹"npw:02"› using its Higher Order Logic
(HOL). We prove the correctness and completeness (adequacy) of Attack Trees in Isabelle
with respect to the model.›
subsection "Attack Tree datatype"
text ‹The following datatype definition @{text ‹attree›} defines attack trees.
The simplest case of an attack tree is a base attack.
The principal idea is that base attacks are defined by a pair of
state sets representing the initial states and the {\it attack property}
-- a set of states characterized by the fact that this property holds
in them.
Attacks can also be combined as the conjunction or disjunction of other attacks.
The operator @{text ‹⊕⇩∨›} creates or-trees and @{text ‹⊕⇩∧›} creates and-trees.
And-attack trees @{text ‹l ⊕⇩∧ s›} and or-attack trees @{text ‹l ⊕⇩∨ s›}
combine lists of attack trees $l$ either conjunctively or disjunctively and
consist of a list of sub-attacks -- again attack trees.›