Theory Security

(*
Title: Value-Dependent SIFUM-Type-Systems
Authors: Toby Murray, Robert Sison, Edward Pierzchalski, Christine Rizkallah
(Based on the SIFUM-Type-Systems AFP entry, whose authors
 are: Sylvia Grewe, Heiko Mantel, Daniel Schoepe)
*)

section ‹Definition of the SIFUM-Security Property›

theory Security
imports Preliminaries
begin

type_synonym ('var, 'val) adaptation = "'var ⇀ ('val × 'val)"

definition apply_adaptation ::
  "bool ⇒ ('Var, 'Val) Mem ⇒ ('Var, 'Val) adaptation ⇒ ('Var, 'Val) Mem"
  where "apply_adaptation first mem A =
         (λ x. case (A x) of
               Some (v⇩1, v⇩2) ⇒ if first then v⇩1 else v⇩2
             | None ⇒ mem x)"

abbreviation apply_adaptation⇩1 ::
  "('Var, 'Val) Mem ⇒ ('Var, 'Val) adaptation ⇒ ('Var, 'Val) Mem"
  ("_ [∥⇩1 _]" [900, 0] 1000)
  where "mem [∥⇩1 A] ≡ apply_adaptation True mem A"

abbreviation apply_adaptation⇩2 ::
  "('Var, 'Val) Mem ⇒ ('Var, 'Val) adaptation ⇒ ('Var, 'Val) Mem"
  ("_ [∥⇩2 _]" [900, 0] 1000)
  where "mem [∥⇩2 A] ≡ apply_adaptation False mem A"

definition
  var_asm_not_written :: "'Var Mds ⇒ 'Var ⇒ bool"
where
  "var_asm_not_written mds x ≡ x ∈ mds AsmNoWrite ∨ x ∈ mds AsmNoReadOrWrite"

context sifum_security_init begin

subsection ‹Evaluation of Concurrent Programs›

abbreviation eval_abv :: "('Com, 'Var, 'Val) LocalConf ⇒ (_, _, _) LocalConf ⇒ bool"
  (infixl "↝" 70)
where
  "x ↝ y ≡ (x, y) ∈ eval"

abbreviation conf_abv :: "'Com ⇒ 'Var Mds ⇒ ('Var, 'Val) Mem ⇒ (_,_,_) LocalConf"
  ("⟨_, _, _⟩" [0, 0, 0] 1000)
where
  "⟨ c, mds, mem ⟩ ≡ ((c, mds), mem)"

(* Labelled evaluation global configurations: *)
inductive_set meval :: "((_,_,_) GlobalConf × nat × (_,_,_) GlobalConf) set"
  and meval_abv :: "_ ⇒ _ ⇒ _ ⇒ bool" ("_ ↝⇘_⇙ _" 70)
where
  "conf ↝⇘k⇙ conf' ≡ (conf, k, conf') ∈ meval" |
  meval_intro [iff]: "⟦ (cms ! n, mem) ↝ (cm', mem'); n < length cms ⟧ ⟹
  ((cms, mem), n, (cms [n := cm'], mem')) ∈ meval"

inductive_cases meval_elim [elim!]: "((cms, mem), k, (cms', mem')) ∈ meval"

inductive neval :: "('Com, 'Var, 'Val) LocalConf ⇒ nat ⇒ (_, _, _) LocalConf ⇒ bool"
  (infixl "↝⇗_⇖" 70)
where
  neval_0: "x = y ⟹ x ↝⇗0⇖ y" |
  neval_S_n: "x ↝ y ⟹ y ↝⇗n⇖ z ⟹ x ↝⇗Suc n⇖ z"

inductive_cases neval_ZeroE: "neval x 0 y"
inductive_cases neval_SucE: "neval x (Suc n) y"

lemma neval_det:
  "x ↝⇗n⇖ y ⟹ x ↝⇗n⇖ y' ⟹ y = y'"
  apply(induct arbitrary: y' rule: neval.induct)
   apply(blast elim: neval_ZeroE)
  apply(blast elim: neval_SucE dest: deterministic)
  done

lemma neval_Suc_simp [simp]:
  "neval x (Suc 0) y = x ↝ y"
proof
  assume a: "neval x (Suc 0) y"
  have "⋀n. neval x n y ⟹ n = Suc 0 ⟹ x ↝ y"
  proof -
    fix n
    assume "neval x n y"
       and "n = Suc 0"
    thus "x ↝ y"
    by(induct rule: neval.induct, auto elim: neval_ZeroE)
  qed
  with a show "x ↝ y" by simp
  next
  assume "x ↝ y"
  thus "neval x (Suc 0) y"
    by(force intro: neval.intros)
qed

fun 
  lc_set_var :: "(_, _, _) LocalConf ⇒ 'Var ⇒ 'Val ⇒ (_, _, _) LocalConf"
where
  "lc_set_var (c, mem) x v = (c, mem (x := v))"

fun 
  meval_sched :: "nat list ⇒ ('Com, 'Var, 'Val) GlobalConf ⇒ (_, _, _) GlobalConf ⇒ bool"
where
  "meval_sched [] c c' = (c = c')" |
  "meval_sched (n#ns) c c' = (∃ c''.  c ↝⇘n⇙ c'' ∧ meval_sched ns c'' c')"

abbreviation
  meval_sched_abv :: "(_,_,_) GlobalConf ⇒ nat list ⇒ (_,_,_) GlobalConf ⇒ bool" ("_ →⇘_⇙ _" 70)
where
  "c →⇘ns⇙ c' ≡ meval_sched ns c c'"

lemma meval_sched_det:
  "meval_sched ns c c' ⟹ meval_sched ns c c'' ⟹ c' = c''"
  apply(induct ns arbitrary: c)
   apply(auto dest: deterministic)
  done

subsection ‹Low-equivalence and Strong Low Bisimulations›

(* Low-equality between memory states: *)
definition 
  low_eq :: "('Var, 'Val) Mem ⇒ (_, _) Mem ⇒ bool" (infixl "=⇧l" 80)
where
  "mem⇩1 =⇧l mem⇩2 ≡ (∀ x. dma mem⇩1 x = Low ⟶ mem⇩1 x = mem⇩2 x)"


(* Low-equality modulo a given mode state: *)
definition 
  low_mds_eq :: "'Var Mds ⇒ ('Var, 'Val) Mem ⇒ (_, _) Mem ⇒ bool"
  ("_ =ı⇧l _" [100, 100] 80)
where
  "(mem⇩1 =⇘mds⇙⇧l mem⇩2) ≡ (∀ x. dma mem⇩1 x = Low ∧ (x ∈ 𝒞 ∨ x ∉ mds AsmNoReadOrWrite) ⟶ mem⇩1 x = mem⇩2 x)"

lemma low_eq_low_mds_eq:
  "(mem⇩1 =⇧l mem⇩2) = (mem⇩1 =⇘(λm. {})⇙⇧l mem⇩2)"
  by(simp add: low_eq_def low_mds_eq_def)

lemma low_mds_eq_dma:
  "(mem⇩1 =⇘mds⇙⇧l mem⇩2) ⟹ dma mem⇩1 = dma mem⇩2"
  apply(rule dma_𝒞)
  apply(simp add: low_mds_eq_def 𝒞_Low)
  done

lemma low_mds_eq_sym:
  "(mem⇩1 =⇘mds⇙⇧l mem⇩2) ⟹ (mem⇩2 =⇘mds⇙⇧l mem⇩1)"
  apply(frule low_mds_eq_dma)
  apply(simp add: low_mds_eq_def)
  done

lemma low_eq_sym:
  "(mem⇩1 =⇧l mem⇩2) ⟹ (mem⇩2 =⇧l mem⇩1)"
  apply(simp add: low_eq_low_mds_eq low_mds_eq_sym)
  done

lemma [simp]: "mem =⇧l mem' ⟹ mem =⇘mds⇙⇧l mem'"
  by (simp add: low_mds_eq_def low_eq_def)

lemma [simp]: "(∀ mds. mem =⇘mds⇙⇧l mem') ⟹ mem =⇧l mem'"
  by (auto simp: low_mds_eq_def low_eq_def)

lemma High_not_in_𝒞 [simp]:
  "dma mem⇩1 x = High ⟹ x ∉ 𝒞"
  apply(case_tac "x ∈ 𝒞")
  by(simp add: 𝒞_Low)

(* Closedness under globally consistent changes: *)
definition 
  closed_glob_consistent :: "(('Com, 'Var, 'Val) LocalConf) rel ⇒ bool"
where
  "closed_glob_consistent ℛ =
  (∀ c⇩1 mds mem⇩1 c⇩2 mem⇩2. (⟨ c⇩1, mds, mem⇩1 ⟩, ⟨ c⇩2, mds, mem⇩2 ⟩) ∈ ℛ ⟶
   (∀ A. ((∀x. case A x of Some (v,v') ⇒ (mem⇩1 x ≠ v ∨ mem⇩2 x ≠ v') ⟶ ¬ var_asm_not_written mds x | _ ⇒ True) ∧
          (∀x. dma (mem⇩1 [∥⇩1 A]) x ≠ dma mem⇩1 x ⟶ ¬ var_asm_not_written mds x) ∧
          (∀x. dma (mem⇩1 [∥⇩1 A]) x = Low ∧ (x ∉ mds AsmNoReadOrWrite ∨ x ∈ 𝒞) ⟶ (mem⇩1 [∥⇩1 A]) x = (mem⇩2 [∥⇩2 A]) x)) ⟶
         (⟨ c⇩1, mds, mem⇩1[∥⇩1 A] ⟩, ⟨ c⇩2, mds, mem⇩2[∥⇩2 A] ⟩) ∈ ℛ))"

(* Strong low bisimulations modulo modes: *)
definition 
  strong_low_bisim_mm :: "(('Com, 'Var, 'Val) LocalConf) rel ⇒ bool"
where
  "strong_low_bisim_mm ℛ ≡
  sym ℛ ∧
  closed_glob_consistent ℛ ∧
  (∀ c⇩1 mds mem⇩1 c⇩2 mem⇩2. (⟨ c⇩1, mds, mem⇩1 ⟩, ⟨ c⇩2, mds, mem⇩2 ⟩) ∈ ℛ ⟶
   (mem⇩1 =⇘mds⇙⇧l mem⇩2) ∧
   (∀ c⇩1' mds' mem⇩1'. ⟨ c⇩1, mds, mem⇩1 ⟩ ↝ ⟨ c⇩1', mds', mem⇩1' ⟩ ⟶
    (∃ c⇩2' mem⇩2'. ⟨ c⇩2, mds, mem⇩2 ⟩ ↝ ⟨ c⇩2', mds', mem⇩2' ⟩ ∧
                  (⟨ c⇩1', mds', mem⇩1' ⟩, ⟨ c⇩2', mds', mem⇩2' ⟩) ∈ ℛ)))"

inductive_set mm_equiv :: "(('Com, 'Var, 'Val) LocalConf) rel"
  and mm_equiv_abv :: "('Com, 'Var, 'Val) LocalConf ⇒ 
  ('Com, 'Var, 'Val) LocalConf ⇒ bool" (infix "≈" 60)
where
  "mm_equiv_abv x y ≡ (x, y) ∈ mm_equiv" |
  mm_equiv_intro [iff]: "⟦ strong_low_bisim_mm ℛ ; (lc⇩1, lc⇩2) ∈ ℛ ⟧ ⟹ (lc⇩1, lc⇩2) ∈ mm_equiv"

inductive_cases mm_equiv_elim [elim]: "⟨ c⇩1, mds, mem⇩1 ⟩ ≈ ⟨ c⇩2, mds, mem⇩2 ⟩"

definition low_indistinguishable :: "'Var Mds ⇒ 'Com ⇒ 'Com ⇒ bool"
  ("_ ∼ı _" [100, 100] 80)
where 
  "c⇩1 ∼⇘mds⇙ c⇩2 = (∀ mem⇩1 mem⇩2. mem⇩1 =⇘mds⇙⇧l mem⇩2 ⟶ ⟨ c⇩1, mds, mem⇩1 ⟩ ≈ ⟨ c⇩2, mds, mem⇩2 ⟩)"

subsection ‹SIFUM-Security›

(* SIFUM-security for commands: *)
definition 
  com_sifum_secure :: "'Com × 'Var Mds ⇒ bool"
where 
  "com_sifum_secure cmd ≡ case cmd of (c,mds⇩s) ⇒ c ∼⇘mds⇩s⇙ c"

(* Continuous SIFUM-security 
   (where we don't care about whether the prog has any assumptions at termination *)
definition 
  prog_sifum_secure_cont :: "('Com × 'Var Mds) list ⇒ bool"
where "prog_sifum_secure_cont cmds =
   (∀ mem⇩1 mem⇩2. INIT mem⇩1 ∧ INIT mem⇩2 ∧ mem⇩1 =⇧l mem⇩2 ⟶
    (∀ sched cms⇩1' mem⇩1'.
     (cmds, mem⇩1) →⇘sched⇙ (cms⇩1', mem⇩1') ⟶
      (∃ cms⇩2' mem⇩2'. (cmds, mem⇩2) →⇘sched⇙ (cms⇩2', mem⇩2') ∧
                      map snd cms⇩1' = map snd cms⇩2' ∧
                      length cms⇩2' = length cms⇩1' ∧
                      (∀ x. dma mem⇩1' x = Low ∧ (x ∈ 𝒞 ∨ (∀ i < length cms⇩1'.
                        x ∉ snd (cms⇩1' ! i) AsmNoReadOrWrite)) ⟶ mem⇩1' x = mem⇩2' x))))"

(* Note that it is equivalent to the following because the 
   programming language is deterministic *)
lemma prog_sifum_secure_cont_def2:
  "prog_sifum_secure_cont cmds ≡
   (∀ mem⇩1 mem⇩2. INIT mem⇩1 ∧ INIT mem⇩2 ∧ mem⇩1 =⇧l mem⇩2 ⟶
    (∀ sched cms⇩1' mem⇩1'.
     (cmds, mem⇩1) →⇘sched⇙ (cms⇩1', mem⇩1') ⟶
      (∃ cms⇩2' mem⇩2'. (cmds, mem⇩2) →⇘sched⇙ (cms⇩2', mem⇩2')) ∧
      (∀ cms⇩2' mem⇩2'. (cmds, mem⇩2) →⇘sched⇙ (cms⇩2', mem⇩2') ⟶
                      map snd cms⇩1' = map snd cms⇩2' ∧
                      length cms⇩2' = length cms⇩1' ∧
                      (∀ x. dma mem⇩1' x = Low ∧ (x ∈ 𝒞 ∨ (∀ i < length cms⇩1'.
                        x ∉ snd (cms⇩1' ! i) AsmNoReadOrWrite)) ⟶ mem⇩1' x = mem⇩2' x))))"
  apply(rule eq_reflection)
  unfolding prog_sifum_secure_cont_def
  apply(rule iffI)
   apply(blast dest: meval_sched_det)
  by fastforce

subsection ‹Sound Mode Use›


(* Suggestive notation for substitution / function application *)
definition 
  subst :: "('a ⇀ 'b) ⇒ ('a ⇒ 'b) ⇒ ('a ⇒ 'b)"
where
  "subst f mem = (λ x. case f x of
                         None ⇒ mem x |
                         Some v ⇒ v)"

abbreviation 
  subst_abv :: "('a ⇒ 'b) ⇒ ('a ⇀ 'b) ⇒ ('a ⇒ 'b)" ("_ [↦_]" [900, 0] 1000)
where
  "f [↦ σ] ≡ subst σ f"

lemma subst_not_in_dom : "⟦ x ∉ dom σ ⟧ ⟹ mem [↦ σ] x = mem x"
  by (simp add: domIff subst_def)

(* Toby: we restrict not reading to also imply not modifying a variable.
         This is done mostly to simplify part of the reasoning in the
         Compositionality theory, but also because reconciling doesnt_read_or_modify
         forcing also not reading the variable's classification in the case
         in the case where it would allow non-reading modifications proved
         to get too unwieldy *)
definition 
  doesnt_read_or_modify_vars :: "'Com ⇒ 'Var set ⇒ bool"
where
  "doesnt_read_or_modify_vars c X = (∀ mds mem c' mds' mem'.
  ⟨ c, mds, mem ⟩ ↝ ⟨ c', mds', mem' ⟩ ⟶
  ((∀x∈X. (∀ v. ⟨ c, mds, mem (x := v) ⟩ ↝ ⟨ c', mds', mem' (x := v) ⟩))))"

definition
  vars_𝒞 :: "'Var set ⇒ 'Var set"
where
  "vars_𝒞 X ≡ ⋃x∈X. 𝒞_vars x"

lemma vars_𝒞_subset_𝒞:
  "vars_𝒞 X ⊆ 𝒞"
  by(auto simp: 𝒞_def vars_𝒞_def)

(* Toby: doesnt_read_or_modify now implies that the classification is not read too *)
definition 
  doesnt_read_or_modify :: "'Com ⇒ 'Var ⇒ bool"
where
  "doesnt_read_or_modify c x ≡ doesnt_read_or_modify_vars c ({x} ∪ 𝒞_vars x)"

definition 
  doesnt_modify :: "'Com ⇒ 'Var ⇒ bool"
where
  "doesnt_modify c x = (∀ mds mem c' mds' mem'. (⟨ c, mds, mem ⟩ ↝ ⟨ c', mds', mem' ⟩) ⟶
                        mem x = mem' x ∧  dma mem x = dma mem' x)"

lemma noread_nowrite:
  assumes step: "⟨c, mds, mem⟩ ↝ ⟨c', mds', mem'⟩"
  assumes noread: "(⋀v. ⟨c, mds, mem(x := v)⟩ ↝ ⟨c', mds', mem'(x := v)⟩)"
  shows "mem x = mem' x"
proof -
  from noread have "⟨c, mds, mem(x := (mem x))⟩ ↝ ⟨c', mds', mem'(x := (mem x))⟩"
    by blast
  hence "⟨c, mds, mem⟩ ↝ ⟨c', mds', mem'(x := (mem x))⟩" by simp
  from step this have "mem' = mem'(x := (mem x))" by (blast dest: deterministic)
  hence "mem' x = (mem'(x := (mem x))) x" by(rule arg_cong)
  thus ?thesis by simp
qed

(* Toby: not sure whether this implication should just be made explicit in the
         definition of doesnt_read_or_modify or not *)
lemma doesnt_read_or_modify_doesnt_modify:
  "doesnt_read_or_modify c x ⟹ doesnt_modify c x"
  by(fastforce simp: doesnt_modify_def doesnt_read_or_modify_def doesnt_read_or_modify_vars_def 
               intro: noread_nowrite dma_𝒞_vars)

(* Local reachability of local configurations: *)
inductive_set 
  loc_reach :: "('Com, 'Var, 'Val) LocalConf ⇒ ('Com, 'Var, 'Val) LocalConf set"
  for lc :: "(_, _, _) LocalConf"
where
  refl : "⟨fst (fst lc), snd (fst lc), snd lc⟩ ∈ loc_reach lc" |
  step : "⟦ ⟨c', mds', mem'⟩ ∈ loc_reach lc;
            ⟨c', mds', mem'⟩ ↝ ⟨c'', mds'', mem''⟩ ⟧ ⟹
          ⟨c'', mds'', mem''⟩ ∈ loc_reach lc" |
  mem_diff : "⟦ ⟨ c', mds', mem' ⟩ ∈ loc_reach lc;
                (∀ x. var_asm_not_written mds' x ⟶ mem' x = mem'' x ∧ dma mem' x = dma mem'' x) ⟧ ⟹
              ⟨ c', mds', mem'' ⟩ ∈ loc_reach lc"

lemma neval_loc_reach:
  "neval lc' n lc'' ⟹ lc' ∈ loc_reach lc ⟹ lc'' ∈ loc_reach lc"
proof(induct rule: neval.induct)
  case (neval_0 x y)
    thus ?case by simp
next
  case (neval_S_n x y n z)
  from ‹x ∈ loc_reach lc› and ‹x ↝ y› have "y ∈ loc_reach lc" 
    (* TODO: can we get rid of this case_tac nonsense? *)
    apply(case_tac x, rename_tac a b, case_tac a, clarsimp)
    apply(case_tac y, rename_tac c d, case_tac c, clarsimp)
    by(blast intro: loc_reach.step)
  thus ?case
    using neval_S_n(3) by blast
qed
    

definition 
  locally_sound_mode_use :: "(_, _, _) LocalConf ⇒ bool"
where
  "locally_sound_mode_use lc =
  (∀ c' mds' mem'. ⟨ c', mds', mem' ⟩ ∈ loc_reach lc ⟶
    (∀ x. (x ∈ mds' GuarNoReadOrWrite ⟶ doesnt_read_or_modify c' x) ∧
          (x ∈ mds' GuarNoWrite ⟶ doesnt_modify c' x)))"

(* RobS: The same property, but for an individual evaluation. Note it doesn't rely on mem! *)
definition 
  respects_own_guarantees :: "('Com × 'Var Mds) ⇒ bool"
where
  "respects_own_guarantees cm ≡
  (∀ x. (x ∈ (snd cm) GuarNoReadOrWrite ⟶ doesnt_read_or_modify (fst cm) x) ∧
        (x ∈ (snd cm) GuarNoWrite ⟶ doesnt_modify (fst cm) x))"

lemma locally_sound_mode_use_def2:
  "locally_sound_mode_use lc ≡ ∀lc' ∈ loc_reach lc. respects_own_guarantees (fst lc')"
  apply(rule eq_reflection)
  apply(simp add: locally_sound_mode_use_def respects_own_guarantees_def)
  apply force
  done

lemma locally_sound_respects_guarantees:
  "locally_sound_mode_use (cm, mem) ⟹ respects_own_guarantees cm"
  unfolding locally_sound_mode_use_def respects_own_guarantees_def
  by (metis fst_conv loc_reach.refl)

definition 
  compatible_modes :: "('Var Mds) list ⇒ bool"
where
  "compatible_modes mdss = (∀ (i :: nat) x. i < length mdss ⟶
    (x ∈ (mdss ! i) AsmNoReadOrWrite ⟶
     (∀ j < length mdss. j ≠ i ⟶ x ∈ (mdss ! j) GuarNoReadOrWrite)) ∧
    (x ∈ (mdss ! i) AsmNoWrite ⟶
     (∀ j < length mdss. j ≠ i ⟶ x ∈ (mdss ! j) GuarNoWrite)))"

definition 
  reachable_mode_states :: "('Com, 'Var, 'Val) GlobalConf ⇒ (('Var Mds) list) set"
where 
  "reachable_mode_states gc ≡
     {mdss. (∃ cms' mem' sched. gc →⇘sched⇙ (cms', mem') ∧ map snd cms' = mdss)}"

definition 
  globally_sound_mode_use :: "('Com, 'Var, 'Val) GlobalConf ⇒ bool"
where 
  "globally_sound_mode_use gc ≡
     (∀ mdss. mdss ∈ reachable_mode_states gc ⟶ compatible_modes mdss)"

primrec 
  sound_mode_use :: "(_, _, _) GlobalConf ⇒ bool"
where
  "sound_mode_use (cms, mem) =
     (list_all (λ cm. locally_sound_mode_use (cm, mem)) cms ∧
      globally_sound_mode_use (cms, mem))"

(* We now show that mm_equiv itself forms a strong low bisimulation modulo modes: *)
lemma mm_equiv_sym:
  assumes equivalent: "⟨c⇩1, mds⇩1, mem⇩1⟩ ≈ ⟨c⇩2, mds⇩2, mem⇩2⟩"
  shows "⟨c⇩2, mds⇩2, mem⇩2⟩ ≈ ⟨c⇩1, mds⇩1, mem⇩1⟩"
proof -
  from equivalent obtain ℛ
    where ℛ_bisim: "strong_low_bisim_mm ℛ ∧ (⟨c⇩1, mds⇩1, mem⇩1⟩, ⟨c⇩2, mds⇩2, mem⇩2⟩) ∈ ℛ"
    by (metis mm_equiv.simps)
  hence "sym ℛ"
    by (auto simp: strong_low_bisim_mm_def)
  hence "(⟨c⇩2, mds⇩2, mem⇩2⟩, ⟨c⇩1, mds⇩1, mem⇩1⟩) ∈ ℛ"
    by (metis ℛ_bisim symE)
  thus ?thesis
    by (metis ℛ_bisim mm_equiv.intros)
qed

lemma low_indistinguishable_sym: "lc ∼⇘mds⇙ lc' ⟹ lc' ∼⇘mds⇙ lc"
  apply(clarsimp simp: low_indistinguishable_def)
  apply(rule mm_equiv_sym)
  apply(blast dest: low_mds_eq_sym)
  done

lemma mm_equiv_glob_consistent: "closed_glob_consistent mm_equiv"
  unfolding closed_glob_consistent_def
  apply clarify
  apply (erule mm_equiv_elim)
  by (auto simp: strong_low_bisim_mm_def closed_glob_consistent_def)

lemma mm_equiv_strong_low_bisim: "strong_low_bisim_mm mm_equiv"
  unfolding strong_low_bisim_mm_def
proof (auto)
  show "closed_glob_consistent mm_equiv" by (rule mm_equiv_glob_consistent)
next
  fix c⇩1 mds mem⇩1 c⇩2 mem⇩2 x
  assume "⟨ c⇩1, mds, mem⇩1 ⟩ ≈ ⟨ c⇩2, mds, mem⇩2 ⟩"
  then obtain ℛ where
    "strong_low_bisim_mm ℛ ∧ (⟨ c⇩1, mds, mem⇩1 ⟩, ⟨ c⇩2, mds, mem⇩2 ⟩) ∈ ℛ"
    by blast
  thus "mem⇩1 =⇘mds⇙⇧l mem⇩2" by (auto simp: strong_low_bisim_mm_def)
next
  fix c⇩1 :: 'Com
  fix mds mem⇩1 c⇩2 mem⇩2 c⇩1' mds' mem⇩1'
  let ?lc⇩1 = "⟨ c⇩1, mds, mem⇩1 ⟩" and
      ?lc⇩1' = "⟨ c⇩1', mds', mem⇩1' ⟩" and
      ?lc⇩2 = "⟨ c⇩2, mds, mem⇩2 ⟩"
  assume "?lc⇩1 ≈ ?lc⇩2"
  then obtain ℛ where "strong_low_bisim_mm ℛ ∧ (?lc⇩1, ?lc⇩2) ∈ ℛ"
    by (rule mm_equiv_elim, blast)
  moreover assume "?lc⇩1 ↝ ?lc⇩1'"
  ultimately show "∃ c⇩2' mem⇩2'. ?lc⇩2 ↝ ⟨ c⇩2', mds', mem⇩2' ⟩ ∧ ?lc⇩1' ≈ ⟨ c⇩2', mds', mem⇩2' ⟩"
    by (simp add: strong_low_bisim_mm_def mm_equiv_sym, blast)
next
  show "sym mm_equiv"
    by (auto simp: sym_def mm_equiv_sym)
qed

end

end