Theory BD_Security_TS

subsection ‹Instantiation for transition systems›

(*<*)
theory BD_Security_TS
imports Abstract_BD_Security Filtermap Transition_System
begin
(*>*)

declare Let_def[simp]

unbundle no relcomp_syntax


locale BD_Security_TS = Transition_System istate validTrans srcOf tgtOf
 for istate :: 'state and validTrans :: "'trans ⇒ bool"
     and srcOf :: "'trans ⇒ 'state" and tgtOf :: "'trans ⇒ 'state"
+
fixes (* value filtering and production:  *)
   φ :: "'trans => bool" and f :: "'trans ⇒ 'value"
 and (* observation filtering and production: *)
   γ :: "'trans => bool" and g :: "'trans ⇒ 'obs"
 and (* declassification trigger:  *)
   T :: "'trans ⇒ bool"
 and (* declassification bound: *)
   B :: "'value list ⇒ 'value list ⇒ bool"
begin

(* The value function: *)
definition V :: "'trans list ⇒ 'value list" where "V ≡ filtermap φ f"
(* The observation function: *)
definition O :: "'trans trace ⇒ 'obs list" where "O ≡ filtermap γ g"

sublocale Abstract_BD_Security
  where validSystemTrace = "validFrom istate" and V = V and O = O and B = B and TT = "never T" .

lemma O_map_filter: "O tr = map g (filter γ tr)" unfolding O_def filtermap_map_filter ..
lemma V_map_filter: "V tr = map f (filter φ tr)" unfolding V_def filtermap_map_filter ..

lemma V_simps[simp]:
"V [] = []"  "¬ φ trn ⟹ V (trn # tr) = V tr"  "φ trn ⟹ V (trn # tr) = f trn # V tr"
unfolding V_def by auto

lemma V_Cons_unfold: "V (trn # tr) = (if φ trn then f trn # V tr else V tr)"
by auto

lemma O_simps[simp]:
"O [] = []"  "¬ γ trn ⟹ O (trn # tr) = O tr"  "γ trn ⟹ O (trn # tr) = g trn # O tr"
unfolding O_def by auto

lemma O_Cons_unfold: "O (trn # tr) = (if γ trn then g trn # O tr else O tr)"
by auto

lemma V_append: "V (tr @ tr1) = V tr @ V tr1"
unfolding V_def using filtermap_append by auto

lemma V_snoc:
"¬ φ trn ⟹ V (tr ## trn) = V tr"  "φ trn ⟹ V (tr ## trn) = V tr ## f trn"
unfolding V_def by auto

lemma O_snoc:
"¬ γ trn ⟹ O (tr ## trn) = O tr"  "γ trn ⟹ O (tr ## trn) = O tr ## g trn"
unfolding O_def by auto

lemma V_Nil_list_ex: "V tr = [] ⟷ ¬ list_ex φ tr"
unfolding V_def using filtermap_Nil_list_ex by auto

lemma V_Nil_never: "V tr = [] ⟷ never φ tr"
unfolding V_def using filtermap_Nil_never by auto

lemma Nil_V_never: "[] = V tr ⟷ never φ tr"
unfolding V_def filtermap_map_filter by (induction tr) auto

lemma list_ex_iff_length_V:
"list_ex φ tr ⟷ length (V tr) > 0"
by (metis V_Nil_list_ex length_greater_0_conv)

lemma length_V: "length (V tr) ≤ length tr"
by (auto simp: V_def length_filtermap)

lemma V_list_all: "V tr = map f tr ⟷ list_all φ tr"
by (auto simp: V_def length_filtermap)

lemma V_eq_Cons:
assumes "V tr = v # vl1"
shows "∃ trn tr2 tr1. tr = tr2 @ [trn] @ tr1 ∧ never φ tr2 ∧ φ trn ∧ f trn = v ∧ V tr1 = vl1"
using assms filtermap_eq_Cons unfolding V_def by auto

lemma V_eq_append:
assumes "V tr = vl1 @ vl2"
shows "∃ tr1 tr2. tr = tr1 @ tr2 ∧ V tr1 = vl1 ∧ V tr2 = vl2"
using assms filtermap_eq_append[of φ f] unfolding V_def by auto

lemma V_eq_RCons:
assumes "V tr = vl1 ## v"
shows "∃ trn tr1 tr2. tr = tr1 @ [trn] @ tr2 ∧ φ trn ∧ f trn = v ∧ V tr1 = vl1 ∧ never φ tr2"
using assms filtermap_eq_RCons[of φ f] unfolding V_def by blast

lemma V_eq_Cons_RCons:
assumes "V tr = v # vl1 ## w"
shows "∃ trv trnv tr1 trnw trw.
   tr = trv @ [trnv] @ tr1 @ [trnw] @ trw ∧
   never φ trv ∧ φ trnv ∧ f trnv = v ∧ V tr1 = vl1 ∧ φ trnw ∧ f trnw = w ∧ never φ trw"
using assms filtermap_eq_Cons_RCons[of φ f] unfolding V_def by blast

lemma O_append: "O (tr @ tr1) = O tr @ O tr1"
unfolding O_def using filtermap_append by auto

lemma O_Nil_list_ex: "O tr = [] ⟷ ¬ list_ex γ tr"
unfolding O_def using filtermap_Nil_list_ex by auto

lemma O_Nil_never: "O tr = [] ⟷ never γ tr"
unfolding O_def using filtermap_Nil_never by auto

lemma Nil_O_never: "[] = O tr ⟷ never γ tr"
unfolding O_def filtermap_map_filter by (induction tr) auto

lemma length_O: "length (O tr) ≤ length tr"
by (auto simp: O_def length_filtermap)

lemma O_list_all: "O tr = map g tr ⟷ list_all γ tr"
by (auto simp: O_def length_filtermap)

lemma O_eq_Cons:
assumes "O tr = obs # obsl1"
shows "∃ trn tr2 tr1. tr = tr2 @ [trn] @ tr1 ∧ never γ tr2 ∧ γ trn ∧ g trn = obs ∧ O tr1 = obsl1"
using assms filtermap_eq_Cons unfolding O_def by auto

lemma O_eq_append:
assumes "O tr = obsl1 @ obsl2"
shows "∃ tr1 tr2. tr = tr1 @ tr2 ∧ O tr1 = obsl1 ∧ O tr2 = obsl2"
using assms filtermap_eq_append[of γ g] unfolding O_def by auto

lemma O_eq_RCons:
assumes "O tr = oul1 ## ou"
shows "∃ trn tr1 tr2. tr = tr1 @ [trn] @ tr2 ∧ γ trn ∧ g trn = ou ∧ O tr1 = oul1 ∧ never γ tr2"
using assms filtermap_eq_RCons[of γ g] unfolding O_def by blast

lemma O_eq_Cons_RCons:
assumes "O tr0 = ou # oul1 ## ouu"
shows "∃ tr trn tr1 trnn trr.
   tr0 = tr @ [trn] @ tr1 @ [trnn] @ trr ∧
   never γ tr ∧ γ trn ∧ g trn = ou ∧ O tr1 = oul1 ∧ γ trnn ∧ g trnn = ouu ∧ never γ trr"
using assms filtermap_eq_Cons_RCons[of γ g] unfolding O_def by blast

lemma O_eq_Cons_RCons_append:
assumes "O tr0 = ou # oul1 ## ouu @ oull"
shows "∃ tr trn tr1 trnn trr.
   tr0 = tr @ [trn] @ tr1 @ [trnn] @ trr ∧
   never γ tr ∧ γ trn ∧ g trn = ou ∧ O tr1 = oul1 ∧ γ trnn ∧ g trnn = ouu ∧ O trr = oull"
proof-
  from O_eq_append[of tr0 "ou # oul1 ## ouu" oull] assms
  obtain tr00 trrr where 1: "tr0 = tr00 @ trrr"
  and 2: "O tr00 = ou # oul1 ## ouu" and 3: "O trrr = oull" by auto
  from O_eq_Cons_RCons[OF 2] obtain tr trn tr1 trnn trr where
  4:"tr00 = tr @ [trn] @ tr1 @ [trnn] @ trr ∧
     never γ tr ∧
     γ trn ∧ g trn = ou ∧ O tr1 = oul1 ∧ γ trnn ∧ g trnn = ouu ∧ never γ trr" by auto
  show ?thesis apply(rule exI[of _ tr], rule exI[of _ trn], rule exI[of _ tr1],
     rule exI[of _ trnn], rule exI[of _ "trr @ trrr"])
  using 1 3 4 by (simp add: O_append O_Nil_never)
qed

lemma O_Nil_tr_Nil: "O tr ≠ [] ⟹ tr ≠ []"
by (induction tr) auto

lemma V_Cons_eq_append: "V (trn # tr) = V [trn] @ V tr"
by (cases "φ trn") auto

lemma set_V: "set (V tr) ⊆ {f trn | trn . trn ∈∈ tr ∧ φ trn}"
using set_filtermap unfolding V_def .

lemma set_O: "set (O tr) ⊆ {g trn | trn . trn ∈∈ tr ∧ γ trn}"
using set_filtermap unfolding O_def .

lemma list_ex_length_O:
assumes "list_ex γ tr"  shows "length (O tr) > 0"
by (metis assms O_Nil_list_ex length_greater_0_conv)

lemma list_ex_iff_length_O:
"list_ex γ tr ⟷ length (O tr) > 0"
by (metis O_Nil_list_ex length_greater_0_conv)

lemma length1_O_list_ex_iff:
"length (O tr) > 1 ⟹ list_ex γ tr"
unfolding list_ex_iff_length_O by auto

lemma list_all_O_map: "list_all γ tr ⟹ O tr = map g tr"
using O_list_all by auto

lemma never_O_Nil: "never γ tr ⟹ O tr = []"
using O_Nil_never by auto

lemma list_all_V_map: "list_all φ tr ⟹ V tr = map f tr"
using V_list_all by auto

lemma never_V_Nil: "never φ tr ⟹ V tr = []"
using V_Nil_never by auto

(* Reachable states by transitions satisfying T: *)
inductive reachNT:: "'state ⇒ bool" where
Istate: "reachNT istate"
|
Step:
"⟦reachNT (srcOf trn); validTrans trn; ¬ T trn⟧
 ⟹ reachNT (tgtOf trn)"

lemma reachNT_reach: assumes "reachNT s"  shows "reach s"
using assms apply induct by (auto intro: reach.intros)

lemma V_iff_non_φ[simp]: "V (trn # tr) = V tr ⟷ ¬ φ trn"
by (cases "φ trn") auto

lemma V_imp_φ: "V (trn # tr) = v # V tr ⟹ φ trn"
by (cases "φ trn") auto

lemma V_imp_Nil: "V (trn # tr) = [] ⟹ V tr = []"
by (cases "φ trn") auto

lemma V_iff_Nil[simp]: "V (trn # tr) = [] ⟷ ¬ φ trn ∧ V tr = []"
by (metis V_iff_non_φ V_imp_Nil)

end (* locale BD_Security_TS *)

(*<*)
end
(*>*)