# Theory MC

section "Kripke structures and CTL"

text ‹We apply Kripke structures and CTL to model state based systems and analyse properties under
dynamic state changes. Snapshots of systems are the states on which we define a state transition.
Temporal logic is then employed to express security and privacy properties.›
theory MC
imports Main
begin

subsection "Lemmas to support least and greatest fixpoints"

lemma predtrans_empty:
assumes "mono (τ :: 'a set ⇒ 'a set)"
shows "∀ i. (τ ^^ i) ({}) ⊆ (τ ^^(i + 1))({})"
using assms funpow_decreasing le_add1 by blast

lemma ex_card: "finite S ⟹ ∃ n:: nat. card S = n"
by simp

lemma less_not_le: "⟦(x:: nat) < y; y ≤ x⟧ ⟹ False"
by arith

lemma infchain_outruns_all:
assumes "finite (UNIV :: 'a set)"
and "∀i :: nat. ((τ :: 'a set ⇒ 'a set)^^ i) ({}:: 'a set) ⊂ (τ ^^ (i + 1)) {}"
shows "∀j :: nat. ∃i :: nat. j < card ((τ ^^ i) {})"
proof (rule allI, induct_tac j)
show "∃i. 0 < card ((τ ^^ i) {})" using assms
by (metis bot.not_eq_extremum card_gt_0_iff finite_subset subset_UNIV)
next show "⋀j n. ∃i. n < card ((τ ^^ i) {})
⟹ ∃i. Suc n < card ((τ ^^ i) {})"
proof -
fix j n
assume a: "∃i. n < card ((τ ^^ i) {})"
obtain i where "n < card ((τ ^^ i) {})"
using a by blast
thus "∃ i. Suc n < card ((τ ^^ i) {})" using assms
by (meson finite_subset le_less_trans le_simps(3) psubset_card_mono subset_UNIV)
qed
qed

lemma no_infinite_subset_chain:
assumes "finite (UNIV :: 'a set)"
and    "mono (τ :: ('a set ⇒ 'a set))"
and    "∀i :: nat. ((τ :: 'a set ⇒ 'a set) ^^ i) {} ⊂ (τ ^^ (i + (1 :: nat))) ({} :: 'a set)"
shows   "False"
text ‹Proof idea: since @{term "UNIV"} is finite, we have from @{text ‹ex_card›} that there is
an n with @{term "card UNIV = n"}. Now, use @{text ‹infchain_outruns_all›} to show as
@{term "∃ i :: nat. card UNIV < card ((τ ^^ i) {})"}.
Since all sets are subsets of @{term "UNIV"}, we also have
@{term "card ((τ ^^ i) {}) ≤ card UNIV"}:
Contradiction!, i.e. proof of False  ›
proof -
have a: "∀ (j :: nat). (∃ (i :: nat). (j :: nat) < card((τ ^^ i)({} :: 'a set)))" using assms
by (erule_tac τ = τ in infchain_outruns_all)
hence b: "∃ (n :: nat). card(UNIV :: 'a set) = n" using assms
by (erule_tac S = UNIV in ex_card)
from this obtain n where c: "card(UNIV :: 'a set) = n" by (erule exE)
hence   d: "∃i. card UNIV < card ((τ ^^ i) {})" using a
by (drule_tac x = "card UNIV" in spec)
from this obtain i where e: "card (UNIV :: 'a set) < card ((τ ^^ i) {})"
by (erule exE)
hence f: "(card((τ ^^ i){})) ≤ (card (UNIV :: 'a set))" using assms
apply (erule_tac A = "((τ ^^ i){})" in Finite_Set.card_mono)
by (rule subset_UNIV)
thus "False" using e
by (erule_tac y = "card((τ ^^ i){})" in less_not_le)
qed

lemma finite_fixp:
assumes "finite(UNIV :: 'a set)"
and "mono (τ :: ('a set ⇒ 'a set))"
shows "∃ i. (τ ^^ i) ({}) = (τ ^^(i + 1))({})"
text ‹Proof idea:
with @{text predtrans_empty} we know

@{term "∀ i. (τ ^^ i){} ⊆ (τ ^^(i + 1))({})"} (1).

@{term "∃ i.  (τ ^^ i)({}) ⊇ (τ ^^(i + 1))({})"} (2),

we can get the goal together with equalityI
@{text "⊆ + ⊇ ⟶ ="}.
To prove (1) we observe that
@{term "(τ ^^ i)({}) ⊇ (τ ^^(i + 1))({})"}
can be inferred from
@{term "¬((τ ^^ i)({}) ⊆ (τ ^^(i + 1))({}))"}
and (1).
Finally, the latter is solved directly by @{text ‹no_infinite_subset_chain›}.›
proof -
have a: "∀i. (τ ^^ i) ({}:: 'a set) ⊆ (τ ^^ (i + (1))) {}"
by(rule predtrans_empty, rule assms(2))
have a3: "¬ (∀ i :: nat. (τ ^^ i) {} ⊂ (τ ^^(i + 1)) {})"
by (rule notI, rule no_infinite_subset_chain, (rule assms)+)
hence b: "(∃ i :: nat. ¬((τ ^^ i) {} ⊂ (τ ^^(i + 1)) {}))" using assms a3
by blast
thus "∃ i. (τ ^^ i) ({}) = (τ ^^(i + 1))({})" using a
by blast
qed

lemma predtrans_UNIV:
assumes "mono (τ :: ('a set ⇒ 'a set))"
shows "∀ i. (τ ^^ i) (UNIV) ⊇ (τ ^^(i + 1))(UNIV)"
proof (rule allI, induct_tac i)
show "(τ ^^ ((0) + (1))) UNIV ⊆ (τ ^^ (0)) UNIV"
by simp
next show "⋀(i) n.
(τ ^^ (n + (1))) UNIV ⊆ (τ ^^ n) UNIV ⟹ (τ ^^ (Suc n + (1))) UNIV ⊆ (τ ^^ Suc n) UNIV"
proof -
fix i n
assume a: "(τ ^^ (n + (1))) UNIV ⊆ (τ ^^ n) UNIV"
have "(τ ((τ ^^ n) UNIV)) ⊇ (τ ((τ ^^ (n + (1 :: nat))) UNIV))" using assms a
by (rule monoE)
thus "(τ ^^ (Suc n + (1))) UNIV ⊆ (τ ^^ Suc n) UNIV" by simp
qed
qed

lemma Suc_less_le: "x < (y - n) ⟹ x ≤ (y - (Suc n))"
by simp

lemma card_univ_subtract:
assumes "finite (UNIV :: 'a set)" and  "mono τ"
and  "(∀i :: nat. ((τ :: 'a set ⇒ 'a set) ^^ (i + (1 :: nat)))(UNIV :: 'a set) ⊂ (τ ^^ i) UNIV)"
shows "(∀ i :: nat. card((τ ^^ i) (UNIV ::'a set)) ≤ (card (UNIV :: 'a set)) - i)"
proof (rule allI, induct_tac i)
show "card ((τ ^^ (0)) UNIV) ≤ card (UNIV :: 'a set) - (0)" using assms
by (simp)
next show "⋀(i) n.
card ((τ ^^ n) (UNIV :: 'a set)) ≤ card (UNIV :: 'a set) - n ⟹
card ((τ ^^ Suc n) (UNIV :: 'a set)) ≤ card (UNIV :: 'a set) - Suc n" using assms
proof -
fix i n
assume a: "card ((τ ^^ n) (UNIV :: 'a set)) ≤ card (UNIV :: 'a set) - n"
have b: "(τ ^^ (n + (1)))(UNIV :: 'a set) ⊂ (τ ^^ n) UNIV" using assms
by (erule_tac x = n in spec)
have "card((τ ^^ (n + (1 :: nat)))(UNIV :: 'a set)) < card((τ ^^ n) (UNIV :: 'a set))"
by (rule psubset_card_mono, rule finite_subset, rule subset_UNIV, rule assms(1), rule b)
thus "card ((τ ^^ Suc n) (UNIV :: 'a set)) ≤ card (UNIV :: 'a set) - Suc n" using a
by simp
qed
qed

lemma card_UNIV_tau_i_below_zero:
assumes "finite (UNIV :: 'a set)" and "mono τ"
and  "(∀i :: nat. ((τ :: ('a set ⇒ 'a set)) ^^ (i + (1 :: nat)))(UNIV :: 'a set) ⊂ (τ ^^ i) UNIV)"
shows "card((τ ^^ (card (UNIV ::'a set))) (UNIV ::'a set)) ≤ 0"
proof -
have "(∀ i :: nat. card((τ ^^ i) (UNIV ::'a set)) ≤ (card (UNIV :: 'a set)) - i)" using assms
by (rule card_univ_subtract)
thus "card((τ ^^ (card (UNIV ::'a set))) (UNIV ::'a set)) ≤ 0"
by (drule_tac x = "card (UNIV ::'a set)" in spec, simp)
qed

lemma finite_card_zero_empty: "⟦ finite S; card S ≤ 0⟧ ⟹ S = {}"
by simp

lemma UNIV_tau_i_is_empty:
assumes "finite (UNIV :: 'a set)" and "mono (τ :: ('a set ⇒ 'a set))"
and   "(∀i :: nat. ((τ :: 'a set ⇒ 'a set) ^^ (i + (1 :: nat)))(UNIV :: 'a set) ⊂ (τ ^^ i) UNIV)"
shows "(τ ^^ (card (UNIV ::'a set))) (UNIV ::'a set) = {}"
by (meson assms card_UNIV_tau_i_below_zero finite_card_zero_empty finite_subset subset_UNIV)

lemma down_chain_reaches_empty:
assumes "finite (UNIV :: 'a set)" and "mono (τ :: 'a set ⇒ 'a set)"
and "(∀i :: nat. ((τ :: 'a set ⇒ 'a set) ^^ (i + (1 :: nat))) UNIV ⊂ (τ ^^ i) UNIV)"
shows "∃ (j :: nat). (τ ^^ j) UNIV = {}"
using UNIV_tau_i_is_empty assms by blast

lemma no_infinite_subset_chain2:
assumes "finite (UNIV :: 'a set)" and "mono (τ :: ('a set ⇒ 'a set))"
and "∀i :: nat. (τ ^^ i) UNIV ⊃ (τ ^^ (i + (1 :: nat))) UNIV"
shows "False"
proof -
have "∃ j :: nat. (τ ^^ j) UNIV = {}" using assms
by (rule down_chain_reaches_empty)
from this obtain j where a: "(τ ^^ j) UNIV = {}" by (erule exE)
have "(τ ^^ (j + (1))) UNIV ⊂ (τ ^^ j) UNIV" using assms
by (erule_tac x = j in spec)
thus False using a by simp
qed

lemma finite_fixp2:
assumes "finite(UNIV :: 'a set)" and "mono (τ :: ('a set ⇒ 'a set))"
shows "∃ i. (τ ^^ i) UNIV = (τ ^^(i + 1)) UNIV"
proof -
have "∀i. (τ ^^ (i + (1))) UNIV ⊆ (τ ^^ i) UNIV"
by (rule predtrans_UNIV , simp add: assms(2))
moreover have "∃i. ¬ (τ ^^ (i + (1))) UNIV ⊂ (τ ^^ i) UNIV" using assms
proof -
have "¬ (∀ i :: nat. (τ ^^ i) UNIV ⊃ (τ ^^(i + 1)) UNIV)"
using assms(1) assms(2) no_infinite_subset_chain2 by blast
thus "∃i. ¬ (τ ^^ (i + (1))) UNIV ⊂ (τ ^^ i) UNIV" by blast
qed
ultimately show "∃ i. (τ ^^ i) UNIV = (τ ^^(i + 1)) UNIV"
by blast
qed

lemma lfp_loop:
assumes "finite (UNIV :: 'b set)" and "mono (τ :: ('b set ⇒ 'b set))"
shows "∃ n . lfp τ  = (τ ^^ n) {}"
proof -
have "∃i. (τ ^^ i) {} = (τ ^^ (i + (1))) {}"  using assms
by (rule finite_fixp)
from this obtain i where " (τ ^^ i) {} = (τ ^^ (i + (1))) {}"
by (erule exE)
hence "(τ ^^ i) {} = (τ ^^ Suc i) {}"
by simp
hence "(τ ^^ Suc i) {} = (τ ^^ i) {}"
by (rule sym)
hence "lfp τ = (τ ^^ i) {}"
thus "∃ n . lfp τ  = (τ ^^ n) {}"
by (rule exI)
qed

text ‹These next two are repeated from the corresponding
theorems in HOL/ZF/Nat.thy for the sake of self-containedness of the exposition.›
lemma Kleene_iter_gpfp:
assumes "mono f" and "p ≤ f p" shows "p ≤ (f^^k) (top::'a::order_top)"
proof(induction k)
case 0 show ?case by simp
next
case Suc
from monoD[OF assms(1) Suc] assms(2)
show ?case by simp
qed

lemma gfp_loop:
assumes "finite (UNIV :: 'b set)"
and "mono (τ :: ('b set ⇒ 'b set))"
shows "∃ n . gfp τ  = (τ ^^ n)UNIV"
proof -
have " ∃i. (τ ^^ i)(UNIV :: 'b set) = (τ ^^ (i + (1))) UNIV" using assms
by (rule finite_fixp2)
from this obtain i where "(τ ^^ i)UNIV = (τ ^^ (i + (1))) UNIV" by (erule exE)
thus "∃ n . gfp τ  = (τ ^^ n)UNIV" using assms
by (metis Suc_eq_plus1 gfp_Kleene_iter)
qed

subsection ‹Generic type of state with state transition and CTL operators›
text ‹The system states and their transition relation are defined as a class called
@{text ‹state›} containing an abstract constant@{text ‹state_transition›}. It introduces the
syntactic infix notation @{text ‹I →⇩i I'›} to denote that system state @{text ‹I›} and @{text ‹I’›}
are in this relation over an arbitrary (polymorphic) type @{text ‹'a›}.›
class state =
fixes state_transition :: "['a :: type, 'a] ⇒ bool"  (infixr "→⇩i" 50)

text ‹The above class definition lifts Kripke structures and CTL to a general level.
The definition of the inductive relation is given by a set of specific rules which are,
however, part of an application like infrastructures. Branching time temporal logic CTL
is defined in general over Kripke structures with arbitrary state transitions and can later
be applied to suitable theories, like infrastructures.
Based on the generic state transition @{text ‹→›} of the type class state, the CTL-operators
EX and AX express that property f holds in some or all next states, respectively.›

definition AX where "AX f ≡ {s. {f0. s →⇩i f0} ⊆ f}"
definition EX' where "EX' f ≡ {s . ∃ f0 ∈ f. s →⇩i f0 }"

text ‹The CTL formula @{text ‹AG f›} means that on all paths branching from a state @{text ‹s›}
the formula @{text ‹f›} is always true (@{text ‹G›} stands for ‘globally’). It can be defined
using the Tarski fixpoint theory by applying the greatest fixpoint operator. In a similar way,
the other CTL operators are defined.›
definition AF where "AF f ≡ lfp (λ Z. f ∪ AX Z)"
definition EF where "EF f ≡ lfp (λ Z. f ∪ EX' Z)"
definition AG where "AG f ≡ gfp (λ Z. f ∩ AX Z)"
definition EG where "EG f ≡ gfp (λ Z. f ∩ EX' Z)"
definition AU where "AU f1 f2 ≡ lfp(λ Z. f2 ∪ (f1 ∩ AX Z))"
definition EU where "EU f1 f2 ≡ lfp(λ Z. f2 ∪ (f1 ∩ EX' Z))"
definition AR where "AR f1 f2 ≡ gfp(λ Z. f2 ∩ (f1 ∪ AX Z))"
definition ER where "ER f1 f2 ≡ gfp(λ Z. f2 ∩ (f1 ∪ EX' Z))"

subsection  ‹Kripke structures and Modelchecking›
datatype 'a kripke =
Kripke "'a set" "'a set"

primrec states where "states (Kripke S I) = S"
primrec init where "init (Kripke S I) = I"

text ‹The formal Isabelle definition of what it means that formula f holds
in a Kripke structure M can be stated as: the initial states of the Kripke
structure init M need to be contained in the set of all states states M that
imply f.›
definition check ("_ ⊢ _" 50)
where "M ⊢ f ≡ (init M) ⊆ {s ∈ (states M). s ∈ f }"

definition state_transition_refl (infixr "→⇩i*" 50)
where "s →⇩i* s' ≡ ((s,s') ∈ {(x,y). state_transition x y}⇧*)"

subsection ‹Lemmas for CTL operators›

subsubsection ‹EF lemmas›
lemma EF_lem0: "(x ∈ EF f) = (x ∈ f ∪ EX' (lfp (λZ :: ('a :: state) set. f ∪ EX' Z)))"
proof -
have "lfp (λZ :: ('a :: state) set. f ∪ EX' Z) =
f ∪ (EX' (lfp (λZ :: 'a set. f ∪ EX' Z)))"
by (rule def_lfp_unfold, rule reflexive, unfold mono_def EX'_def, auto)
thus "(x ∈ EF (f :: ('a :: state) set)) = (x ∈ f ∪ EX' (lfp (λZ :: ('a :: state) set. f ∪ EX' Z)))"
qed

lemma EF_lem00: "(EF f) = (f ∪ EX' (lfp (λ Z :: ('a :: state) set. f ∪ EX' Z)))"
by (auto simp: EF_lem0)

lemma EF_lem000: "(EF f) = (f ∪ EX' (EF f))"
by (metis EF_def EF_lem00)

lemma EF_lem1: "x ∈ f ∨ x ∈ (EX' (EF f)) ⟹ x ∈ EF f"
assume a: "x ∈ f ∨ x ∈ EX' (lfp (λZ::'a set. f ∪ EX' Z))"
show "x ∈ lfp (λZ::'a set. f ∪ EX' Z)"
proof -
have b: "lfp (λZ :: ('a :: state) set. f ∪ EX' Z) =
f ∪ (EX' (lfp (λZ :: ('a :: state) set. f ∪ EX' Z)))"
using EF_def EF_lem00 by blast
thus "x ∈ lfp (λZ::'a set. f ∪ EX' Z)" using a
by (subst b, blast)
qed
qed

lemma EF_lem2b:
assumes "x ∈ (EX' (EF f))"
shows "x ∈ EF f"

lemma EF_lem2a: assumes "x ∈ f" shows "x ∈ EF f"

lemma EF_lem2c: assumes "x ∉ f" shows "x ∈ EF (- f)"

lemma EF_lem2d: assumes "x ∉ EF f" shows "x ∉ f"
using EF_lem1 assms by auto

lemma EF_lem3b: assumes "x ∈ EX' (f ∪ EX' (EF f))" shows "x ∈ (EF f)"
by (metis EF_lem000 EF_lem2b assms)

lemma EX_lem0l: "x ∈ (EX' f) ⟹ x ∈ (EX' (f ∪ g))"
by (auto simp: EX'_def)

lemma EX_lem0r: "x ∈ (EX' g) ⟹ x ∈ (EX' (f ∪ g))"
by (auto simp: EX'_def)

lemma EX_step: assumes "x  →⇩i y" and "y ∈ f" shows "x ∈ EX' f"
using assms by (auto simp: EX'_def)

lemma EF_E[rule_format]: "∀ f. x ∈ (EF f) ⟶ x ∈ (f ∪ EX' (EF f))"
using EF_lem000 by blast

lemma EF_step: assumes "x  →⇩i y" and "y ∈ f" shows "x ∈ EF f"
using EF_lem3b EX_step assms by blast

lemma EF_step_step: assumes "x  →⇩i y" and "y ∈ EF f" shows  "x ∈ EF f"
using EF_lem2b EX_step assms by blast

lemma EF_step_star: "⟦ x  →⇩i* y; y ∈ f ⟧ ⟹ x ∈ EF f"
show "(x, y) ∈ {(x::'a, y::'a). x →⇩i y}⇧* ⟹ y ∈ f ⟹ x ∈ EF f"
proof (erule converse_rtrancl_induct)
show "y ∈ f ⟹ y ∈ EF f"
by (erule EF_lem2a)
next show "⋀ya z::'a. y ∈ f ⟹
(ya, z) ∈ {(x,y). x →⇩i y} ⟹
(z, y) ∈ {(x,y). x →⇩i y}⇧* ⟹ z ∈ EF f ⟹ ya ∈ EF f"
qed
qed

lemma EF_induct: "(a::'a::state) ∈ EF f ⟹
mono (λ Z. f ∪ EX' Z) ⟹
(⋀x. x ∈ ((λ Z. f ∪ EX' Z)(EF f ∩ {x::'a::state. P x})) ⟹ P x) ⟹
P a"
by (metis (mono_tags, lifting) EF_def def_lfp_induct_set)

lemma valEF_E: "M ⊢ EF f ⟹ x ∈ init M ⟹ x ∈ EF f"
by (auto simp: check_def)

lemma EF_step_star_rev[rule_format]: "x ∈ EF s ⟹  (∃ y ∈ s.  x  →⇩i* y)"
proof (erule EF_induct)
show "mono (λZ::'a set. s ∪ EX' Z)"
by (force simp add: mono_def EX'_def)
next show "⋀x::'a. x ∈ s ∪ EX' (EF s ∩ {x::'a. ∃y::'a∈s. x →⇩i* y}) ⟹ ∃y::'a∈s. x →⇩i* y"
apply (erule UnE)
using state_transition_refl_def apply auto[1]
by (auto simp add: EX'_def state_transition_refl_def intro: converse_rtrancl_into_rtrancl)
qed

lemma EF_step_inv: "(I ⊆ {sa::'s :: state. (∃i∈I. i →⇩i* sa) ∧ sa ∈ EF s})
⟹ ∀ x ∈ I. ∃ y ∈ s. x →⇩i* y"
using EF_step_star_rev by fastforce

subsubsection ‹AG lemmas›

lemma AG_in_lem:   "x ∈ AG s ⟹ x ∈ s"
by (auto simp add: AG_def gfp_def)

lemma AG_lem1: "x ∈ s ∧ x ∈ (AX (AG s)) ⟹ x ∈ AG s"
have "gfp (λZ::'a set. s ∩ AX Z) = s ∩ (AX (gfp (λZ::'a set. s ∩ AX Z)))"
by (rule def_gfp_unfold) (auto simp: mono_def AX_def)
then show "x ∈ s ∧ x ∈ AX (gfp (λZ::'a set. s ∩ AX Z)) ⟹ x ∈ gfp (λZ::'a set. s ∩ AX Z)"
by blast
qed

lemma AG_lem2: "x ∈ AG s ⟹ x ∈ (s ∩ (AX (AG s)))"
proof -
have a: "AG s = s ∩ (AX (AG s))"
unfolding AG_def
by (rule def_gfp_unfold) (auto simp: mono_def AX_def)
thus "x ∈ AG s ⟹ x ∈ (s ∩ (AX (AG s)))"
by (erule subst)
qed

lemma AG_lem3: "AG s = (s ∩ (AX (AG s)))"
using AG_lem1 AG_lem2 by blast

lemma AG_step: "y →⇩i z ⟹ y ∈ AG s ⟹ z ∈ AG s"
using AG_lem2 AX_def by blast

lemma AG_all_s: " x →⇩i* y ⟹ x ∈ AG s ⟹ y ∈ AG s"
show "(x, y) ∈ {(x,y). x →⇩i y}⇧* ⟹ x ∈ AG s ⟹ y ∈ AG s"
by (erule rtrancl_induct) (auto simp add: AG_step)
qed

lemma AG_imp_notnotEF:
"I ≠ {} ⟹ ((Kripke {s. ∃ i ∈ I. (i →⇩i* s)} I  ⊢ AG s)) ⟹
(¬(Kripke {s. ∃ i ∈ I. (i →⇩i* s)} (I :: ('s :: state)set)  ⊢ EF (- s)))"
proof (rule notI, simp add: check_def)
assume a0: "I ≠ {}" and
a1: "I ⊆ {sa::'s. (∃i∈I. i →⇩i* sa) ∧ sa ∈ AG s}" and
a2: "I ⊆ {sa::'s. (∃i∈I. i →⇩i* sa) ∧ sa ∈ EF (- s)}"
show "False"
proof -
have a3: "{sa::'s. (∃i∈I. i →⇩i* sa) ∧ sa ∈ AG s} ∩
{sa::'s. (∃i∈I. i →⇩i* sa) ∧ sa ∈ EF (- s)} = {}"
proof -
have "(? x. x ∈ {sa::'s. (∃i∈I. i →⇩i* sa) ∧ sa ∈ AG s} ∧
x ∈ {sa::'s. (∃i∈I. i →⇩i* sa) ∧ sa ∈ EF (- s)}) ⟹ False"
proof -
assume a4: "(? x. x ∈ {sa::'s. (∃i∈I. i →⇩i* sa) ∧ sa ∈ AG s} ∧
x ∈ {sa::'s. (∃i∈I. i →⇩i* sa) ∧ sa ∈ EF (- s)})"
from a4 obtain x where  a5: "x ∈ {sa::'s. (∃i∈I. i →⇩i* sa) ∧ sa ∈ AG s} ∧
x ∈ {sa::'s. (∃i∈I. i →⇩i* sa) ∧ sa ∈ EF (- s)}"
by (erule exE)
thus "False"
by (metis (mono_tags, lifting) AG_all_s AG_in_lem ComplD EF_step_star_rev a5 mem_Collect_eq)
qed
thus "{sa::'s. (∃i∈I. i →⇩i* sa) ∧ sa ∈ AG s} ∩
{sa::'s. (∃i∈I. i →⇩i* sa) ∧ sa ∈ EF (- s)} = {}"
by blast
qed
moreover have b: "? x. x : I" using a0
by blast
moreover obtain x where "x ∈ I"
using b by blast
ultimately show "False" using a0 a1 a2
by blast
qed
qed

text ‹A simplified way of Modelchecking is given by the following lemma.›
lemma check2_def: "(Kripke S I ⊢ f) = (I ⊆ S ∩ f)"

end

# 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''"

lemma att_and_empty2: " ⊢([] ⊕⇩∧⇗(s, s)⇖)"

lemma att_or_empty[rule_format] : " ⊢([] ⊕⇩∨⇗(s', s'')⇖) ⟶ s' ⊆ s''"

lemma att_or_empty_back[rule_format]: " s' ⊆ s'' ⟶  ⊢([] ⊕⇩∨⇗(s', s'')⇖)"

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)⇖)"

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
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))"

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"

lemma nth_app_eq1_rev:   "i < length sla ⟹  sla ! i = (sla @ sl) ! i"

lemma nth_app_eq2[rule_format]: "∀ sl i. length sla ≤ i ∧ i < length (sla @ sl)
⟶ (sla @ sl) ! i = sl ! (i - (length sla))"

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)⇙"

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)⇙"
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"
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"

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
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"
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)]",
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)]"
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"
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

end

# Theory 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 ‹Actors can delete data.›
definition actor_can_delete ::   "[infrastructure, actor, location] ⇒ bool"
where actor_can_delete_def: "actor_can_delete I h l ≡
(∀ as n. ((h, as), n) ∉ (snd (lgra (graphI I) l)))"
*)
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"

(* This part is relevant to model Insiders but is not needed for Infrastructures.

datatype psy_states = happy | depressed | disgruntled | angry | stressed
datatype motivations = financial | political | revenge | curious | competitive_advantage | power | peer_recognition

datatype actor_state = Actor_state "psy_states" "motivations set"
primrec motivation :: "actor_state ⇒ motivations set"
where "motivation  (Actor_state p m) =  m"
primrec psy_state :: "actor_state ⇒ psy_states"
where "psy_state  (Actor_state p m) = p"

definition tipping_point :: "actor_state ⇒ bool" where
"tipping_point a ≡ ((motivation a ≠ {}) ∧ (happy ≠ psy_state a))"

consts astate :: "identity ⇒ actor_state"

(* Two versions of an impersonation predicate "a can act as b".
The first one is stronger and allows substitution of the insider in any context;
the second one is parameterized over a context predicate to describe this.   *)
definition UasI ::  "[identity, identity] ⇒ bool "
where "UasI a b ≡ (Actor a = Actor b) ∧ (∀ x y. x ≠ a ∧ y ≠ a ∧ Actor x = Actor y ⟶ x = y)"

definition UasI' ::  "[actor => bool, identity, identity] ⇒ bool "
where "UasI' P a b ≡ P (Actor b) ⟶ P (Actor a)"

definition Insider :: "[identity, identity set] ⇒ bool"
where "Insider a C ≡ (tipping_point (astate a) ⟶ (∀ b∈C. UasI a b))"

definition Insider' :: "[actor ⇒ bool, identity, identity set] ⇒ bool"
where "Insider' P a C ≡ (tipping_point (astate a) ⟶ (∀ b∈C. UasI' P a b ∧ inj_on Actor C))"
*)

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)"
(*
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 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 {}))"
(* The nicer representation with case suffers from
not so nice presentation in the cases (need to unfold the syntax)
fixes ex_loc_ass_alt :: "location ⇒ identity set"
defines ex_loc_ass_alt_def: "ex_loc_ass_alt ≡
(λ x.  (case x of
Location (Suc 0) ⇒ {''Patient''}
| Location (Suc (Suc 0)) ⇒ {''Doctor'', ''Eve''}
|  _ ⇒ {}))"
*)
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"
(* Same as above: the nicer representation with case suffers from
not so nice presentation in the cases (need to unfold the syntax)
fixes local_policies_alt :: "[igraph, location] ⇒ policy set"
defines local_policies_alt_def: "local_policies_alt G ≡
(λ x. case x of
Location (Suc 0) ⇒ {(λ y. True, {put,get,move,eval})}
| Location 0 ⇒ {((λ y. has G (y, ''PIN'')), {put,get,move,eval})}
| Location (Suc (Suc (Suc 0))) ⇒ {(λ y. True, {put,get,move,eval})}
| Location (Suc (Suc 0)) ⇒
{((λ y. (∃ n. (n  @⇘G⇙ hospital) ∧ Actor n = y ∧
has G (y, ''skey''))), {put,get,move,eval})}
| _ ⇒  {})"
*)
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 {}))))"
(* problems with case in locales?
defines local_policies_def: "local_policies G x ≡
(case x of
home ⇒ {(λ y. True, {put,get,move,eval})}
| sphone ⇒ {((λ y. has G (y, ''PIN'')), {put,get,move,eval})}
| cloud ⇒ {(λ y. True, {put,get,move,eval})}
| hospital ⇒ {((λ y. (∃ n. (n  @⇘G⇙ hospital) ∧ Actor n = y ∧
has G (y, ''skey''))), {put,get,move,eval})}
| _ ⇒  {})"
*)
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}"
(* other states of scenario *)
(* First step: Patient goes onto cloud *)
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'}"
(* Second step: Eve goes onto cloud from where she'll be able to get the data *)
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)
qed

lemma step1r: "gdpr_scenario  →⇩n* gdpr_scenario'"
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)
by blast
qed

lemma step2r: "gdpr_scenario'  →⇩n* gdpr_scenario''"
show "(gdpr_scenario', gdpr_scenario'') ∈ {(x::infrastructure, y::infrastructure). x →⇩n y}⇧*"
by (insert step2, auto)
qed

(* Attack example: Eve can get onto cloud and get Patient's data
because the policy allows Eve to get on cloud.
This attack can easily be fixed by disabling Eve to "get"
in the policy (just change the "True" for cloud to a set with no
Eve in it).
However, it would not prevent Insider attacks (where Eve is
impersonating the Doctor, for example). Insider attacks can
be checked using the UasI predicate.
*)
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)

(* However, when integrating DLM into the model and hence labeling
information becomes part of the conditions of the get_data rule this isn't
possible any more: gdpr_EF is not true any more *)
(** GDPR properties  for the illustration of the DLM labeling **)
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.›
(* GDPR three: Processing preserves ownership in any location *)
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 (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`