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.›
datatype ('s :: state) attree = BaseAttack "('s set) * ('s set)" ("𝒩⇘(_)⇙") |
AndAttack "('s attree) list" "('s set) * ('s set)" ("_ ⊕⇩∧⇗(_)⇖" 60) |
OrAttack "('s attree) list" "('s set) * ('s set)" ("_ ⊕⇩∨⇗(_)⇖" 61)
primrec attack :: "('s :: state) attree ⇒ ('s set) * ('s set)"
where
"attack (BaseAttack b) = b"|
"attack (AndAttack as s) = s" |
"attack (OrAttack as s) = s"
subsection ‹Attack Tree refinement›
text ‹When we develop an attack tree, we proceed from an abstract attack, given
by an attack goal, by breaking it down into a series of sub-attacks. This
proceeding corresponds to a process of {\it refinement}. Therefore, as part of
the attack tree calculus, we provide a notion of attack tree refinement.
The relation @{text ‹refines_to›} "constructs" the attack tree. Here the above
defined attack vectors are used to define how nodes in an attack tree
can be expanded into more detailed (refined) attack sequences. This
process of refinement @{text "⊑"} allows to eventually reach a fully detailed
attack that can then be proved using @{text "⊢"}.›
inductive refines_to :: "[('s :: state) attree, 's attree] ⇒ bool" ("_ ⊑ _" [40] 40)
where
refI: "⟦ A = ((l @ [ 𝒩⇘(si',si'')⇙] @ l'')⊕⇩∧⇗(si,si''')⇖ );
A' = (l' ⊕⇩∧⇗(si',si'')⇖);
A'' = (l @ l' @ l'' ⊕⇩∧⇗(si,si''')⇖)
⟧ ⟹ A ⊑ A''"|
ref_or: "⟦ as ≠ []; ∀ A' ∈ set(as). (A ⊑ A') ∧ attack A = s ⟧ ⟹ A ⊑ (as ⊕⇩∨⇗s⇖)" |
ref_trans: "⟦ A ⊑ A'; A' ⊑ A'' ⟧ ⟹ A ⊑ A''"|
ref_refl : "A ⊑ A"
subsection ‹Validity of Attack Trees›
text ‹A valid attack, intuitively, is one which is fully refined into fine-grained
attacks that are feasible in a model. The general model we provide is
a Kripke structure, i.e., a set of states and a generic state transition.
Thus, feasible steps in the model are single steps of the state transition.
We call them valid base attacks.
The composition of sequences of valid base attacks into and-attacks yields
again valid attacks if the base attacks line up with respect to the states
in the state transition. If there are different valid attacks for the same
attack goal starting from the same initial state set, these can be
summarized in an or-attack.
More precisely, the different cases of the validity predicate are distinguished
by pattern matching over the attack tree structure.
\begin{itemize}
\item A base attack @{text ‹𝒩(s0,s1)›} is valid if from all
states in the pre-state set @{text ‹s0›} we can get with a single step of the
state transition relation to a state in the post-state set ‹s1›. Note,
that it is sufficient for a post-state to exist for each pre-state. After all,
we are aiming to validate attacks, that is, possible attack paths to some
state that fulfills the attack property.
\item An and-attack @{text ‹As ⊕⇩∧ (s0,s1)›} is a valid attack
if either of the following cases holds:
\begin{itemize}
\item empty attack sequence @{text ‹As›}: in this case
all pre-states in @{text ‹s0›} must already be attack states
in @{text ‹s1›}, i.e., @{text ‹s0 ⊆ s1›};
\item attack sequence @{text ‹As›} is singleton: in this case, the
singleton element attack @{text ‹a›} in @{text ‹[a]›},
must be a valid attack and it must be an attack with pre-state
@{text ‹s0›} and post-state @{text ‹s1›};
\item otherwise, @{text ‹As›} must be a list matching @{text ‹a # l›} for
some attack @{text ‹a›} and tail of attack list @{text ‹l›} such that
@{text ‹a›} is a valid attack with pre-state identical to the overall
pre-state @{text ‹s0›} and the goal of the tail @{text ‹l›} is
@{text ‹s1›} the goal of the overall attack. The pre-state of the
attack represented by @{text ‹l›} is @{text ‹snd(attack a)›} since this is
the post-state set of the first step @{text ‹a›}.
\end{itemize}
\item An or-attack @{text ‹As ⊕⇩∨(s0,s1)›} is a valid attack
if either of the following cases holds:
\begin{itemize}
\item the empty attack case is identical to the and-attack above:
@{text ‹s0 ⊆ s1›};
\item attack sequence @{text ‹As›} is singleton: in this case, the
singleton element attack @{text ‹a›}
must be a valid attack and
its pre-state must include the overall attack pre-state set @{text ‹s0›}
(since @{text ‹a›} is singleton in the or) while the post-state of
@{text ‹a›} needs to be included in the global attack goal @{text ‹s1›};
\item otherwise, @{text ‹As›} must be a list @{text ‹a # l›} for
an attack @{text ‹a›} and a list @{text ‹l›} of alternative attacks.
The pre-states can be just a subset of @{text ‹s0›} (since there are
other attacks in @{text ‹l›} that can cover the rest) and the goal
states @{text ‹snd(attack a)›} need to lie all in the overall goal
state @{text ‹set s1›}. The other or-attacks in @{text ‹l›} need
to cover only the pre-states @{text ‹fst s - fst(attack a)›}
(where @{text ‹-›} is set difference) and have the same goal @{text ‹snd s›}.
\end{itemize}
\end{itemize}
The proof calculus is thus completely described by one recursive function. ›
fun is_attack_tree :: "[('s :: state) attree] ⇒ bool" ("⊢_" [40] 40)
where
att_base: "(⊢ 𝒩⇘s⇙) = ( (∀ x ∈ (fst s). (∃ y ∈ (snd s). x →⇩i y )))" |
att_and: "(⊢(As ⊕⇩∧⇗s⇖)) =
(case As of
[] ⇒ (fst s ⊆ snd s)
| [a] ⇒ ( ⊢ a ∧ attack a = s)
| (a # l) ⇒ (( ⊢ a) ∧ (fst(attack a) = fst s) ∧
(⊢(l ⊕⇩∧⇗(snd(attack a),snd(s))⇖))))" |
att_or: "(⊢(As ⊕⇩∨⇗s⇖)) =
(case As of
[] ⇒ (fst s ⊆ snd s)
| [a] ⇒ ( ⊢ a ∧ (fst(attack a) ⊇ fst s) ∧ (snd(attack a) ⊆ snd s))
| (a # l) ⇒ (( ⊢ a) ∧ fst(attack a) ⊆ fst s ∧
snd(attack a) ⊆ snd s ∧
( ⊢(l ⊕⇩∨⇗(fst s - fst(attack a), snd s)⇖))))"
text ‹Since the definition is constructive, code can be generated directly from it, here
into the programming language Scala.›
export_code is_attack_tree in Scala
subsection "Lemmas for Attack Tree validity"
lemma att_and_one: assumes "⊢ a" and "attack a = s"
shows "⊢([a] ⊕⇩∧⇗s⇖)"
proof -
show " ⊢([a] ⊕⇩∧⇗s⇖)" using assms
by (subst att_and, simp del: att_and att_or)
qed
declare is_attack_tree.simps[simp del]
lemma att_and_empty[rule_format] : " ⊢([] ⊕⇩∧⇗(s', s'')⇖) ⟶ s' ⊆ s''"
by (simp add: is_attack_tree.simps(2))
lemma att_and_empty2: " ⊢([] ⊕⇩∧⇗(s, s)⇖)"
by (simp add: is_attack_tree.simps(2))
lemma att_or_empty[rule_format] : " ⊢([] ⊕⇩∨⇗(s', s'')⇖) ⟶ s' ⊆ s''"
by (simp add: is_attack_tree.simps(3))
lemma att_or_empty_back[rule_format]: " s' ⊆ s'' ⟶ ⊢([] ⊕⇩∨⇗(s', s'')⇖)"
by (simp add: is_attack_tree.simps(3))
lemma att_or_empty_rev: assumes "⊢(l ⊕⇩∨⇗(s, s')⇖)" and "¬(s ⊆ s')" shows "l ≠ []"
using assms att_or_empty by blast
lemma att_or_empty2: "⊢([] ⊕⇩∨⇗(s, s)⇖)"
by (simp add: att_or_empty_back)
lemma att_andD1: " ⊢(x1 # x2 ⊕⇩∧⇗s⇖) ⟹ ⊢ x1"
by (metis (no_types, lifting) is_attack_tree.simps(2) list.exhaust list.simps(4) list.simps(5))
lemma att_and_nonemptyD2[rule_format]:
"(x2 ≠ [] ⟶ ⊢(x1 # x2 ⊕⇩∧⇗s⇖) ⟶ ⊢ (x2 ⊕⇩∧⇗(snd(attack x1),snd s)⇖))"
by (metis (no_types, lifting) is_attack_tree.simps(2) list.exhaust list.simps(5))
lemma att_andD2 : " ⊢(x1 # x2 ⊕⇩∧⇗s⇖) ⟹ ⊢ (x2 ⊕⇩∧⇗(snd(attack x1),snd s)⇖)"
by (metis (mono_tags, lifting) att_and_empty2 att_and_nonemptyD2 is_attack_tree.simps(2) list.simps(4) list.simps(5))
lemma att_and_fst_lem[rule_format]:
"⊢(x1 # x2a ⊕⇩∧⇗x⇖) ⟶ xa ∈ fst (attack (x1 # x2a ⊕⇩∧⇗x⇖))
⟶ xa ∈ fst (attack x1)"
by (induction x2a, (subst att_and, simp)+)
lemma att_orD1: " ⊢(x1 # x2 ⊕⇩∨⇗x⇖) ⟹ ⊢ x1"
by (case_tac x2, (subst (asm) att_or, simp)+)
lemma att_or_snd_hd: " ⊢(a # list ⊕⇩∨⇗(aa, b)⇖) ⟹ snd(attack a) ⊆ b"
by (case_tac list, (subst (asm) att_or, simp)+)
lemma att_or_singleton[rule_format]:
" ⊢([x1] ⊕⇩∨⇗x⇖) ⟶ ⊢([] ⊕⇩∨⇗(fst x - fst (attack x1), snd x)⇖)"
by (subst att_or, simp, rule impI, rule att_or_empty_back, blast)
lemma att_orD2[rule_format]:
" ⊢(x1 # x2 ⊕⇩∨⇗x⇖) ⟶ ⊢ (x2 ⊕⇩∨⇗(fst x - fst(attack x1), snd x)⇖)"
by (case_tac x2, simp add: att_or_singleton, simp, subst att_or, simp)
lemma att_or_snd_att[rule_format]: "∀ x. ⊢ (x2 ⊕⇩∨⇗x⇖) ⟶ (∀ a ∈ (set x2). snd(attack a) ⊆ snd x )"
proof (induction x2)
case Nil
then show ?case by (simp add: att_or)
next
case (Cons a x2)
then show ?case using att_orD2 att_or_snd_hd by fastforce
qed
lemma singleton_or_lem: " ⊢([x1] ⊕⇩∨⇗x⇖) ⟹ fst x ⊆ fst(attack x1)"
by (subst (asm) att_or, simp)+
lemma or_att_fst_sup0[rule_format]: "x2 ≠ [] ⟶ (∀ x. (⊢ ((x2 ⊕⇩∨⇗x⇖):: ('s :: state) attree)) ⟶
((⋃ y::'s attree∈ set x2. fst (attack y)) ⊇ fst(x))) "
proof (induction x2)
case Nil
then show ?case by simp
next
case (Cons a x2)
then show ?case using att_orD2 singleton_or_lem by fastforce
qed
lemma or_att_fst_sup:
assumes "(⊢ ((x1 # x2 ⊕⇩∨⇗x⇖):: ('s :: state) attree))"
shows "((⋃ y::'s attree∈ set (x1 # x2). fst (attack y)) ⊇ fst(x))"
by (rule or_att_fst_sup0, simp, rule assms)
text ‹The lemma @{text ‹att_elem_seq›} is the main lemma for Correctness.
It shows that for a given attack tree x1, for each element in the set of start sets
of the first attack, we can reach in zero or more steps a state in the states in which
the attack is successful (the final attack state @{text ‹snd(attack x1)›}).
This proof is a big alternative to an earlier version of the proof with
@{text ‹first_step›} etc that mapped first on a sequence of sets of states.›
lemma att_elem_seq[rule_format]: "⊢ x1 ⟶ (∀ x ∈ fst(attack x1).
(∃ y. y ∈ snd(attack x1) ∧ x →⇩i* y))"
text ‹First attack tree induction›
proof (induction x1)
case (BaseAttack x)
then show ?case
by (metis AT.att_base EF_step EF_step_star_rev attack.simps(1))
next
case (AndAttack x1a x2)
then show ?case
apply (rule_tac x = x2 in spec)
apply (subgoal_tac "(∀ x1aa::'a attree.
x1aa ∈ set x1a ⟶
⊢x1aa ⟶
(∀x::'a∈fst (attack x1aa). ∃y::'a. y ∈ snd (attack x1aa) ∧ x →⇩i* y))")
apply (rule mp)
prefer 2
apply (rotate_tac -1)
apply assumption
text ‹Induction for @{text ‹∧›}: the manual instantiation seems tedious but in the @{text ‹∧›}
case necessary to get the right induction hypothesis.›
proof (rule_tac list = "x1a" in list.induct)
text ‹The @{text ‹∧›} induction empty case›
show "(∀x1aa::'a attree.
x1aa ∈ set [] ⟶
⊢x1aa ⟶ (∀x::'a∈fst (attack x1aa). ∃y::'a. y ∈ snd (attack x1aa) ∧ x →⇩i* y)) ⟶
(∀x::'a set × 'a set.
⊢([] ⊕⇩∧⇗x⇖) ⟶
(∀xa::'a∈fst (attack ([] ⊕⇩∧⇗x⇖)). ∃y::'a. y ∈ snd (attack ([] ⊕⇩∧⇗x⇖)) ∧ xa →⇩i* y))"
using att_and_empty state_transition_refl_def by fastforce
text ‹The @{text ‹∧›} induction case nonempty›
next show "⋀(x1a::'a attree list) (x2::'a set × 'a set) (x1::'a attree) (x2a::'a attree list).
(⋀x1aa::'a attree.
(x1aa ∈ set x1a) ⟹
((⊢x1aa) ⟶ (∀x::'a∈fst (attack x1aa). ∃y::'a. y ∈ snd (attack x1aa) ∧ x →⇩i* y))) ⟹
∀x1aa::'a attree.
(x1aa ∈ set x1a) ⟶
(⊢x1aa) ⟶ ((∀x::'a∈fst (attack x1aa). ∃y::'a. y ∈ snd (attack x1aa) ∧ x →⇩i* y)) ⟹
(∀x1aa::'a attree.
(x1aa ∈ set x2a) ⟶
(⊢x1aa) ⟶ (∀x::'a∈fst (attack x1aa). ∃y::'a. y ∈ snd (attack x1aa) ∧ x →⇩i* y)) ⟶
(∀x::'a set × 'a set.
(⊢(x2a ⊕⇩∧⇗x⇖)) ⟶
((∀xa::'a∈fst (attack (x2a ⊕⇩∧⇗x⇖)). ∃y::'a. y ∈ snd (attack (x2a ⊕⇩∧⇗x⇖)) ∧ xa →⇩i* y))) ⟹
((∀x1aa::'a attree.
(x1aa ∈ set (x1 # x2a)) ⟶
(⊢x1aa) ⟶ ((∀x::'a∈fst (attack x1aa). ∃y::'a. y ∈ snd (attack x1aa) ∧ x →⇩i* y))) ⟶
(∀x::'a set × 'a set.
( ⊢(x1 # x2a ⊕⇩∧⇗x⇖)) ⟶
(∀xa::'a∈fst (attack (x1 # x2a ⊕⇩∧⇗x⇖)).
(∃y::'a. y ∈ snd (attack (x1 # x2a ⊕⇩∧⇗x⇖)) ∧ (xa →⇩i* y)))))"
apply (rule impI, rule allI, rule impI)
text ‹Set free the Induction Hypothesis: this is necessary to provide the grounds for specific
instantiations in the step.›
apply (subgoal_tac "(∀x::'a set × 'a set.
⊢(x2a ⊕⇩∧⇗x⇖) ⟶
(∀xa::'a∈fst (attack (x2a ⊕⇩∧⇗x⇖)).
∃y::'a. y ∈ snd (attack (x2a ⊕⇩∧⇗x⇖)) ∧ xa →⇩i* y))")
prefer 2
apply simp
text ‹The following induction step for @{text ‹∧›} needs a number of manual instantiations
so that the proof is not found automatically. In the subsequent case for @{text ‹∨›},
sledgehammer finds the proof.›
proof -
show "⋀(x1a::'a attree list) (x2::'a set × 'a set) (x1::'a attree) (x2a::'a attree list) x::'a set × 'a set.
∀x1aa::'a attree.
x1aa ∈ set (x1 # x2a) ⟶
⊢x1aa ⟶ (∀x::'a∈fst (attack x1aa). ∃y::'a. y ∈ snd (attack x1aa) ∧ x →⇩i* y) ⟹
⊢(x1 # x2a ⊕⇩∧⇗x⇖) ⟹
∀x::'a set × 'a set.
⊢(x2a ⊕⇩∧⇗x⇖) ⟶
(∀xa::'a∈fst (attack (x2a ⊕⇩∧⇗x⇖)). ∃y::'a. y ∈ snd (attack (x2a ⊕⇩∧⇗x⇖)) ∧ xa →⇩i* y) ⟹
∀xa::'a∈fst (attack (x1 # x2a ⊕⇩∧⇗x⇖)). ∃y::'a. y ∈ snd (attack (x1 # x2a ⊕⇩∧⇗x⇖)) ∧ xa →⇩i* y"
apply (rule ballI)
apply (rename_tac xa)
text ‹Prepare the steps›
apply (drule_tac x = "(snd(attack x1), snd x)" in spec)
apply (rotate_tac -1)
apply (erule impE)
apply (erule att_andD2)
text ‹Premise for x1›
apply (drule_tac x = x1 in spec)
apply (drule mp)
apply simp
apply (drule mp)
apply (erule att_andD1)
text ‹Instantiate first step for xa›
apply (rotate_tac -1)
apply (drule_tac x = xa in bspec)
apply (erule att_and_fst_lem, assumption)
apply (erule exE)
apply (erule conjE)
text ‹Take this y and put it as first into the second part›
apply (drule_tac x = y in bspec)
apply simp
apply (erule exE)
apply (erule conjE)
text ‹Bind the first @{text ‹xa →⇩i* y›} and second @{text ‹y →⇩i* ya›} together for solution›
apply (rule_tac x = ya in exI)
apply (rule conjI)
apply simp
by (simp add: state_transition_refl_def)
qed
qed auto
next
case (OrAttack x1a x2)
then show ?case
proof (induction x1a arbitrary: x2)
case Nil
then show ?case
by (metis EF_lem2a EF_step_star_rev att_or_empty attack.simps(3) subsetD surjective_pairing)
next
case (Cons a x1a)
then show ?case
by (smt DiffI att_orD1 att_orD2 att_or_snd_att attack.simps(3) insert_iff list.set(2) prod.sel(1) snd_conv subset_iff)
qed
qed
lemma att_elem_seq0: "⊢ x1 ⟹ (∀ x ∈ fst(attack x1).
(∃ y. y ∈ snd(attack x1) ∧ x →⇩i* y))"
by (simp add: att_elem_seq)
subsection ‹Valid refinements›
definition valid_ref :: "[('s :: state) attree, 's attree] ⇒ bool" ("_ ⊑⇩V _" 50)
where
"A ⊑⇩V A' ≡ ( (A ⊑ A') ∧ ⊢ A')"
definition ref_validity :: "[('s :: state) attree] ⇒ bool" ("⊢⇩V _" 50)
where
"⊢⇩V A ≡ (∃ A'. (A ⊑⇩V A'))"
lemma ref_valI: " A ⊑ A'⟹ ⊢ A' ⟹ ⊢⇩V A"
using ref_validity_def valid_ref_def by blast
section "Correctness and Completeness"
text ‹This section presents the main theorems of Correctness and Completeness
between AT and Kripke, essentially:
@{text ‹⊢ (init K, p) ≡ K ⊢ EF p›}.
First, we proof a number of lemmas needed for both directions before we
show the Correctness theorem followed by the Completeness theorem.
›
subsection ‹Lemma for Correctness and Completeness›
lemma nth_app_eq[rule_format]:
"∀ sl x. sl ≠ [] ⟶ sl ! (length sl - Suc (0)) = x
⟶ (l @ sl) ! (length l + length sl - Suc (0)) = x"
by (induction l) auto
lemma nth_app_eq1[rule_format]: "i < length sla ⟹ (sla @ sl) ! i = sla ! i"
by (simp add: nth_append)
lemma nth_app_eq1_rev: "i < length sla ⟹ sla ! i = (sla @ sl) ! i"
by (simp add: nth_append)
lemma nth_app_eq2[rule_format]: "∀ sl i. length sla ≤ i ∧ i < length (sla @ sl)
⟶ (sla @ sl) ! i = sl ! (i - (length sla))"
by (simp add: nth_append)
lemma tl_ne_ex[rule_format]: "l ≠ [] ⟶ (? x . l = x # (tl l))"
by (induction l, auto)
lemma tl_nempty_lngth[rule_format]: "tl sl ≠ [] ⟶ 2 ≤ length(sl)"
using le_less by fastforce
lemma list_app_one_length: "length l = n ⟹ (l @ [s]) ! n = s"
by (erule subst, simp)
lemma tl_lem1[rule_format]: "l ≠ [] ⟶ tl l = [] ⟶ length l = 1"
by (induction l, simp+)
lemma nth_tl_length[rule_format]: "tl sl ≠ [] ⟶
tl sl ! (length (tl sl) - Suc (0)) = sl ! (length sl - Suc (0))"
by (induction sl, simp+)
lemma nth_tl_length1[rule_format]: "tl sl ≠ [] ⟶
tl sl ! n = sl ! (n + 1)"
by (induction sl, simp+)
lemma ineq1: "i < length sla - n ⟹
(0) ≤ n ⟹ i < length sla"
by simp
lemma ineq2[rule_format]: "length sla ≤ i ⟶ i + (1) - length sla = i - length sla + 1"
by arith
lemma ineq3: "tl sl ≠ [] ⟹ length sla ≤ i ⟹ i < length (sla @ tl sl) - (1)
⟹ i - length sla + (1) < length sl - (1)"
by simp
lemma tl_eq1[rule_format]: "sl ≠ [] ⟶ tl sl ! (0) = sl ! Suc (0)"
by (induction sl, simp+)
lemma tl_eq2[rule_format]: "tl sl = [] ⟶ sl ! (0) = sl ! (length sl - (1))"
by (induction sl, simp+)
lemma tl_eq3[rule_format]: "tl sl ≠ [] ⟶
tl sl ! (length sl - Suc (Suc (0))) = sl ! (length sl - Suc (0))"
by (induction sl, simp+)
lemma nth_app_eq3: assumes "tl sl ≠ []"
shows "(sla @ tl sl) ! (length (sla @ tl sl) - (1)) = sl ! (length sl - (1))"
using assms nth_app_eq nth_tl_length by fastforce
lemma not_empty_ex: "A ≠ {} ⟹ ? x. x ∈ A"
by force
lemma fst_att_eq: "(fst x # sl) ! (0) = fst (attack (al ⊕⇩∧⇗x⇖))"
by simp
lemma list_eq1[rule_format]: "sl ≠ [] ⟶
(fst x # sl) ! (length (fst x # sl) - (1)) = sl ! (length sl - (1))"
by (induction sl, auto)
lemma attack_eq1: "snd (attack (x1 # x2a ⊕⇩∧⇗x⇖)) = snd (attack (x2a ⊕⇩∧⇗(snd (attack x1), snd x)⇖))"
by simp
lemma fst_lem1[rule_format]: "∀ (a:: 's set) b (c :: 's set) d. (a, c) = (b, d) ⟶ a = b"
by auto
lemma fst_eq1: "(sla ! (0), y) = attack x1 ⟹
sla ! (0) = fst (attack x1)"
by (rule_tac c = y and d = "snd(attack x1)" in fst_lem1, simp)
lemma base_att_lem1: " y0 ⊆ y1 ⟹ ⊢ 𝒩⇘(y1, y)⇙ ⟹⊢ 𝒩⇘(y0, y)⇙"
by (simp add: att_base, blast)
lemma ref_pres_att: "A ⊑ A' ⟹ attack A = attack A'"
proof (erule refines_to.induct)
show "⋀(A::'a attree) (l::'a attree list) (si'::'a set) (si''::'a set) (l''::'a attree list) (si::'a set)
(si'''::'a set) (A'::'a attree) (l'::'a attree list) A''::'a attree.
A = (l @ [𝒩⇘(si', si'')⇙] @ l'' ⊕⇩∧⇗(si, si''')⇖) ⟹
A' = (l' ⊕⇩∧⇗(si', si'')⇖) ⟹ A'' = (l @ l' @ l'' ⊕⇩∧⇗(si, si''')⇖) ⟹ attack A = attack A''"
by simp
next show "⋀(as::'a attree list) (A::'a attree) (s::'a set × 'a set).
as ≠ [] ⟹
(∀A'::'a attree∈ (set as). ((A ⊑ A') ∧ (attack A = attack A')) ∧ attack A = s) ⟹
attack A = attack (as ⊕⇩∨⇗s⇖)"
using last_in_set by auto
next show "⋀(A::'a attree) (A'::'a attree) A''::'a attree.
A ⊑ A' ⟹ attack A = attack A' ⟹ A' ⊑ A'' ⟹ attack A' = attack A'' ⟹ attack A = attack A''"
by simp
next show "⋀A::'a attree. attack A = attack A" by (rule refl)
qed
lemma base_subset:
assumes "xa ⊆ xc"
shows "⊢𝒩⇘(x, xa)⇙ ⟹ ⊢𝒩⇘(x, xc)⇙"
proof (simp add: att_base)
show " ∀x::'a∈x. ∃xa::'a∈xa. x →⇩i xa ⟹ ∀x::'a∈x. ∃xa::'a∈xc. x →⇩i xa"
by (meson assms in_mono)
qed
subsection "Correctness Theorem"
text ‹Proof with induction over the definition of EF using the main
lemma @{text ‹att_elem_seq0›}.
There is also a second version of Correctness for valid refinements.›
theorem AT_EF: assumes " ⊢ (A :: ('s :: state) attree)"
and "attack A = (I,s)"
shows "Kripke {s :: ('s :: state). ∃ i ∈ I. (i →⇩i* s)} (I :: ('s :: state)set) ⊢ EF s"
proof (simp add:check_def)
show "I ⊆ {sa::('s :: state). (∃i::'s∈I. i →⇩i* sa) ∧ sa ∈ EF s}"
proof (rule subsetI, rule CollectI, rule conjI, simp add: state_transition_refl_def)
show "⋀x::'s. x ∈ I ⟹ ∃i::'s∈I. (i, x) ∈ {(x::'s, y::'s). x →⇩i y}⇧*"
by (rule_tac x = x in bexI, simp)
next show "⋀x::'s. x ∈ I ⟹ x ∈ EF s" using assms
proof -
have a: "∀ x ∈ I. ∃ y ∈ s. x →⇩i* y" using assms
proof -
have "∀x::'s∈fst (attack A). ∃y::'s. y ∈ snd (attack A) ∧ x →⇩i* y"
by (rule att_elem_seq0, rule assms)
thus " ∀x::'s∈I. ∃y::'s∈s. x →⇩i* y" using assms
by force
qed
thus "⋀x::'s. x ∈ I ⟹ x ∈ EF s"
proof -
fix x
assume b: "x ∈ I"
have "∃y::'s∈s::('s :: state) set. x →⇩i* y"
by (rule_tac x = x and A = I in bspec, rule a, rule b)
from this obtain y where "y ∈ s" and "x →⇩i* y" by (erule bexE)
thus "x ∈ EF s"
by (erule_tac f = s in EF_step_star)
qed
qed
qed
qed
theorem ATV_EF: "⟦ ⊢⇩V A; (I,s) = attack A ⟧ ⟹
(Kripke {s. ∃ i ∈ I. (i →⇩i* s) } I ⊢ EF s)"
by (metis (full_types) AT_EF ref_pres_att ref_validity_def valid_ref_def)
subsection "Completeness Theorem"
text ‹This section contains the completeness direction, informally:
@{text ‹⊢ EF s ⟹ ∃ A. ⊢ A ∧ attack A = (I,s)›}.
The main theorem is presented last since its
proof just summarises a number of main lemmas @{text ‹Compl_step1, Compl_step2,
Compl_step3, Compl_step4›} which are presented first together with other
auxiliary lemmas.›
subsubsection "Lemma @{text ‹Compl_step1›}"
lemma Compl_step1:
"Kripke {s :: ('s :: state). ∃ i ∈ I. (i →⇩i* s)} I ⊢ EF s
⟹ ∀ x ∈ I. ∃ y ∈ s. x →⇩i* y"
by (simp add: EF_step_star_rev valEF_E)
subsubsection "Lemma @{text ‹Compl_step2›}"
text ‹First, we prove some auxiliary lemmas.›
lemma rtrancl_imp_singleton_seq2: "x →⇩i* y ⟹
x = y ∨ (∃ s. s ≠ [] ∧ (tl s ≠ []) ∧ s ! 0 = x ∧ s ! (length s - 1) = y ∧
(∀ i < (length s - 1). (s ! i) →⇩i (s ! (Suc i))))"
unfolding state_transition_refl_def
proof (induction rule: rtrancl_induct)
case base
then show ?case
by simp
next
case (step y z)
show ?case
using step.IH
proof (elim disjE exE conjE)
assume "x=y"
with step.hyps show ?case
by (force intro!: exI [where x="[y,z]"])
next
show "⋀s. ⟦s ≠ []; tl s ≠ []; s ! 0 = x;
s ! (length s - 1) = y;
∀i<length s - 1.
s ! i →⇩i s ! Suc i⟧
⟹ x = z ∨
(∃s. s ≠ [] ∧
tl s ≠ [] ∧ s ! 0 = x ∧
s ! (length s - 1) = z ∧
(∀i<length s - 1. s ! i →⇩i s ! Suc i))"
apply (rule disjI2)
apply (rule_tac x="s @ [z]" in exI)
apply (auto simp: nth_append)
by (metis One_nat_def Suc_lessI diff_Suc_1 mem_Collect_eq old.prod.case step.hyps(2))
qed
qed
lemma tl_nempty_length[rule_format]: "s ≠ [] ⟶ tl s ≠ [] ⟶ 0 < length s - 1"
by (induction s, simp+)
lemma tl_nempty_length2[rule_format]: "s ≠ [] ⟶ tl s ≠ [] ⟶ Suc 0 < length s"
by (induction s, simp+)
lemma length_last[rule_format]: "(l @ [x]) ! (length (l @ [x]) - 1) = x"
by (induction l, simp+)
lemma Compl_step2: "∀ x ∈ I. ∃ y ∈ s. x →⇩i* y ⟹
( ∀ x ∈ I. x ∈ s ∨ (∃ (sl :: ((('s :: state) set)list)).
(sl ≠ []) ∧ (tl sl ≠ []) ∧
(sl ! 0, sl ! (length sl - 1)) = ({x},s) ∧
(∀ i < (length sl - 1). ⊢ 𝒩⇘(sl ! i,sl ! (i+1) )⇙
)))"
proof (rule ballI, drule_tac x = x in bspec, assumption, erule bexE)
fix x y
assume a: "x ∈ I" and b: "y ∈ s" and c: "x →⇩i* y"
show "x ∈ s ∨
(∃sl::'s set list.
sl ≠ [] ∧
tl sl ≠ [] ∧
(sl ! (0), sl ! (length sl - (1))) = ({x}, s) ∧
(∀i<length sl - (1). ⊢𝒩⇘(sl ! i, sl ! (i + (1)))⇙))"
proof -
have d : "x = y ∨
(∃s'. s' ≠ [] ∧
tl s' ≠ [] ∧
s' ! (0) = x ∧
s' ! (length s' - (1)) = y ∧ (∀i<length s' - (1). s' ! i →⇩i s' ! Suc i))"
using c rtrancl_imp_singleton_seq2 by blast
thus "x ∈ s ∨
(∃sl::'s set list.
sl ≠ [] ∧
tl sl ≠ [] ∧
(sl ! (0), sl ! (length sl - (1))) = ({x}, s) ∧
(∀i<length sl - (1). ⊢𝒩⇘(sl ! i, sl ! (i + (1)))⇙))"
apply (rule disjE)
using b apply blast
apply (rule disjI2, elim conjE exE)
apply (rule_tac x = "[{s' ! j}. j ← [0..<(length s' - 1)]] @ [s]" in exI)
apply (auto simp: nth_append)
apply (metis AT.att_base Suc_lessD fst_conv prod.sel(2) singletonD singletonI)
apply (metis AT.att_base Suc_lessI b fst_conv prod.sel(2) singletonD)
using tl_nempty_length2 by blast
qed
qed
subsubsection "Lemma @{text ‹Compl_step3›}"
text ‹First, we need a few lemmas.›
lemma map_hd_lem[rule_format] : "n > 0 ⟶ (f 0 # map (λi. f i) [1..<n]) = map (λi. f i) [0..<n]"
by (simp add : hd_map upt_rec)
lemma map_Suc_lem[rule_format] : "n > 0 ⟶ map (λ i:: nat. f i)[1..<n] =
map (λ i:: nat. f(Suc i))[0..<(n - 1)]"
proof -
have "(f 0 # map (λn. f (Suc n)) [0..<n - 1] = f 0 # map f [1..<n]) = (map (λn. f (Suc n)) [0..<n - 1] = map f [1..<n])"
by blast
then show ?thesis
by (metis Suc_pred' map_hd_lem map_upt_Suc)
qed
lemma forall_ex_fun: "finite S ⟹ (∀ x ∈ S. (∃ y. P y x)) ⟶ (∃ f. ∀ x ∈ S. P (f x) x)"
proof (induction rule: finite.induct)
case emptyI
then show ?case
by simp
next
case (insertI F x)
then show ?case
proof (clarify)
assume d: "(∀x::'a∈insert x F. ∃y::'b. P y x)"
have "(∀x::'a∈F. ∃y::'b. P y x)"
using d by blast
then obtain f where f: "∀x::'a∈F. P (f x) x"
using insertI.IH by blast
from d obtain y where "P y x" by blast
thus "(∃f::'a ⇒ 'b. ∀x::'a∈insert x F. P (f x) x)" using f
by (rule_tac x = "λ z. if z = x then y else f z" in exI, simp)
qed
qed
primrec nodup :: "['a, 'a list] ⇒ bool"
where
nodup_nil: "nodup a [] = True" |
nodup_step: "nodup a (x # ls) = (if x = a then (a ∉ (set ls)) else nodup a ls)"
definition nodup_all:: "'a list ⇒ bool"
where
"nodup_all l ≡ ∀ x ∈ set l. nodup x l"
lemma nodup_all_lem[rule_format]:
"nodup_all (x1 # a # l) ⟶ (insert x1 (insert a (set l)) - {x1}) = insert a (set l)"
by (induction l, (simp add: nodup_all_def)+)
lemma nodup_all_tl[rule_format]: "nodup_all (x # l) ⟶ nodup_all l"
by (induction l, (simp add: nodup_all_def)+)
lemma finite_nodup: "finite I ⟹ ∃ l. set l = I ∧ nodup_all l"
proof (induction rule: finite.induct)
case emptyI
then show ?case
by (simp add: nodup_all_def)
next
case (insertI A a)
then show ?case
by (metis insertE insert_absorb list.simps(15) nodup_all_def nodup_step)
qed
lemma Compl_step3: "I ≠ {} ⟹ finite I ⟹
( ∀ x ∈ I. x ∈ s ∨ (∃ (sl :: ((('s :: state) set)list)).
(sl ≠ []) ∧ (tl sl ≠ []) ∧
(sl ! 0, sl ! (length sl - 1)) = ({x},s) ∧
(∀ i < (length sl - 1). ⊢ 𝒩⇘(sl ! i,sl ! (i+1) )⇙
)) ⟹
(∃ lI. set lI = {x :: 's :: state. x ∈ I ∧ x ∉ s} ∧ (∃ Sj :: ((('s :: state) set)list) list.
length Sj = length lI ∧ nodup_all lI ∧
(∀ j < length Sj. (((Sj ! j) ≠ []) ∧ (tl (Sj ! j) ≠ []) ∧
((Sj ! j) ! 0, (Sj ! j) ! (length (Sj ! j) - 1)) = ({lI ! j},s) ∧
(∀ i < (length (Sj ! j) - 1). ⊢ 𝒩⇘((Sj ! j) ! i, (Sj ! j) ! (i+1) )⇙
))))))"
proof -
assume i: "I ≠ {}" and f: "finite I" and
fa: "∀x::'s∈I.
x ∈ s ∨
(∃sl::'s set list.
sl ≠ [] ∧
tl sl ≠ [] ∧
(sl ! (0), sl ! (length sl - (1))) = ({x}, s) ∧
(∀i<length sl - (1). ⊢𝒩⇘(sl ! i, sl ! (i + (1)))⇙))"
have a: "∃ lI. set lI = {x::'s ∈ I. x ∉ s} ∧ nodup_all lI"
by (simp add: f finite_nodup)
from this obtain lI where b: "set lI = {x::'s ∈ I. x ∉ s} ∧ nodup_all lI"
by (erule exE)
thus "∃lI::'s list.
set lI = {x::'s ∈ I. x ∉ s} ∧
(∃Sj::'s set list list.
length Sj = length lI ∧
nodup_all lI ∧
(∀j<length Sj.
Sj ! j ≠ [] ∧
tl (Sj ! j) ≠ [] ∧
(Sj ! j ! (0), Sj ! j ! (length (Sj ! j) - (1))) = ({lI ! j}, s) ∧
(∀i<length (Sj ! j) - (1). ⊢𝒩⇘(Sj ! j ! i, Sj ! j ! (i + (1)))⇙)))"
apply (rule_tac x = lI in exI)
apply (rule conjI)
apply (erule conjE, assumption)
proof -
have c: "∀ x ∈ set(lI). (∃ sl::'s set list.
sl ≠ [] ∧
tl sl ≠ [] ∧
(sl ! (0), sl ! (length sl - (1))) = ({x}, s) ∧
(∀i<length sl - (1). ⊢𝒩⇘(sl ! i, sl ! (i + (1)))⇙))"
using b fa by fastforce
thus "∃Sj::'s set list list.
length Sj = length lI ∧
nodup_all lI ∧
(∀j<length Sj.
Sj ! j ≠ [] ∧
tl (Sj ! j) ≠ [] ∧
(Sj ! j ! (0), Sj ! j ! (length (Sj ! j) - (1))) = ({lI ! j}, s) ∧
(∀i<length (Sj ! j) - (1). ⊢𝒩⇘(Sj ! j ! i, Sj ! j ! (i + (1)))⇙))"
apply (subgoal_tac "finite (set lI)")
apply (rotate_tac -1)
apply (drule forall_ex_fun)
apply (drule mp)
apply assumption
apply (erule exE)
apply (rule_tac x = "[f (lI ! j). j ← [0..<(length lI)]]" in exI)
apply simp
apply (insert b)
apply (erule conjE, assumption)
apply (rule_tac A = "set lI" and B = I in finite_subset)
apply blast
by (rule f)
qed
qed
subsubsection ‹Lemma @{text ‹Compl_step4›}›
text ‹Again, we need some additional lemmas first.›
lemma list_one_tl_empty[rule_format]: "length l = Suc (0 :: nat) ⟶ tl l = []"
by (induction l, simp+)
lemma list_two_tl_not_empty[rule_format]: "∀ list. length l = Suc (Suc (length list)) ⟶ tl l ≠ []"
by (induction l, simp+, force)
lemma or_empty: "⊢([] ⊕⇩∨⇗({}, s)⇖)" by (simp add: att_or)
text ‹Note, this is not valid for any l, i.e., @{text ‹⊢ l ⊕⇩∨⇗({}, s)⇖›} is not a theorem.›
lemma list_or_upt[rule_format]:
"∀ l . lI ≠ [] ⟶ length l = length lI ⟶ nodup_all lI ⟶
(∀ i < length lI. (⊢ (l ! i)) ∧ (attack (l ! i) = ({lI ! i}, s)))
⟶ ( ⊢ (l ⊕⇩∨⇗(set lI, s)⇖))"
proof (induction lI, simp, clarify)
fix x1 x2 l
show "∀l::'a attree list.
x2 ≠ [] ⟶
length l = length x2 ⟶
nodup_all x2 ⟶
(∀i<length x2. ⊢(l ! i) ∧ attack (l ! i) = ({x2 ! i}, s)) ⟶ ⊢(l ⊕⇩∨⇗(set x2, s)⇖) ⟹
x1 # x2 ≠ [] ⟹
length l = length (x1 # x2) ⟹
nodup_all (x1 # x2) ⟹
∀i<length (x1 # x2). ⊢(l ! i) ∧ attack (l ! i) = ({(x1 # x2) ! i}, s) ⟹ ⊢(l ⊕⇩∨⇗(set (x1 # x2), s)⇖)"
apply (case_tac x2, simp, subst att_or, case_tac l, simp+)
text ‹Case @{text ‹∀i<Suc (Suc (length list)). ⊢l ! i ∧ attack (l ! i) = ({(x1 # a # list) ! i}, s) ⟹
x2 = a # list ⟹ ⊢l ⊕⇩∨⇗(insert x1 (insert a (set list)), s)⇖›}›
apply (subst att_or, case_tac l, simp, clarify, simp, rename_tac lista, case_tac lista, simp+)
text ‹Remaining conjunct of three conditions: @{text ‹ ⊢aa ∧
fst (attack aa) ⊆ insert x1 (insert a (set list)) ∧
snd (attack aa) ⊆ s ∧ ⊢ab # listb ⊕⇩∨⇗(insert x1 (insert a (set list)) - fst (attack aa), s)⇖›}›
apply (rule conjI)
text ‹First condition @{text ‹ ⊢aa›}›
apply (drule_tac x = 0 in spec, drule mp, simp, (erule conjE)+, simp, rule conjI)
text ‹Second condition @{text ‹fst (attack aa) ⊆ insert x1 (insert a (set list))›}›
apply (drule_tac x = 0 in spec, drule mp, simp, erule conjE, simp)
text ‹The remaining conditions
@{text ‹snd (attack aa) ⊆ s ∧ ⊢ab # listb ⊕⇩∨⇗(insert x1 (insert a (set list)) - fst (attack aa), s)⇖›}
are solved automatically!›
by (metis Suc_mono add.right_neutral add_Suc_right list.size(4) nodup_all_lem nodup_all_tl nth_Cons_0 nth_Cons_Suc order_refl prod.sel(1) prod.sel(2) zero_less_Suc)
qed
lemma app_tl_empty_hd[rule_format]: "tl (l @ [a]) = [] ⟶ hd (l @ [a]) = a"
by (induction l) auto
lemma tl_hd_empty[rule_format]: "tl (l @ [a]) = [] ⟶ l = []"
by (induction l) auto
lemma tl_hd_not_empty[rule_format]: "tl (l @ [a]) ≠ [] ⟶ l ≠ []"
by (induction l) auto
lemma app_tl_empty_length[rule_format]: "tl (map f [0..<length l] @ [a]) = []
⟹ l = []"
by (drule tl_hd_empty, simp)
lemma not_empty_hd_fst[rule_format]: "l ≠ [] ⟶ hd(l @ [a]) = l ! 0"
by (induction l) auto
lemma app_tl_hd_list[rule_format]: "tl (map f [0..<length l] @ [a]) ≠ []
⟹ hd(map f [0..<length l] @ [a]) = (map f [0..<length l]) ! 0"
by (drule tl_hd_not_empty, erule not_empty_hd_fst)
lemma tl_app_in[rule_format]: "l ≠ [] ⟶
map f [0..<(length l - (Suc 0:: nat))] @ [f(length l - (Suc 0 :: nat))] = map f [0..<length l]"
by (induction l) auto
lemma map_fst[rule_format]: "n > 0 ⟶ map f [0..<n] = f 0 # (map f [1..<n])"
by (induction n) auto
lemma step_lem[rule_format]: "l ≠ [] ⟹
tl (map (λ i. f((x1 # a # l) ! i)((a # l) ! i)) [0..<length l]) =
map (λi. f((a # l) ! i)(l ! i)) [0..<length l - (1)]"
proof (simp)
assume l: "l ≠ []"
have a: "map (λi. f ((x1 # a # l) ! i) ((a # l) ! i)) [0..<length l] =
(f(x1)(a) # (map (λi. f ((a # l) ! i) (l ! i)) [0..<(length l - 1)]))"
proof -
have b : "map (λi. f ((x1 # a # l) ! i) ((a # l) ! i)) [0..<length l] =
f ((x1 # a # l) ! 0) ((a # l) ! 0) #
(map (λi. f ((x1 # a # l) ! i) ((a # l) ! i)) [1..<length l])"
by (rule map_fst, simp, rule l)
have c: "map (λi. f ((x1 # a # l) ! i) ((a # l) ! i)) [Suc (0)..<length l] =
map (λi. f ((x1 # a # l) ! Suc i) ((a # l) ! Suc i)) [(0)..<(length l - 1)]"
by (subgoal_tac "[Suc (0)..<length l] = map Suc [0..<(length l - 1)]",
simp, simp add: map_Suc_upt l)
thus "map (λi. f ((x1 # a # l) ! i) ((a # l) ! i)) [0..<length l] =
f x1 a # map (λi. f ((a # l) ! i) (l ! i)) [0..<length l - (1)]"
by (simp add: b c)
qed
thus "l ≠ [] ⟹
tl (map (λi. f ((x1 # a # l) ! i) ((a # l) ! i)) [0..<length l]) =
map (λi. f ((a # l) ! i) (l ! i)) [0..<length l - Suc (0)]"
by (subst a, simp)
qed
lemma step_lem2a[rule_format]: "0 < length list ⟹ map (λi. 𝒩⇘((x1 # a # list) ! i, (a # list) ! i)⇙)
[0..<length list] @
[𝒩⇘((x1 # a # list) ! length list, (a # list) ! length list)⇙] =
aa # listb ⟶ 𝒩⇘((x1, a))⇙ = aa"
by (subst map_fst, assumption, simp)
lemma step_lem2b[rule_format]: "0 = length list ⟹ map (λi. 𝒩⇘((x1 # a # list) ! i, (a # list) ! i)⇙)
[0..<length list] @
[𝒩⇘((x1 # a # list) ! length list, (a # list) ! length list)⇙] =
aa # listb ⟶ 𝒩⇘((x1, a))⇙ = aa"
by simp
lemma step_lem2: "map (λi. 𝒩⇘((x1 # a # list) ! i, (a # list) ! i)⇙)
[0..<length list] @
[𝒩⇘((x1 # a # list) ! length list, (a # list) ! length list)⇙] =
aa # listb ⟹ 𝒩⇘((x1, a))⇙ = aa"
proof (case_tac "length list", rule step_lem2b, erule sym, assumption)
show "⋀nat.
map (λi. 𝒩⇘((x1 # a # list) ! i, (a # list) ! i)⇙) [0..<length list] @
[𝒩⇘((x1 # a # list) ! length list, (a # list) ! length list)⇙] =
aa # listb ⟹
length list = Suc nat ⟹ 𝒩⇘(x1, a)⇙ = aa"
by (rule_tac list = list in step_lem2a, simp)
qed
lemma base_list_and[rule_format]: "Sji ≠ [] ⟶ tl Sji ≠ [] ⟶
(∀ li. Sji ! (0) = li ⟶
Sji! (length (Sji) - 1) = s ⟶
(∀i<length (Sji) - 1. ⊢𝒩⇘(Sji ! i, Sji ! Suc i)⇙) ⟶
⊢ (map (λi. 𝒩⇘(Sji ! i, Sji ! Suc i)⇙)
[0..<length (Sji) - Suc (0)] ⊕⇩∧⇗(li, s)⇖))"
proof (induction Sji)
case Nil
then show ?case by simp
next
case (Cons a Sji)
then show ?case
apply (subst att_and, case_tac Sji, simp, simp)
apply (rule impI)+
proof -
fix aa list
show "list ≠ [] ⟶
list ! (length list - Suc 0) = s ⟶
(∀i<length list. ⊢𝒩⇘((aa # list) ! i, list ! i)⇙) ⟶
⊢(map (λi. 𝒩⇘((aa # list) ! i, list ! i)⇙) [0..<length list] ⊕⇩∧⇗(aa, s)⇖) ⟹
Sji = aa # list ⟹
(aa # list) ! length list = s ⟹
∀i<Suc (length list). ⊢𝒩⇘((a # aa # list) ! i, (aa # list) ! i)⇙ ⟹
case map (λi. 𝒩⇘((a # aa # list) ! i, (aa # list) ! i)⇙) [0..<length list] @
[𝒩⇘((a # aa # list) ! length list, s)⇙] of
[] ⇒ fst (a, s) ⊆ snd (a, s) | [aa] ⇒ ⊢aa ∧ attack aa = (a, s)
| aa # ab # list ⇒
⊢aa ∧ fst (attack aa) = fst (a, s) ∧ ⊢(ab # list ⊕⇩∧⇗(snd (attack aa), snd (a, s))⇖)"
proof (case_tac "map (λi. 𝒩⇘((a # aa # list) ! i, (aa # list) ! i)⇙) [0..<length list] @
[𝒩⇘((a # aa # list) ! length list, s)⇙]", simp, clarify, simp)
fix ab lista
have *: "tl (map (λi. 𝒩⇘((a # aa # list) ! i, (aa # list) ! i)⇙) [0..<length list])
= (map (λi. 𝒩⇘((aa # list) ! i, (list) ! i)⇙) [0..<(length list - 1)])"
if "list ≠ []"
apply (subgoal_tac "tl (map (λi. 𝒩⇘((a # aa # list) ! i, (aa # list) ! i)⇙) [0..<length list])
= (map (λi. 𝒩⇘((aa # list) ! i, (list) ! i)⇙) [0..<(length list - 1)])")
apply blast
apply (subst step_lem [OF that])
apply simp
done
show "list ≠ [] ⟶
(∀i<length list. ⊢𝒩⇘((aa # list) ! i, list ! i)⇙) ⟶
⊢(map (λi. 𝒩⇘((aa # list) ! i, list ! i)⇙)
[0..<length list] ⊕⇩∧⇗(aa, list ! (length list - Suc 0))⇖) ⟹
Sji = aa # list ⟹
∀i<Suc (length list). ⊢𝒩⇘((a # aa # list) ! i, (aa # list) ! i)⇙ ⟹
map (λi. 𝒩⇘((a # aa # list) ! i, (aa # list) ! i)⇙) [0..<length list] @
[𝒩⇘((a # aa # list) ! length list, (aa # list) ! length list)⇙] =
ab # lista ⟹
s = (aa # list) ! length list ⟹
case lista of [] ⇒ ⊢ab ∧ attack ab = (a, (aa # list) ! length list)
| aba # lista ⇒
⊢ab ∧ fst (attack ab) = a ∧ ⊢(aba # lista ⊕⇩∧⇗(snd (attack ab), (aa # list) ! length list)⇖)"
apply (auto simp: split: list.split)
apply (metis (no_types, lifting) app_tl_hd_list length_greater_0_conv list.sel(1) list.sel(3) list.simps(3) list.simps(8) list.size(3) map_fst nth_Cons_0 self_append_conv2 upt_0 zero_less_Suc)
apply (metis (no_types, lifting) app_tl_hd_list attack.simps(1) fst_conv length_greater_0_conv list.sel(1) list.sel(3) list.simps(3) list.simps(8) list.size(3) map_fst nth_Cons_0 self_append_conv2 upt_0)
apply (metis (mono_tags, lifting) app_tl_hd_list attack.simps(1) fst_conv length_greater_0_conv list.sel(1) list.sel(3) list.simps(3) list.simps(8) list.size(3) map_fst nth_Cons_0 self_append_conv2 upt_0)
by (smt * One_nat_def app_tl_hd_list attack.simps(1) length_greater_0_conv list.sel(1) list.sel(3) list.simps(3) list.simps(8) list.size(3) map_fst nth_Cons_0 nth_Cons_pos self_append_conv2 snd_conv tl_app_in tl_append2 upt_0)
qed
qed
qed
lemma Compl_step4: "I ≠ {} ⟹ finite I ⟹ ¬ I ⊆ s ⟹
(∃ lI. set lI = {x. x ∈ I ∧ x ∉ s} ∧ (∃ Sj :: ((('s :: state) set)list) list.
length Sj = length lI ∧ nodup_all lI ∧
(∀ j < length Sj. (((Sj ! j) ≠ []) ∧ (tl (Sj ! j) ≠ []) ∧
((Sj ! j) ! 0, (Sj ! j) ! (length (Sj ! j) - 1)) = ({lI ! j},s) ∧
(∀ i < (length (Sj ! j) - 1). ⊢ 𝒩⇘((Sj ! j) ! i, (Sj ! j) ! (i+1) )⇙
)))))
⟹ ∃ (A :: ('s :: state) attree). ⊢ A ∧ attack A = (I,s)"
proof (erule exE, erule conjE, erule exE, erule conjE)
fix lI Sj
assume a: "I ≠ {}" and b: "finite I" and c: "¬ I ⊆ s"
and d: "set lI = {x::'s ∈ I. x ∉ s}" and e: "length Sj = length lI"
and f: "nodup_all lI ∧
(∀j<length Sj. Sj ! j ≠ [] ∧
tl (Sj ! j) ≠ [] ∧
(Sj ! j ! (0), Sj ! j ! (length (Sj ! j) - (1))) = ({lI ! j}, s) ∧
(∀i<length (Sj ! j) - (1). ⊢𝒩⇘(Sj ! j ! i, Sj ! j ! (i + (1)))⇙))"
show "∃A::'s attree. ⊢A ∧ attack A = (I, s)"
apply (rule_tac x =
"[([] ⊕⇩∨⇗({x. x ∈ I ∧ x ∈ s}, s)⇖),
([[ 𝒩⇘((Sj ! j) ! i, (Sj ! j) ! (i + (1)))⇙.
i ← [0..<(length (Sj ! j)-(1))]] ⊕⇩∧⇗(({lI ! j},s))⇖. j ← [0..<(length Sj)]]
⊕⇩∨⇗({x. x ∈ I ∧ x ∉ s},s)⇖)] ⊕⇩∨⇗(I, s)⇖" in exI)
proof
show "⊢([[] ⊕⇩∨⇗({x::'s ∈ I. x ∈ s}, s)⇖,
map (λj.
((map (λi. 𝒩⇘(Sj ! j ! i, Sj ! j ! (i + (1)))⇙)
[0..<length (Sj ! j) - (1)]) ⊕⇩∧⇗({lI ! j}, s)⇖))
[0..<length Sj] ⊕⇩∨⇗({x::'s ∈ I. x ∉ s}, s)⇖] ⊕⇩∨⇗(I, s)⇖)"
proof -
have g: "I - {x::'s ∈ I. x ∈ s} = {x::'s ∈ I. x ∉ s}" by blast
thus "⊢([[] ⊕⇩∨⇗({x::'s ∈ I. x ∈ s}, s)⇖,
(map (λj.
((map (λi. 𝒩⇘(Sj ! j ! i, Sj ! j ! (i + (1)))⇙)
[0..<length (Sj ! j) - (1)]) ⊕⇩∧⇗({lI ! j}, s)⇖))
[0..<length Sj]) ⊕⇩∨⇗({x::'s ∈ I. x ∉ s}, s)⇖] ⊕⇩∨⇗(I, s)⇖)"
apply (subst att_or, simp)
proof
show "I - {x ∈ I. x ∈ s} = {x ∈ I. x ∉ s} ⟹ ⊢([] ⊕⇩∨⇗({x ∈ I. x ∈ s}, s)⇖)"
by (metis (no_types, lifting) CollectD att_or_empty_back subsetI)
next show "I - {x ∈ I. x ∈ s} = {x ∈ I. x ∉ s} ⟹
⊢([map (λj. ((map (λi. 𝒩⇘(Sj ! j ! i, Sj ! j ! Suc i)⇙) [0..<length (Sj ! j) - Suc 0]) ⊕⇩∧⇗({lI ! j}, s)⇖))
[0..<length Sj] ⊕⇩∨⇗({x ∈ I. x ∉ s}, s)⇖] ⊕⇩∨⇗({x ∈ I. x ∉ s}, s)⇖)"
text ‹Use lemma @{text ‹list_or_upt›} to distribute attack validity over list lI›
proof (erule ssubst, subst att_or, simp, rule subst, rule d, rule_tac lI = lI in list_or_upt)
show "lI ≠ []"
using c d by auto
next show "⋀i.
i < length lI ⟹
⊢(map (λj.
((map (λi. 𝒩⇘(Sj ! j ! i, Sj ! j ! Suc i)⇙)
[0..<length (Sj ! j) - Suc (0)]) ⊕⇩∧⇗({lI ! j}, s)⇖))
[0..<length Sj] !
i) ∧
(attack
(map (λj.
((map (λi. 𝒩⇘(Sj ! j ! i, Sj ! j ! Suc i)⇙)
[0..<length (Sj ! j) - Suc (0)]) ⊕⇩∧⇗({lI ! j}, s)⇖))
[0..<length Sj] !
i) =
({lI ! i}, s))"
proof (simp add: a b c d e f)
show "⋀i.
i < length lI ⟹
⊢(map (λia. 𝒩⇘(Sj ! i ! ia, Sj ! i ! Suc ia)⇙)
[0..<length (Sj ! i) - Suc (0)] ⊕⇩∧⇗({lI ! i}, s)⇖)"
proof -
fix i :: nat
assume a1: "i < length lI"
have "∀n. ⊢map (λna. 𝒩⇘(Sj ! n ! na, Sj ! n ! Suc na)⇙) [0..< length (Sj ! n) - 1] ⊕⇩∧⇗(Sj ! n ! 0, Sj ! n ! (length (Sj ! n) - 1))⇖ ∨ ¬ n < length Sj"
by (metis (no_types) One_nat_def add.right_neutral add_Suc_right base_list_and f)
then show "⊢map (λn. 𝒩⇘(Sj ! i ! n, Sj ! i ! Suc n)⇙) [0..< length (Sj ! i) - Suc 0] ⊕⇩∧⇗({lI ! i}, s)⇖"
using a1 by (metis (no_types) One_nat_def e f)
qed
qed
qed (auto simp add: e f)
qed
qed
qed auto
qed
subsubsection ‹Main Theorem Completeness›
theorem Completeness: "I ≠ {} ⟹ finite I ⟹
Kripke {s :: ('s :: state). ∃ i ∈ I. (i →⇩i* s)} (I :: ('s :: state)set) ⊢ EF s
⟹ ∃ (A :: ('s :: state) attree). ⊢ A ∧ attack A = (I,s)"
proof (case_tac "I ⊆ s")
show "I ≠ {} ⟹ finite I ⟹
Kripke {s::'s. ∃i::'s∈I. i →⇩i* s} I ⊢ EF s ⟹ I ⊆ s ⟹ ∃A::'s attree. ⊢A ∧ attack A = (I, s)"
using att_or_empty_back attack.simps(3) by blast
next
show "I ≠ {} ⟹ finite I ⟹
Kripke {s::'s. ∃i::'s∈I. i →⇩i* s} I ⊢ EF s ⟹ ¬ I ⊆ s
⟹ ∃A::'s attree. ⊢A ∧ attack A = (I, s)"
by (iprover intro: Compl_step1 Compl_step2 Compl_step3 Compl_step4 elim: )
qed
subsubsection ‹Contrapositions of Correctness and Completeness›
lemma contrapos_compl:
"I ≠ {} ⟹ finite I ⟹
(¬ (∃ (A :: ('s :: state) attree). ⊢ A ∧ attack A = (I, - s))) ⟹
¬ (Kripke {s. ∃i∈I. i →⇩i* s} I ⊢ EF (- s))"
using Completeness by auto
lemma contrapos_corr:
"(¬(Kripke {s :: ('s :: state). ∃ i ∈ I. (i →⇩i* s)} I ⊢ EF s))
⟹ attack A = (I,s)
⟹ ¬ (⊢ A)"
using AT_EF by blast
endTheory Infrastructure
section ‹Infrastructures›
text ‹The Isabelle Infrastructure framework supports the representation of infrastructures
as graphs with actors and policies attached to nodes. These infrastructures
are the {\it states} of the Kripke structure.
The transition between states is triggered by non-parametrized
actions @{text ‹get, move, eval, put›} executed by actors.
Actors are given by an abstract type @{text ‹actor›} and a function
@{text ‹Actor›} that creates elements of that type from identities
(of type @{text ‹string›}). Policies are given by pairs of predicates
(conditions) and sets of (enabled) actions.›
subsection ‹Actors, actions, and data labels›
theory Infrastructure
imports AT
begin
datatype action = get | move | eval | put
typedecl actor
type_synonym identity = string
consts Actor :: "string ⇒ actor"
type_synonym policy = "((actor ⇒ bool) * action set)"
definition ID :: "[actor, string] ⇒ bool"
where "ID a s ≡ (a = Actor s)"
text ‹The Decentralised Label Model (DLM) \cite{ml:98} introduced the idea to
label data by owners and readers. We pick up this idea and formalize
a new type to encode the owner and the set of readers as a pair.
The first element is the owner of a data item, the second one is the
set of all actors that may access the data item.
This enables the unique security
labelling of data within the system additionally taking the ownership into
account.›
type_synonym data = nat
type_synonym dlm = "actor * actor set"
subsection ‹Infrastructure graphs and policies›
text‹Actors are contained in an infrastructure graph. An @{text ‹igraph›} contains
a set of location pairs representing the topology of the infrastructure
as a graph of nodes and a list of actor identities associated to each node
(location) in the graph.
Also an @{text ‹igraph›} associates actors to a pair of string sets by
a pair-valued function whose first range component is a set describing
the credentials in the possession of an actor and the second component
is a set defining the roles the actor can take on. More importantly in this
context, an @{text ‹igraph›} assigns locations to a pair of a string that defines
the state of the component and an element of type @{text ‹(dlm * data) set›}. This
set of labelled data may represent a condition on that data.
Corresponding projection functions for each of these components of an
@{text ‹igraph›} are provided; they are named @{text ‹gra›} for the actual set of pairs of
locations, @{text ‹agra›} for the actor map, @{text ‹cgra›} for the credentials,
and @{text ‹lgra›} for the state of a location and the data at that location.›
datatype location = Location nat
datatype igraph = Lgraph "(location * location)set" "location ⇒ identity set"
"actor ⇒ (string set * string set)"
"location ⇒ string * (dlm * data) set"
datatype infrastructure =
Infrastructure "igraph"
"[igraph, location] ⇒ policy set"
primrec loc :: "location ⇒ nat"
where "loc(Location n) = n"
primrec gra :: "igraph ⇒ (location * location)set"
where "gra(Lgraph g a c l) = g"
primrec agra :: "igraph ⇒ (location ⇒ identity set)"
where "agra(Lgraph g a c l) = a"
primrec cgra :: "igraph ⇒ (actor ⇒ string set * string set)"
where "cgra(Lgraph g a c l) = c"
primrec lgra :: "igraph ⇒ (location ⇒ string * (dlm * data) set)"
where "lgra(Lgraph g a c l) = l"
definition nodes :: "igraph ⇒ location set"
where "nodes g == { x. (? y. ((x,y): gra g) | ((y,x): gra g))}"
definition actors_graph :: "igraph ⇒ identity set"
where "actors_graph g == {x. ? y. y : nodes g ∧ x ∈ (agra g y)}"
text ‹There are projection functions text{@ ‹graphI›} and text{@ ‹delta›} when applied
to an infrastructure return the graph and the policy, respectively. Other projections
are introduced for the labels, the credential, and roles and to express their meaning.›
primrec graphI :: "infrastructure ⇒ igraph"
where "graphI (Infrastructure g d) = g"
primrec delta :: "[infrastructure, igraph, location] ⇒ policy set"
where "delta (Infrastructure g d) = d"
primrec tspace :: "[infrastructure, actor ] ⇒ string set * string set"
where "tspace (Infrastructure g d) = cgra g"
primrec lspace :: "[infrastructure, location ] ⇒ string * (dlm * data)set"
where "lspace (Infrastructure g d) = lgra g"
definition credentials :: "string set * string set ⇒ string set"
where "credentials lxl ≡ (fst lxl)"
definition has :: "[igraph, actor * string] ⇒ bool"
where "has G ac ≡ snd ac ∈ credentials(cgra G (fst ac))"
definition roles :: "string set * string set ⇒ string set"
where "roles lxl ≡ (snd lxl)"
definition role :: "[igraph, actor * string] ⇒ bool"
where "role G ac ≡ snd ac ∈ roles(cgra G (fst ac))"
definition isin :: "[igraph,location, string] ⇒ bool"
where "isin G l s ≡ s = fst (lgra G l)"
text ‹Predicates and projections for the labels to encode their meaning.›
definition owner :: "dlm * data ⇒ actor" where "owner d ≡ fst(fst d)"
definition owns :: "[igraph, location, actor, dlm * data] ⇒ bool"
where "owns G l a d ≡ owner d = a"
definition readers :: "dlm * data ⇒ actor set"
where "readers d ≡ snd (fst d)"
text ‹The predicate @{text ‹has_access›} is true for owners or readers.›
definition has_access :: "[igraph, location, actor, dlm * data] ⇒ bool"
where "has_access G l a d ≡ owns G l a d ∨ a ∈ readers d"
text ‹We define a type of functions that preserves the security labeling and a
corresponding function application operator.›
typedef label_fun = "{f :: dlm * data ⇒ dlm * data.
∀ x:: dlm * data. fst x = fst (f x)}"
by (fastforce)
definition secure_process :: "label_fun ⇒ dlm * data ⇒ dlm * data" (infixr "⇕" 50)
where "f ⇕ d ≡ (Rep_label_fun f) d"
text ‹The predicate atI -- mixfix syntax @{text ‹@⇘G⇙›} -- expresses that an actor (identity)
is at a certain location in an igraph.›
definition atI :: "[identity, igraph, location] ⇒ bool" ("_ @⇘(_)⇙ _" 50)
where "a @⇘G⇙ l ≡ a ∈ (agra G l)"
text ‹Policies specify the expected behaviour of actors of an infrastructure.
They are defined by the @{text ‹enables›} predicate:
an actor @{text ‹h›} is enabled to perform an action @{text ‹a›}
in infrastructure @{text ‹I›}, at location @{text ‹l›}
if there exists a pair @{text ‹(p,e)›} in the local policy of @{text ‹l›}
(@{text ‹delta I l›} projects to the local policy) such that the action
@{text ‹a›} is a member of the action set @{text ‹e›} and the policy
predicate @{text ‹p›} holds for actor @{text ‹h›}.›
definition enables :: "[infrastructure, location, actor, action] ⇒ bool"
where
"enables I l a a' ≡ (∃ (p,e) ∈ delta I (graphI I) l. a' ∈ e ∧ p a)"
text ‹The behaviour is the good behaviour, i.e. everything allowed by the policy of infrastructure I.›
definition behaviour :: "infrastructure ⇒ (location * actor * action)set"
where "behaviour I ≡ {(t,a,a'). enables I t a a'}"
text ‹The misbehaviour is the complement of the behaviour of an infrastructure I.›
definition misbehaviour :: "infrastructure ⇒ (location * actor * action)set"
where "misbehaviour I ≡ -(behaviour I)"
subsection "State transition on infrastructures"
text ‹The state transition defines how actors may act on infrastructures through actions
within the boundaries of the policy. It is given as an inductive definition over the
states which are infrastructures. This state transition relation is dependent on actions but also on
enabledness and the current state of the infrastructure.
First we introduce some auxiliary functions dealing
with repetitions in lists and actors moving in an igraph.›
primrec jonce :: "['a, 'a list] ⇒ bool"
where
jonce_nil: "jonce a [] = False" |
jonce_cons: "jonce a (x#ls) = (if x = a then (a ∉ (set ls)) else jonce a ls)"
definition move_graph_a :: "[identity, location, location, igraph] ⇒ igraph"
where "move_graph_a n l l' g ≡ Lgraph (gra g)
(if n ∈ ((agra g) l) & n ∉ ((agra g) l') then
((agra g)(l := (agra g l) - {n}))(l' := (insert n (agra g l')))
else (agra g))(cgra g)(lgra g)"
inductive state_transition_in :: "[infrastructure, infrastructure] ⇒ bool" ("(_ →⇩n _)" 50)
where
move: "⟦ G = graphI I; a @⇘G⇙ l; l ∈ nodes G; l' ∈ nodes G;
(a) ∈ actors_graph(graphI I); enables I l' (Actor a) move;
I' = Infrastructure (move_graph_a a l l' (graphI I))(delta I) ⟧ ⟹ I →⇩n I'"
| get : "⟦ G = graphI I; a @⇘G⇙ l; a' @⇘G⇙ l; has G (Actor a, z);
enables I l (Actor a) get;
I' = Infrastructure
(Lgraph (gra G)(agra G)
((cgra G)(Actor a' :=
(insert z (fst(cgra G (Actor a'))), snd(cgra G (Actor a')))))
(lgra G))
(delta I)
⟧ ⟹ I →⇩n I'"
| get_data : "G = graphI I ⟹ a @⇘G⇙ l ⟹
enables I l' (Actor a) get ⟹
((Actor a', as), n) ∈ snd (lgra G l') ⟹ Actor a ∈ as ⟹
I' = Infrastructure
(Lgraph (gra G)(agra G)(cgra G)
((lgra G)(l := (fst (lgra G l),
snd (lgra G l) ∪ {((Actor a', as), n)}))))
(delta I)
⟹ I →⇩n I'"
| process : "G = graphI I ⟹ a @⇘G⇙ l ⟹
enables I l (Actor a) eval ⟹
((Actor a', as), n) ∈ snd (lgra G l) ⟹ Actor a ∈ as ⟹
I' = Infrastructure
(Lgraph (gra G)(agra G)(cgra G)
((lgra G)(l := (fst (lgra G l),
snd (lgra G l) - {((Actor a', as), n)}
∪ {(f :: label_fun) ⇕ ((Actor a', as), n)}))))
(delta I)
⟹ I →⇩n I'"
| del_data : "G = graphI I ⟹ a ∈ actors G ⟹ l ∈ nodes G ⟹
((Actor a, as), n) ∈ snd (lgra G l) ⟹
I' = Infrastructure
(Lgraph (gra G)(agra G)(cgra G)
((lgra G)(l := (fst (lgra G l), snd (lgra G l) - {((Actor a, as), n)}))))
(delta I)
⟹ I →⇩n I'"
| put : "G = graphI I ⟹ a @⇘G⇙ l ⟹ enables I l (Actor a) put ⟹
I' = Infrastructure
(Lgraph (gra G)(agra G)(cgra G)
((lgra G)(l := (s, snd (lgra G l) ∪ {((Actor a, as), n)}))))
(delta I)
⟹ I →⇩n I'"
text ‹Note that the type infrastructure can now be instantiated to the axiomatic type class
@{text‹state›} which enables the use of the underlying Kripke structures and CTL.›
instantiation "infrastructure" :: state
begin
definition
state_transition_infra_def: "(i →⇩i i') = (i →⇩n (i' :: infrastructure))"
instance
by (rule MC.class.MC.state.of_class.intro)
definition state_transition_in_refl ("(_ →⇩n* _)" 50)
where "s →⇩n* s' ≡ ((s,s') ∈ {(x,y). state_transition_in x y}⇧*)"
end
lemma move_graph_eq: "move_graph_a a l l g = g"
by (simp add: move_graph_a_def, case_tac g, force)
end
Theory GDPRhealthcare
section ‹Application example from IoT healthcare›
text ‹The example of an IoT healthcare systems is taken from the context of the CHIST-ERA project
SUCCESS \cite{suc:16}. In this system architecture, data is collected by sensors
in the home or via a smart phone helping to monitor bio markers of the patient. The data
collection is in a cloud based server to enable hospitals (or scientific institutions)
to access the data which is controlled via the smart phone.
The identities Patient and Doctor represent patients
and their doctors; double quotes ''s'' indicate strings
in Isabelle/HOL.
The global policy is `only the patient and the doctor can access the data in the cloud'.›
theory GDPRhealthcare
imports Infrastructure
begin
text ‹Local policies are represented as a function over an @{text ‹igraph G›}
that additionally assigns each location of a scenario to its local policy
given as a pair of requirements to an actor (first element of the pair) in
order to grant him actions in the location (second element of the pair).
The predicate @{text ‹@G›} checks whether an actor is at a given location
in the @{text ‹igraph G›}.›
locale scenarioGDPR =
fixes gdpr_actors :: "identity set"
defines gdpr_actors_def: "gdpr_actors ≡ {''Patient'', ''Doctor''}"
fixes gdpr_locations :: "location set"
defines gdpr_locations_def: "gdpr_locations ≡
{Location 0, Location 1, Location 2, Location 3}"
fixes sphone :: "location"
defines sphone_def: "sphone ≡ Location 0"
fixes home :: "location"
defines home_def: "home ≡ Location 1"
fixes hospital :: "location"
defines hospital_def: "hospital ≡ Location 2"
fixes cloud :: "location"
defines cloud_def: "cloud ≡ Location 3"
fixes global_policy :: "[infrastructure, identity] ⇒ bool"
defines global_policy_def: "global_policy I a ≡ a ≠ ''Doctor''
⟶ ¬(enables I hospital (Actor a) eval)"
fixes global_policy' :: "[infrastructure, identity] ⇒ bool"
defines global_policy'_def: "global_policy' I a ≡ a ∉ gdpr_actors
⟶ ¬(enables I cloud (Actor a) get)"
fixes ex_creds :: "actor ⇒ (string set * string set)"
defines ex_creds_def: "ex_creds ≡ (λ x. if x = Actor ''Patient'' then
({''PIN'',''skey''}, {}) else
(if x = Actor ''Doctor'' then
({''PIN''},{}) else ({},{})))"
fixes ex_locs :: "location ⇒ string * (dlm * data) set"
defines "ex_locs ≡ (λ x. if x = cloud then
(''free'',{((Actor ''Patient'',{Actor ''Doctor''}),42)})
else ('''',{}))"
fixes ex_loc_ass :: "location ⇒ identity set"
defines ex_loc_ass_def: "ex_loc_ass ≡
(λ x. if x = home then {''Patient''}
else (if x = hospital then {''Doctor'', ''Eve''}
else {}))"
fixes ex_graph :: "igraph"
defines ex_graph_def: "ex_graph ≡ Lgraph
{(home, cloud), (sphone, cloud), (cloud,hospital)}
ex_loc_ass
ex_creds ex_locs"
fixes ex_graph' :: "igraph"
defines ex_graph'_def: "ex_graph' ≡ Lgraph
{(home, cloud), (sphone, cloud), (cloud,hospital)}
(λ x. if x = cloud then {''Patient''} else
(if x = hospital then {''Doctor'',''Eve''} else {}))
ex_creds ex_locs"
fixes ex_graph'' :: "igraph"
defines ex_graph''_def: "ex_graph'' ≡ Lgraph
{(home, cloud), (sphone, cloud), (cloud,hospital)}
(λ x. if x = cloud then {''Patient'', ''Eve''} else
(if x = hospital then {''Doctor''} else {}))
ex_creds ex_locs"
fixes local_policies :: "[igraph, location] ⇒ policy set"
defines local_policies_def: "local_policies G ≡
(λ x. if x = home then
{(λ y. True, {put,get,move,eval})}
else (if x = sphone then
{((λ y. has G (y, ''PIN'')), {put,get,move,eval})}
else (if x = cloud then
{(λ y. True, {put,get,move,eval})}
else (if x = hospital then
{((λ y. (∃ n. (n @⇘G⇙ hospital) ∧ Actor n = y ∧
has G (y, ''skey''))), {put,get,move,eval})} else {}))))"
fixes gdpr_scenario :: "infrastructure"
defines gdpr_scenario_def:
"gdpr_scenario ≡ Infrastructure ex_graph local_policies"
fixes Igdpr :: "infrastructure set"
defines Igdpr_def:
"Igdpr ≡ {gdpr_scenario}"
fixes gdpr_scenario' :: "infrastructure"
defines gdpr_scenario'_def:
"gdpr_scenario' ≡ Infrastructure ex_graph' local_policies"
fixes GDPR' :: "infrastructure set"
defines GDPR'_def:
"GDPR' ≡ {gdpr_scenario'}"
fixes gdpr_scenario'' :: "infrastructure"
defines gdpr_scenario''_def:
"gdpr_scenario'' ≡ Infrastructure ex_graph'' local_policies"
fixes GDPR'' :: "infrastructure set"
defines GDPR''_def:
"GDPR'' ≡ {gdpr_scenario''}"
fixes gdpr_states
defines gdpr_states_def: "gdpr_states ≡ { I. gdpr_scenario →⇩i* I }"
fixes gdpr_Kripke
defines "gdpr_Kripke ≡ Kripke gdpr_states {gdpr_scenario}"
fixes sgdpr
defines "sgdpr ≡ {x. ¬ (global_policy' x ''Eve'')}"
begin
subsection ‹Using Attack Tree Calculus›
text ‹Since we consider a predicate transformer semantics, we use sets of states
to represent properties. For example, the attack property is given by the above
@{text ‹set sgdpr›}.
The attack we are interested in is to see whether for the scenario
@{text ‹gdpr scenario ≡ Infrastructure ex_graph local_policies›}
from the initial state
@{text ‹Igdpr ≡{gdpr scenario}›},
the critical state
@{text ‹sgdpr›} can be reached, i.e., is there a valid attack @{text ‹(Igdpr,sgdpr)›}?
We first present a number of lemmas showing single and multi-step state transitions
for relevant states reachable from our @{text ‹gdpr_scenario›}.›
lemma step1: "gdpr_scenario →⇩n gdpr_scenario'"
proof (rule_tac l = home and a = "''Patient''" and l' = cloud in move)
show "graphI gdpr_scenario = graphI gdpr_scenario" by (rule refl)
next show "''Patient'' @⇘graphI gdpr_scenario⇙ home"
by (simp add: gdpr_scenario_def ex_graph_def ex_loc_ass_def atI_def nodes_def)
next show "home ∈ nodes (graphI gdpr_scenario)"
by (simp add: gdpr_scenario_def ex_graph_def ex_loc_ass_def atI_def nodes_def, blast)
next show "cloud ∈ nodes (graphI gdpr_scenario)"
by (simp add: gdpr_scenario_def nodes_def ex_graph_def, blast)
next show "''Patient'' ∈ actors_graph (graphI gdpr_scenario)"
by (simp add: actors_graph_def gdpr_scenario_def ex_graph_def ex_loc_ass_def nodes_def, blast)
next show "enables gdpr_scenario cloud (Actor ''Patient'') move"
by (simp add: enables_def gdpr_scenario_def ex_graph_def local_policies_def
ex_creds_def ex_locs_def has_def credentials_def)
next show "gdpr_scenario' =
Infrastructure (move_graph_a ''Patient'' home cloud (graphI gdpr_scenario)) (delta gdpr_scenario)"
apply (simp add: gdpr_scenario'_def ex_graph'_def move_graph_a_def
gdpr_scenario_def ex_graph_def home_def cloud_def hospital_def
ex_loc_ass_def ex_creds_def)
apply (rule ext)
by (simp add: hospital_def)
qed
lemma step1r: "gdpr_scenario →⇩n* gdpr_scenario'"
proof (simp add: state_transition_in_refl_def)
show " (gdpr_scenario, gdpr_scenario') ∈ {(x::infrastructure, y::infrastructure). x →⇩n y}⇧*"
by (insert step1, auto)
qed
lemma step2: "gdpr_scenario' →⇩n gdpr_scenario''"
proof (rule_tac l = hospital and a = "''Eve''" and l' = cloud in move, rule refl)
show "''Eve'' @⇘graphI gdpr_scenario'⇙ hospital"
by (simp add: gdpr_scenario'_def ex_graph'_def hospital_def cloud_def atI_def nodes_def)
next show "hospital ∈ nodes (graphI gdpr_scenario')"
by (simp add: gdpr_scenario'_def ex_graph'_def hospital_def cloud_def atI_def nodes_def, blast)
next show "cloud ∈ nodes (graphI gdpr_scenario')"
by (simp add: gdpr_scenario'_def nodes_def ex_graph'_def, blast)
next show "''Eve'' ∈ actors_graph (graphI gdpr_scenario')"
by (simp add: actors_graph_def gdpr_scenario'_def ex_graph'_def nodes_def
hospital_def cloud_def, blast)
next show "enables gdpr_scenario' cloud (Actor ''Eve'') move"
by (simp add: enables_def gdpr_scenario'_def ex_graph_def local_policies_def
ex_creds_def ex_locs_def has_def credentials_def cloud_def sphone_def)
next show "gdpr_scenario'' =
Infrastructure (move_graph_a ''Eve'' hospital cloud (graphI gdpr_scenario')) (delta gdpr_scenario')"
apply (simp add: gdpr_scenario'_def ex_graph''_def move_graph_a_def gdpr_scenario''_def
ex_graph'_def home_def cloud_def hospital_def ex_creds_def)
apply (rule ext)
apply (simp add: hospital_def)
by blast
qed
lemma step2r: "gdpr_scenario' →⇩n* gdpr_scenario''"
proof (simp add: state_transition_in_refl_def)
show "(gdpr_scenario', gdpr_scenario'') ∈ {(x::infrastructure, y::infrastructure). x →⇩n y}⇧*"
by (insert step2, auto)
qed
text ‹For the Kripke structure
@{text ‹gdpr_Kripke ≡ Kripke { I. gdpr_scenario →⇩i* I } {gdpr_scenario}›}
we first derive a valid and-attack using the attack tree proof calculus.
@{text ‹"⊢[𝒩⇘(Igdpr,GDPR')⇙, 𝒩⇘(GDPR',sgdpr)⇙] ⊕⇩∧⇗(Igdpr,sgdpr)⇖›}
The set @{text ‹GDPR'›} (see above) is an intermediate state where Eve accesses the cloud.›
lemma gdpr_ref: "[𝒩⇘(Igdpr,sgdpr)⇙] ⊕⇩∧⇗(Igdpr,sgdpr)⇖ ⊑
([𝒩⇘(Igdpr,GDPR')⇙, 𝒩⇘(GDPR',sgdpr)⇙] ⊕⇩∧⇗(Igdpr,sgdpr)⇖)"
proof (rule_tac l = "[]" and l' = "[𝒩⇘(Igdpr,GDPR')⇙, 𝒩⇘(GDPR',sgdpr)⇙]" and
l'' = "[]" and si = Igdpr and si' = Igdpr and
si'' = sgdpr and si''' = sgdpr in refI, simp, rule refl)
show "([𝒩⇘(Igdpr, GDPR')⇙, 𝒩⇘(GDPR', sgdpr)⇙] ⊕⇩∧⇗(Igdpr, sgdpr)⇖) =
([] @ [𝒩⇘(Igdpr, GDPR')⇙, 𝒩⇘(GDPR', sgdpr)⇙] @ [] ⊕⇩∧⇗(Igdpr, sgdpr)⇖)"
by simp
qed
lemma att_gdpr: "⊢([𝒩⇘(Igdpr,GDPR')⇙, 𝒩⇘(GDPR',sgdpr)⇙] ⊕⇩∧⇗(Igdpr,sgdpr)⇖)"
proof (subst att_and, simp, rule conjI)
show " ⊢𝒩⇘(Igdpr, GDPR')⇙"
apply (simp add: Igdpr_def GDPR'_def att_base)
using state_transition_infra_def step1 by blast
next
have "¬ global_policy' gdpr_scenario'' ''Eve''" "gdpr_scenario' →⇩n gdpr_scenario''"
using step2
by (auto simp: global_policy'_def gdpr_scenario''_def gdpr_actors_def
enables_def local_policies_def cloud_def sphone_def intro!: step2)
then show "⊢([𝒩⇘(GDPR', sgdpr)⇙] ⊕⇩∧⇗(GDPR', sgdpr)⇖)"
apply (subst att_and)
apply (simp add: GDPR'_def sgdpr_def att_base)
using state_transition_infra_def by blast
qed
lemma gdpr_abs_att: "⊢⇩V([𝒩⇘(Igdpr,sgdpr)⇙] ⊕⇩∧⇗(Igdpr,sgdpr)⇖)"
by (rule ref_valI, rule gdpr_ref, rule att_gdpr)
text ‹We can then simply apply the Correctness theorem @{text ‹AT EF›} to immediately
prove the following CTL statement.
@{text ‹gdpr_Kripke ⊢ EF sgdpr›}
This application of the meta-theorem of Correctness of attack trees saves us
proving the CTL formula tediously by exploring the state space.›
lemma gdpr_att: "gdpr_Kripke ⊢ EF {x. ¬(global_policy' x ''Eve'')}"
proof -
have a: " ⊢([𝒩⇘(Igdpr, GDPR')⇙, 𝒩⇘(GDPR', sgdpr)⇙] ⊕⇩∧⇗(Igdpr, sgdpr)⇖)"
by (rule att_gdpr)
hence "(Igdpr,sgdpr) = attack ([𝒩⇘(Igdpr, GDPR')⇙, 𝒩⇘(GDPR', sgdpr)⇙] ⊕⇩∧⇗(Igdpr, sgdpr)⇖)"
by simp
hence "Kripke {s::infrastructure. ∃i::infrastructure∈Igdpr. i →⇩i* s} Igdpr ⊢ EF sgdpr"
using ATV_EF gdpr_abs_att by fastforce
thus "gdpr_Kripke ⊢ EF {x::infrastructure. ¬ global_policy' x ''Eve''}"
by (simp add: gdpr_Kripke_def gdpr_states_def Igdpr_def sgdpr_def)
qed
theorem gdpr_EF: "gdpr_Kripke ⊢ EF sgdpr"
using gdpr_att sgdpr_def by blast
text ‹Similarly, vice-versa, the CTL statement proved in @{text ‹gdpr_EF›}
can now be directly translated into Attack Trees using the Completeness
Theorem\footnote{This theorem could easily
be proved as a direct instance of @{text ‹att_gdpr›} above but we want to illustrate
an alternative proof method using Completeness here.}.›
theorem gdpr_AT: "∃ A. ⊢ A ∧ attack A = (Igdpr,sgdpr)"
proof -
have a: "gdpr_Kripke ⊢ EF sgdpr " by (rule gdpr_EF)
have b: "Igdpr ≠ {}" by (simp add: Igdpr_def)
thus "∃A::infrastructure attree. ⊢A ∧ attack A = (Igdpr, sgdpr)"
proof (rule Completeness)
show "Kripke {s. ∃i∈Igdpr. i →⇩i* s} Igdpr ⊢ EF sgdpr"
using a by (simp add: gdpr_Kripke_def Igdpr_def gdpr_states_def)
qed (auto simp: Igdpr_def)
qed
text ‹Conversely, since we have an attack given by rule @{text ‹gdpr_AT›}, we can immediately
infer @{text ‹EF s›} using Correctness @{text ‹AT_EF›}\footnote{Clearly, this theorem is identical
to @{text ‹gdpr_EF›} and could thus be inferred from that one but we want to show here an
alternative way of proving it using the Correctness theorem @{text ‹AT_EF›}.}.›
theorem gdpr_EF': "gdpr_Kripke ⊢ EF sgdpr"
using gdpr_AT by (auto simp: gdpr_Kripke_def gdpr_states_def Igdpr_def dest: AT_EF)
section ‹Data Protection by Design for GDPR compliance›
subsection ‹General Data Protection Regulation (GDPR)›
text ‹Since 26th May 2018, the GDPR has become mandatory within the European Union and hence
also for any supplier of IT products. Breaches of the regulation will be fined with penalties
of 20 Million EUR. Despite the relatively large size of the document of 209 pages, the technically
relevant portion for us is only about 30 pages (Pages 81–111, Chapters I to Chapter III, Section 3).
In summary, Chapter III specifies that the controller must give the data subject read access (1)
to any information, communications, and “meta-data” of the data, e.g., retention time and purpose.
In addition, the system must enable deletion of data (2) and restriction of processing.
An invariant condition for data processing resulting from these Articles is that the system functions
must preserve any of the access rights of personal data (3).
Using labeled data, we can now express the essence of Article 4 Paragraph (1):
’personal data’ means any information relating to an identified or identifiable natural
person (’data subject’).
The labels of data must not be changed by processing: we have identified this as
an invariant (3) resulting from the GDPR above. This invariant is formalized in
our Isabelle model by the type definition of functions on labeled data @{text ‹label_fun›}
(see Section 4.2) that preserve the data labels.›
subsection ‹Policy enforcement and privacy preservation›
text ‹We can now use the labeled data to encode the privacy constraints of the
GDPR in the rules. For example, the get data rule (see Section 4.3) has labelled data
@{text ‹((Actor a’, as), n)›} and uses the labeling in the precondition to guarantee
that only entitled users can get data.
We can prove that processing preserves ownership as defined in the initial state for all paths
globally (AG) within the Kripke structure and in all locations of the graph.›
lemma gdpr_three: "h ∈ gdpr_actors ⟹ l ∈ gdpr_locations ⟹
owns (Igraph gdpr_scenario) l (Actor h) d ⟹
gdpr_Kripke ⊢ AG {x. ∀ l ∈ gdpr_locations. owns (Igraph x) l (Actor h) d }"
proof (simp add: gdpr_Kripke_def check_def, rule conjI)
show "gdpr_scenario ∈ gdpr_states" by (simp add: gdpr_states_def state_transition_refl_def)
next
show "h ∈ gdpr_actors ⟹
l ∈ gdpr_locations ⟹
owns (Igraph gdpr_scenario) l (Actor h) d ⟹
gdpr_scenario ∈ AG {x::infrastructure. ∀l∈gdpr_locations. owns (Igraph x) l (Actor h) d}"
apply (simp add: AG_def gfp_def)
apply (rule_tac x = "{x::infrastructure. ∀l∈gdpr_locations. owns (Igraph x) l (Actor h) d}" in exI)
by (auto simp: AX_def gdpr_scenario_def owns_def)
qed
text ‹The final application example of Correctness contraposition
shows that there is no attack to ownership possible.
The proved meta-theory for attack trees can be applied to facilitate the proof.
The contraposition of the Correctness property grants that if there is no attack on
@{text ‹(I,¬f)›}, then @{text ‹(EF ¬f)›} does not hold in the Kripke structure. This
yields the theorem since the @{text ‹AG f›} statement corresponds to @{text ‹¬(EF ¬f)›}.
›
theorem no_attack_gdpr_three:
"h ∈ gdpr_actors ⟹ l ∈ gdpr_locations ⟹
owns (Igraph gdpr_scenario) l (Actor h) d ⟹
attack A = (Igdpr, -{x. ∀ l ∈ gdpr_locations. owns (Igraph x) l (Actor h) d })
⟹ ¬ (⊢ A)"
proof (rule_tac I = Igdpr and
s = "-{x::infrastructure. ∀l∈gdpr_locations. owns (Igraph x) l (Actor h) d}"
in contrapos_corr)
show "h ∈ gdpr_actors ⟹
l ∈ gdpr_locations ⟹
owns (Igraph gdpr_scenario) l (Actor h) d ⟹
attack A = (Igdpr, - {x::infrastructure. ∀l∈gdpr_locations. owns (Igraph x) l (Actor h) d}) ⟹
¬ (Kripke {s::infrastructure. ∃i::infrastructure∈Igdpr. i →⇩i* s}
Igdpr ⊢ EF (- {x::infrastructure. ∀l∈gdpr_locations. owns (Igraph x) l (Actor h) d}))"
apply (rule AG_imp_notnotEF)
apply (simp add: gdpr_Kripke_def Igdpr_def gdpr_states_def)
using Igdpr_def gdpr_Kripke_def gdpr_states_def gdpr_three by auto
qed
end
end