Session Attack_Trees

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 
    contradiction point that
    @{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).

If we can additionally show 

@{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) {}"
     by (simp add: assms(2) lfp_Kleene_iter)
   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)))"
    by (simp add: EF_def) 
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"
proof (simp add: EF_def)
  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"
  by (simp add: EF_lem1 assms)

lemma EF_lem2a: assumes "x  f" shows "x  EF f"
  by (simp add: EF_lem1 assms)

lemma EF_lem2c: assumes "x  f" shows "x  EF (- f)"
  by (simp add: EF_lem1 assms)

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"
proof (simp add: state_transition_refl_def)
  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"
        by (simp add: EF_step_step)
    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::'as. x i* y})  y::'as. 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. (iI. 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"
proof (simp add: AG_def)
  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"
proof (simp add: state_transition_refl_def)
  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. (iI. i i* sa)  sa  AG s}" and
    a2: "I  {sa::'s. (iI. i i* sa)  sa  EF (- s)}" 
  show "False"
  proof - 
    have a3: "{sa::'s. (iI. i i* sa)  sa  AG s} 
                        {sa::'s. (iI. i i* sa)  sa  EF (- s)} = {}"
      proof -
        have "(? x. x  {sa::'s. (iI. i i* sa)  sa  AG s} 
                           x  {sa::'s. (iI. i i* sa)  sa  EF (- s)})  False"
        proof -
          assume a4: "(? x. x  {sa::'s. (iI. i i* sa)  sa  AG s} 
                           x  {sa::'s. (iI. i i* sa)  sa  EF (- s)})"          
            from a4 obtain x where  a5: "x  {sa::'s. (iI. i i* sa)  sa  AG s} 
                                   x  {sa::'s. (iI. 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. (iI. i i* sa)  sa  AG s} 
                        {sa::'s. (iI. 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)" 
  by (auto simp add: check_def)
    
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  (ass)" |
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: "((Ass)) = 
               (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: "((Ass)) = 
               (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 # x2s)   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 # x2s)   (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 # x2s)   (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 # x2ax)  xa  fst (attack (x1 # x2ax))
                      xa  fst (attack x1)"  
  by (induction x2a, (subst att_and, simp)+)

lemma att_orD1: " (x1 # x2x)   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 # x2x)    (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.  (x2x)  ( 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. ( ((x2x):: ('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 # x2x):: ('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::'afst (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::'afst (attack x1aa). y::'a. y  snd (attack x1aa)  x i* y)) 
       (x::'a set × 'a set.
           ([]x) 
           (xa::'afst (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::'afst (attack x1aa). y::'a. y  snd (attack x1aa)  x i* y))) 
       x1aa::'a attree.
          (x1aa  set x1a) 
          (x1aa)  ((x::'afst (attack x1aa). y::'a. y  snd (attack x1aa)  x i* y)) 
       (x1aa::'a attree.
           (x1aa  set x2a) 
           (x1aa)  (x::'afst (attack x1aa). y::'a. y  snd (attack x1aa)  x i* y)) 
       (x::'a set × 'a set.
           ((x2ax)) 
           ((xa::'afst (attack (x2ax)). y::'a. y  snd (attack (x2ax))  xa i* y))) 
       ((x1aa::'a attree.
           (x1aa  set (x1 # x2a)) 
           (x1aa)  ((x::'afst (attack x1aa). y::'a. y  snd (attack x1aa)  x i* y))) 
       (x::'a set × 'a set.
          ( (x1 # x2ax)) 
           (xa::'afst (attack (x1 # x2ax)).
               (y::'a. y  snd (attack (x1 # x2ax))  (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.
                             (x2ax) 
                             (xa::'afst (attack (x2ax)).
                              y::'a. y  snd (attack (x2ax))  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::'afst (attack x1aa). y::'a. y  snd (attack x1aa)  x i* y) 
       (x1 # x2ax) 
       x::'a set × 'a set.
          (x2ax) 
          (xa::'afst (attack (x2ax)). y::'a. y  snd (attack (x2ax))  xa i* y) 
       xa::'afst (attack (x1 # x2ax)). y::'a. y  snd (attack (x1 # x2ax))  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 (alx))"
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 # x2ax)) = 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 (ass)"
    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::'ax. xa::'axa. x i xa  x::'ax. xa::'axc. 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::'sI. 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::'sI. (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::'sfst (attack A). y::'s. y  snd (attack A)  x i* y"
        by (rule att_elem_seq0, rule assms)
      thus " x::'sI. y::'ss. 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::'ss::('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::'ainsert x F. y::'b. P y x)"
    have "(x::'aF. y::'b. P y x)" 
      using d by blast
    then obtain f where f: "x::'aF. P (f x) x" 
      using insertI.IH by blast 
    from d obtain y where "P y x" by blast
    thus "(f::'a  'b. x::'ainsert 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::'sI.
       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::'sI. 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::'sI. 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. iI. 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)
    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
     
(* 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::infrastructureIgdpr. 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. iIgdpr. 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. lgdpr_locations. owns (Igraph x) l (Actor h) d}"
    apply (simp add: AG_def gfp_def)
    apply (rule_tac x = "{x::infrastructure. lgdpr_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. lgdpr_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. lgdpr_locations. owns (Igraph x) l (Actor h) d}) 
    ¬ (Kripke {s::infrastructure. i::infrastructureIgdpr. i i* s}
        Igdpr  EF (- {x::infrastructure. lgdpr_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