Theory secTypes

theory secTypes
imports Semantics
begin

section ‹Security types›

subsection ‹Security definitions›


datatype secLevel = Low | High

type_synonym typeEnv = "vname ⇀ secLevel"

inductive secExprTyping :: "typeEnv ⇒ expr ⇒ secLevel ⇒ bool" (‹_ ⊢ _ : _›)
where typeVal:  "Γ ⊢ Val V : lev"

  | typeVar:    "Γ Vn = Some lev ⟹ Γ ⊢ Var Vn : lev"

  | typeBinOp1: "⟦Γ ⊢ e1 : Low; Γ ⊢ e2 : Low⟧ ⟹ Γ ⊢ e1 «bop» e2 : Low"

  | typeBinOp2: "⟦Γ ⊢ e1 : High; Γ ⊢ e2 : lev⟧ ⟹ Γ ⊢ e1 «bop» e2 : High"

  | typeBinOp3: "⟦Γ ⊢ e1 : lev; Γ ⊢ e2 : High⟧ ⟹ Γ ⊢ e1 «bop» e2 : High"



inductive secComTyping :: "typeEnv ⇒ secLevel ⇒ com ⇒ bool" (‹_,_ ⊢ _›)
where typeSkip:  "Γ,T ⊢ Skip"

  | typeAssH:    "Γ V = Some High ⟹ Γ,T ⊢ V := e"

  | typeAssL:    "⟦Γ ⊢ e : Low; Γ V = Some Low⟧ ⟹ Γ,Low ⊢ V := e"

  | typeSeq:     "⟦Γ,T ⊢ c1; Γ,T ⊢ c2⟧ ⟹ Γ,T ⊢ c1;;c2"

  | typeWhile:   "⟦Γ ⊢ b : T; Γ,T ⊢ c⟧ ⟹ Γ,T ⊢ while (b) c"

  | typeIf:      "⟦Γ ⊢ b : T; Γ,T ⊢ c1; Γ,T ⊢ c2⟧ ⟹ Γ,T ⊢ if (b) c1 else c2"

  | typeConvert: "Γ,High ⊢ c ⟹ Γ,Low ⊢ c"


subsection ‹Lemmas concerning expressions›

lemma exprTypeable:
  assumes "fv e ⊆ dom Γ" obtains T where "Γ ⊢ e : T"
proof -
  from ‹fv e ⊆ dom Γ› have "∃T. Γ ⊢ e : T"
  proof(induct e)
    case (Val V)
    have "Γ ⊢ Val V : Low" by(rule typeVal)
    thus ?case by (rule exI)
  next
    case (Var V)
    have "V ∈ fv (Var V)" by simp
    with ‹fv (Var V) ⊆ dom Γ› have "V ∈ dom Γ" by simp
    then obtain T where "Γ V = Some T" by auto
    hence "Γ ⊢ Var V : T" by (rule typeVar)
    thus ?case by (rule exI)
  next
    case (BinOp e1 bop e2)
    note IH1 = ‹fv e1 ⊆ dom Γ ⟹ ∃T. Γ ⊢ e1 : T›
    note IH2 = ‹fv e2 ⊆ dom Γ ⟹ ∃T. Γ ⊢ e2 : T›
    from ‹fv (e1 «bop» e2) ⊆ dom Γ›
    have "fv e1 ⊆ dom Γ" and "fv e2 ⊆ dom Γ" by auto
    from IH1[OF ‹fv e1 ⊆ dom Γ›] obtain T1 where "Γ ⊢ e1 : T1" by auto
    from IH2[OF ‹fv e2 ⊆ dom Γ›] obtain T2 where "Γ ⊢ e2 : T2" by auto
    show ?case
    proof (cases T1)
      case Low
      show ?thesis
      proof (cases T2)
        case Low
        with ‹Γ ⊢ e1 : T1› ‹Γ ⊢ e2 : T2› ‹T1 = Low›
        have "Γ ⊢ e1 «bop» e2 : Low" by(simp add:typeBinOp1)
        thus ?thesis by(rule exI)
      next
        case High
        with ‹Γ ⊢ e1 : T1› ‹Γ ⊢ e2 : T2› ‹T1 = Low›
        have "Γ ⊢ e1 «bop» e2 : High" by(simp add:typeBinOp3)
        thus ?thesis by(rule exI)
      qed
    next
      case High
      with ‹Γ ⊢ e1 : T1› ‹Γ ⊢ e2 : T2›
      have "Γ ⊢ e1 «bop» e2 : High" by (simp add: typeBinOp2)
      thus ?thesis by (rule exI)
    qed
  qed
  with that show ?thesis by blast
qed


lemma exprBinopTypeable: 
  assumes "Γ ⊢ e1 «bop» e2 : T"
  shows "(∃T1. Γ ⊢ e1 : T1) ∧ (∃T2. Γ ⊢ e2 : T2)"
using assms by(auto elim:secExprTyping.cases)



lemma exprTypingHigh: 
  assumes "Γ ⊢ e : T" and "x ∈ fv e" and "Γ x = Some High"
  shows "Γ ⊢ e : High"
using assms
proof (induct e arbitrary:T)
  case (Val V) show ?case by (rule typeVal)
next
  case (Var V)
  from ‹x ∈ fv (Var V)› have "x = V" by simp
  with ‹Γ x = Some High› show ?case by(simp add:typeVar)
next
  case (BinOp e1 bop e2)
  note IH1 = ‹⋀T. ⟦Γ ⊢ e1 : T; x ∈ fv e1; Γ x = Some High⟧ ⟹ Γ ⊢ e1 : High›
  note IH2 = ‹⋀T. ⟦Γ ⊢ e2 : T; x ∈ fv e2; Γ x = Some High⟧ ⟹ Γ ⊢ e2 : High›
  from ‹Γ ⊢ e1 «bop» e2 : T› 
  have T:"(∃T1. Γ ⊢ e1 : T1) ∧ (∃T2. Γ ⊢ e2 : T2)" by (auto intro!:exprBinopTypeable)
  then obtain T1 where "Γ ⊢ e1 : T1" by auto
  from T obtain T2 where "Γ ⊢ e2 : T2" by auto
  from ‹x ∈ fv (e1 «bop» e2)› have "x ∈ (fv e1 ∪ fv e2)" by simp
  hence "x ∈ fv e1 ∨ x ∈ fv e2" by auto
  thus ?case
  proof
    assume "x ∈ fv e1"
    from IH1[OF ‹Γ ⊢ e1 : T1› this ‹Γ x = Some High›] have "Γ ⊢ e1 : High" .
    with ‹Γ ⊢ e2 : T2› show ?thesis by(simp add:typeBinOp2)
  next 
    assume "x ∈ fv e2" 
    from IH2[OF ‹Γ ⊢ e2 : T2› this ‹Γ x = Some High›] have "Γ ⊢ e2 : High" .
    with ‹Γ ⊢ e1 : T1› show ?thesis by(simp add:typeBinOp3)
  qed
qed


lemma exprTypingLow: 
  assumes "Γ ⊢ e : Low" and "x ∈ fv e" shows "Γ x = Some Low"
using assms
proof (induct e)
  case (Val V)
  have "fv (Val V) =  {}" by (rule FVc)
  with ‹x ∈ fv (Val V)› have False by auto
  thus ?thesis by simp
next
  case (Var V)
  from ‹x ∈ fv (Var V)› have xV: "x = V" by simp
  from ‹Γ ⊢ Var V : Low› have "Γ V = Some Low" by (auto elim:secExprTyping.cases)
  with xV show ?thesis by simp
next
  case (BinOp e1 bop e2)
  note IH1 = ‹⟦Γ ⊢ e1 : Low; x ∈ fv e1⟧ ⟹ Γ x = Some Low›
  note IH2=‹⟦Γ ⊢ e2 : Low; x ∈ fv e2⟧ ⟹ Γ x = Some Low›
  from ‹Γ ⊢ e1 «bop» e2 : Low› have "Γ ⊢ e1 : Low" and "Γ ⊢ e2 : Low"
    by(auto elim:secExprTyping.cases)
  from ‹x ∈ fv (e1 «bop» e2)› have "x ∈ fv e1 ∪ fv e2" by (simp add:FVe)
  hence "x ∈ fv e1 ∨ x ∈ fv e2" by auto
  thus ?case
  proof
    assume "x ∈ fv e1"
    with IH1[OF ‹Γ ⊢ e1 : Low›] show ?thesis by auto
  next
    assume "x ∈ fv e2" 
    with IH2[OF ‹Γ ⊢ e2 : Low›] show ?thesis by auto
  qed
qed


lemma typeableFreevars:
  assumes "Γ ⊢ e : T" shows "fv e ⊆ dom Γ"
using assms
proof(induct e arbitrary:T)
  case (Val V)
  have "fv (Val V) = {}" by (rule FVc)
  thus ?case by simp
next
  case (Var V)
  show ?case
  proof
    fix x assume "x ∈ fv (Var V)"
    hence "x = V" by simp 
    from ‹Γ ⊢ Var V : T› have  "Γ V = Some T" by (auto elim:secExprTyping.cases)
    with ‹x = V› show "x ∈ dom Γ" by auto
  qed
next
  case (BinOp e1 bop e2)
  note IH1 = ‹⋀T. Γ ⊢ e1 : T  ⟹ fv e1 ⊆ dom Γ›
  note IH2 = ‹⋀T. Γ ⊢ e2 : T  ⟹ fv e2 ⊆ dom Γ›
  show ?case
  proof
    fix x assume "x ∈ fv (e1 «bop» e2)"
    from ‹Γ ⊢ e1 «bop» e2 : T› 
    have Q:"(∃T1. Γ ⊢ e1 : T1) ∧ (∃T2. Γ ⊢ e2 : T2)" 
      by(rule exprBinopTypeable)
    then obtain T1 where "Γ ⊢ e1 : T1" by blast
    from Q obtain T2 where "Γ ⊢ e2 : T2" by blast
    from IH1[OF ‹Γ ⊢ e1 : T1›] have "fv e1 ⊆ dom Γ" .
    moreover
    from IH2[OF ‹Γ ⊢ e2 : T2›] have "fv e2 ⊆ dom Γ" .
    ultimately have "(fv e1) ∪ (fv e2) ⊆ dom Γ" by auto
    hence "fv (e1 «bop» e2) ⊆ dom Γ" by(simp add:FVe)
    with ‹x ∈ fv (e1 «bop» e2)› show "x ∈ dom Γ" by auto
  qed
qed


(* We assume that expressions are type correct and thus never evaluate to None.
   In this setting, the first premise is not needed.
   But for further extensions of the language with a standard type system 
   we do not remove it. *)
lemma exprNotNone:
assumes "Γ ⊢ e : T" and "fv e ⊆ dom s"
shows "⟦e⟧ s ≠ None"
using assms
proof (induct e arbitrary: Γ T s)
  case (Val v)
  show ?case by(simp add:Val)
next
  case (Var V)
  have "⟦Var V⟧ s = s V" by (simp add:Var)
  have "V ∈ fv (Var V)" by (auto simp add:FVv)
  with ‹fv (Var V) ⊆ dom s› have "V ∈ dom s" by simp
  thus ?case by auto
next
  case (BinOp e1 bop e2)
  note IH1 = ‹⋀T. ⟦Γ ⊢ e1 : T; fv e1 ⊆ dom s ⟧  ⟹ ⟦e1⟧ s ≠ None›
  note IH2 = ‹⋀T. ⟦Γ ⊢ e2 : T; fv e2 ⊆ dom s ⟧  ⟹ ⟦e2⟧ s ≠ None›
  from ‹Γ ⊢ e1 «bop» e2 :  T› have "(∃T1. Γ ⊢ e1 : T1) ∧ (∃T2. Γ ⊢ e2 : T2)"
    by(rule exprBinopTypeable)
  then obtain T1 T2 where "Γ ⊢ e1 : T1" and "Γ ⊢ e2 : T2" by blast
  from ‹fv (e1 «bop» e2)  ⊆ dom s› have "fv e1 ∪ fv e2 ⊆ dom s" by(simp add:FVe)
  hence "fv e1 ⊆ dom s" and "fv e2 ⊆ dom s" by auto
  from IH1[OF ‹Γ ⊢ e1 : T1› ‹fv e1 ⊆ dom s›] have "⟦e1⟧s ≠ None" .
  moreover from IH2[OF ‹Γ ⊢ e2 : T2› ‹fv e2 ⊆ dom s›] have "⟦e2⟧s ≠ None" .
  ultimately show ?case
    apply(cases bop) apply auto
    apply(case_tac y,auto,case_tac ya,auto)+
    done
qed



subsection ‹Noninterference definitions›

subsubsection ‹Low Equivalence›

text ‹Low Equivalence is reflexive even if the involved states are undefined. 
  But in non-reflexive situations low variables must be initialized 
  (i.e. ‹∈ dom state›), otherwise the proof will not work. This is not 
  a restriction, but a natural requirement, and could be formalized as part of 
  a standard type system.

  Low equivalence is also symmetric and transitiv (see lemmas) hence an
  equivalence relation.›


definition lowEquiv :: "typeEnv ⇒ state ⇒ state ⇒ bool" (‹_ ⊢ _ ≈⇩L _›)
where "Γ ⊢ s1 ≈⇩L s2 ≡ ∀v∈dom Γ. Γ v = Some Low ⟶ (s1 v = s2 v)"


lemma lowEquivReflexive: "Γ ⊢ s1 ≈⇩L s1" 
by(simp add:lowEquiv_def)

lemma lowEquivSymmetric:
  "Γ ⊢ s1 ≈⇩L s2 ⟹ Γ ⊢ s2 ≈⇩L s1"
by(simp add:lowEquiv_def)

lemma lowEquivTransitive:
  "⟦Γ ⊢ s1 ≈⇩L s2; Γ ⊢ s2 ≈⇩L s3⟧ ⟹ Γ ⊢ s1 ≈⇩L s3"
by(simp add:lowEquiv_def)



subsubsection ‹Non Interference›


definition nonInterference :: "typeEnv ⇒ com ⇒ bool"
where "nonInterference Γ c ≡ 
  (∀s1 s2 s1' s2'. (Γ ⊢ s1 ≈⇩L s2 ∧ ⟨c,s1⟩ →* ⟨Skip,s1'⟩ ∧ ⟨c,s2⟩ →* ⟨Skip,s2'⟩) 
    ⟶ Γ ⊢ s1' ≈⇩L s2')"

lemma nonInterferenceI: 
  "⟦⋀s1 s2 s1' s2'. ⟦Γ ⊢ s1 ≈⇩L s2; ⟨c,s1⟩ →* ⟨Skip,s1'⟩; ⟨c,s2⟩ →* ⟨Skip,s2'⟩⟧
  ⟹ Γ ⊢ s1' ≈⇩L s2'⟧ ⟹ nonInterference Γ c"
by(auto simp:nonInterference_def)


lemma interpretLow:
  assumes "Γ ⊢ s1 ≈⇩L s2" and all:"∀V∈fv e. Γ V = Some Low"
  shows "⟦e⟧ s1 = ⟦e⟧ s2"
using all
proof (induct e)
  case (Val v)
  show ?case by (simp add: Val)
next
  case (Var V)
  have "⟦Var V⟧ s1 = s1 V" and "⟦Var V⟧ s2 = s2 V" by(auto simp:Var)
  have "V ∈ fv (Var V)" by(simp add:FVv)
  from ‹V ∈ fv (Var V)› ‹∀X∈fv (Var V). Γ X = Some Low› have "Γ V = Some Low" by simp
  with assms have "s1 V = s2 V" by(auto simp add:lowEquiv_def)
  thus ?case by auto
next
  case (BinOp e1 bop e2)
  note IH1 = ‹∀V∈fv e1. Γ V = Some Low ⟹ ⟦e1⟧s1 = ⟦e1⟧s2›
  note IH2 = ‹∀V∈fv e2. Γ V = Some Low ⟹ ⟦e2⟧s1 = ⟦e2⟧s2›
  from ‹∀V∈fv (e1 «bop» e2). Γ V = Some Low› have "∀V∈fv e1. Γ V = Some Low"
    and "∀V∈ fv e2. Γ V = Some Low" by auto
  from IH1[OF ‹∀V∈fv e1. Γ V = Some Low›] have "⟦e1⟧ s1 = ⟦e1⟧ s2" .
  moreover
  from IH2[OF ‹∀V∈fv e2. Γ V = Some Low›] have "⟦e2⟧ s1 = ⟦e2⟧ s2" .
  ultimately show ?case by(cases "⟦e1⟧ s2",auto)
qed


lemma interpretLow2:
  assumes "Γ ⊢ e : Low" and "Γ ⊢ s1 ≈⇩L s2" shows "⟦e⟧ s1 = ⟦e⟧ s2"
proof -
  from ‹Γ ⊢ e : Low› have "fv e ⊆ dom Γ" by(auto dest:typeableFreevars)
  have "∀x∈ fv e. Γ x = Some Low"
  proof
    fix x assume "x ∈ fv e"
    with ‹Γ ⊢ e : Low› show "Γ x = Some Low" by(auto intro:exprTypingLow)
  qed
  with ‹Γ ⊢ s1 ≈⇩L s2› show ?thesis by(rule interpretLow)
qed


lemma assignNIhighlemma:
  assumes "Γ ⊢ s1 ≈⇩L s2"  and "Γ V = Some High" and "s1' = s1(V:= ⟦e⟧ s1)" 
  and "s2' = s2(V:= ⟦e⟧ s2)"
  shows "Γ ⊢ s1' ≈⇩L s2'"
proof -
  { fix V' assume "V' ∈ dom Γ" and  "Γ V' = Some Low"
    from ‹Γ ⊢ s1 ≈⇩L s2›  ‹Γ V' = Some Low› have "s1 V' = s2 V'" 
      by(auto simp add:lowEquiv_def)
    have "s1' V' = s2' V'"
    proof(cases "V' = V")
      case True
      with ‹Γ V' = Some Low› ‹Γ V = Some High› have False by simp
      thus ?thesis by simp
    next
      case False
      with ‹s1' = s1(V:= ⟦e⟧ s1)› ‹s2' = s2(V:= ⟦e⟧ s2)›
      have "s1 V' = s1' V'" and "s2 V' = s2' V'" by auto
      with ‹s1 V' = s2 V'› show ?thesis by simp
    qed
  }
  thus ?thesis by(auto simp add:lowEquiv_def)
qed



lemma assignNIlowlemma:
  assumes "Γ ⊢ s1 ≈⇩L s2"  and "Γ V = Some Low" and "Γ ⊢ e : Low" 
  and "s1' = s1(V:= ⟦e⟧ s1)" and "s2' = s2(V:= ⟦e⟧ s2)"
  shows "Γ ⊢ s1' ≈⇩L s2'" 
proof -
  { fix V' assume "V' ∈ dom Γ" and  "Γ V' = Some Low"
    from ‹Γ ⊢ s1 ≈⇩L s2›  ‹Γ V' = Some Low›
    have "s1 V' = s2 V'" by(auto simp add:lowEquiv_def)
    have "s1' V' = s2' V'"
    proof(cases "V' = V")
      case True
      with ‹s1' = s1(V:= ⟦e⟧ s1)› ‹s2' = s2(V:= ⟦e⟧ s2)›
      have "s1' V' = ⟦e⟧ s1" and "s2' V' = ⟦e⟧ s2" by auto
      from ‹Γ ⊢ e : Low› ‹Γ ⊢ s1 ≈⇩L s2› have "⟦e⟧ s1 = ⟦e⟧ s2" 
        by(auto intro:interpretLow2)
      with ‹s1' V' = ⟦e⟧ s1› ‹s2' V' = ⟦e⟧ s2› show ?thesis by simp
    next
      case False
      with ‹s1' = s1(V:= ⟦e⟧ s1)› ‹s2' = s2(V:= ⟦e⟧ s2)›
      have "s1' V' = s1 V'" and "s2' V' = s2 V'" by auto
      with ‹s1 V' = s2 V'› have "s1' V' = s2' V'" by simp
      with False ‹s1' V' = s1 V'› ‹s2' V' = s2 V'›
      show ?thesis by auto
    qed
  }
  thus ?thesis by(simp add:lowEquiv_def)
qed


text ‹Sequential Compositionality is given the status of a theorem because 
  compositionality is no longer valid in case of concurrency›

theorem SeqCompositionality:
  assumes "nonInterference Γ c1" and "nonInterference Γ c2" 
  shows "nonInterference Γ (c1;;c2)"
proof(rule nonInterferenceI)
  fix s1 s2 s1' s2'
  assume "Γ ⊢ s1 ≈⇩L s2" and "⟨c1;;c2,s1⟩ →* ⟨Skip,s1'⟩" 
    and "⟨c1;;c2,s2⟩ →* ⟨Skip,s2'⟩"
  from ‹⟨c1;;c2,s1⟩ →* ⟨Skip,s1'⟩› obtain s1'' where "⟨c1,s1⟩ →* ⟨Skip,s1''⟩"
    and "⟨c2,s1''⟩ →* ⟨Skip,s1'⟩" by(auto dest:Seq_reds)
  from ‹⟨c1;;c2,s2⟩ →* ⟨Skip,s2'⟩› obtain s2'' where "⟨c1,s2⟩ →* ⟨Skip,s2''⟩"
    and "⟨c2,s2''⟩ →* ⟨Skip,s2'⟩" by(auto dest:Seq_reds)
  from ‹Γ ⊢ s1 ≈⇩L s2› ‹⟨c1,s1⟩ →* ⟨Skip,s1''⟩› ‹⟨c1,s2⟩ →* ⟨Skip,s2''⟩›
    ‹nonInterference Γ c1›
  have "Γ ⊢ s1'' ≈⇩L s2''" by(auto simp:nonInterference_def)
  with ‹⟨c2,s1''⟩ →* ⟨Skip,s1'⟩› ‹⟨c2,s2''⟩ →* ⟨Skip,s2'⟩› ‹nonInterference Γ c2› 
  show "Γ ⊢ s1' ≈⇩L s2'" by(auto simp:nonInterference_def)
qed



lemma WhileStepInduct:
  assumes while:"⟨while (b) c,s1⟩ →* ⟨Skip,s2⟩"
  and body:"⋀s1 s2. ⟨c,s1⟩ →* ⟨Skip,s2⟩  ⟹ Γ ⊢ s1 ≈⇩L s2" and "Γ,High ⊢ c"
  shows "Γ ⊢ s1 ≈⇩L s2"
using while
proof (induct rule:while_reds_induct)
  case (false s) thus ?case by(auto simp add:lowEquiv_def)
next 
  case (true s1 s3)
  from body[OF ‹⟨c,s1⟩ →* ⟨Skip,s3⟩›] have "Γ ⊢ s1 ≈⇩L s3" by simp
  with ‹Γ ⊢ s3 ≈⇩L s2› show ?case by(auto intro:lowEquivTransitive)
qed



text ‹In case control conditions from if/while are high, the body of an
  if/while must not change low variables in order to prevent implicit flow.
  That is, start and end state of any if/while body must be low equivalent.›

theorem highBodies:
  assumes "Γ,High ⊢ c" and "⟨c,s1⟩ →* ⟨Skip,s2⟩"
  shows "Γ ⊢ s1 ≈⇩L s2"
  ― ‹all intermediate states must be well formed, otherwise the proof does not 
  work for uninitialized variables. Thus it is propagated through the 
  theorem conclusion›
using assms
proof(induct c arbitrary:s1 s2 rule:com.induct)
  case Skip
  from ‹⟨Skip,s1⟩ →* ⟨Skip,s2⟩› have "s1 = s2" by (auto dest:Skip_reds)
  thus ?case by(simp add:lowEquiv_def)
next
  case (LAss V e)
  from ‹Γ,High ⊢ V:=e› have "Γ V = Some High" by(auto elim:secComTyping.cases)
  from ‹⟨V:=e,s1⟩ →* ⟨Skip,s2⟩› have "s2 = s1(V:= ⟦e⟧s1)" by (auto intro:LAss_reds)
  { fix V' assume "V' ∈ dom Γ" and "Γ V' = Some Low"
    have "s1 V' = s2 V'"
    proof(cases "V' = V")
      case True
      with ‹Γ V' = Some Low› ‹Γ V = Some High› have False by simp
      thus ?thesis by simp
    next
      case False
      with ‹s2 = s1(V:= ⟦e⟧s1)› show ?thesis by simp 
    qed
  }
  thus ?case by(auto simp add:lowEquiv_def)
next
  case (Seq c1 c2)
  note IH1 = ‹⋀s1 s2. ⟦Γ,High ⊢ c1; ⟨c1,s1⟩ →* ⟨Skip,s2⟩⟧ ⟹ Γ ⊢ s1 ≈⇩L s2›
  note IH2 = ‹⋀s1 s2. ⟦Γ,High ⊢ c2; ⟨c2,s1⟩ →* ⟨Skip,s2⟩⟧ ⟹ Γ ⊢ s1 ≈⇩L s2›
  from ‹Γ,High ⊢ c1;;c2› have "Γ,High ⊢ c1" and "Γ,High ⊢ c2"
    by(auto elim:secComTyping.cases)
  from ‹⟨c1;;c2,s1⟩ →* ⟨Skip,s2⟩› 
  have "∃s3. ⟨c1,s1⟩ →* ⟨Skip,s3⟩ ∧ ⟨c2,s3⟩ →* ⟨Skip,s2⟩" by(auto intro:Seq_reds)
  then obtain s3 where "⟨c1,s1⟩ →* ⟨Skip,s3⟩" and "⟨c2,s3⟩ →* ⟨Skip,s2⟩" by auto
  from IH1[OF ‹Γ,High ⊢ c1› ‹⟨c1,s1⟩ →* ⟨Skip,s3⟩›]
  have "Γ ⊢ s1 ≈⇩L s3" by simp
  from IH2[OF ‹Γ,High ⊢ c2› ‹⟨c2,s3⟩ →* ⟨Skip,s2⟩›]
  have "Γ ⊢ s3 ≈⇩L s2" by simp
  from ‹Γ ⊢ s1 ≈⇩L s3› ‹Γ ⊢ s3 ≈⇩L s2› show ?case
    by(auto intro:lowEquivTransitive)
next
  case (Cond b c1 c2)
  note IH1 = ‹⋀s1 s2. ⟦Γ,High ⊢ c1; ⟨c1,s1⟩ →* ⟨Skip,s2⟩⟧ ⟹ Γ ⊢ s1 ≈⇩L s2›
  note IH2 = ‹⋀s1 s2. ⟦Γ,High ⊢ c2; ⟨c2,s1⟩ →* ⟨Skip,s2⟩⟧ ⟹ Γ ⊢ s1 ≈⇩L s2›
  from ‹Γ,High ⊢ if (b) c1 else c2› have "Γ,High ⊢ c1" and "Γ,High ⊢ c2"
    by(auto elim:secComTyping.cases)
  from ‹⟨if (b) c1 else c2,s1⟩ →* ⟨Skip,s2⟩› 
  have "⟦b⟧ s1 = Some true ∨ ⟦b⟧ s1 = Some false" by(auto dest:Cond_True_or_False)
  thus ?case
  proof
    assume "⟦b⟧ s1 = Some true"
    with ‹⟨if (b) c1 else c2,s1⟩ →* ⟨Skip,s2⟩› have "⟨c1,s1⟩ →* ⟨Skip,s2⟩"
      by (auto intro:CondTrue_reds)
    from IH1[OF ‹Γ,High ⊢ c1› this] show ?thesis .
  next
    assume "⟦b⟧ s1 = Some false"
    with ‹⟨if (b) c1 else c2,s1⟩ →* ⟨Skip,s2⟩› have "⟨c2,s1⟩ →* ⟨Skip,s2⟩"
      by(auto intro:CondFalse_reds)
    from IH2[OF ‹Γ,High ⊢ c2› this] show ?thesis .
  qed
next
  case (While b c')
  note IH = ‹⋀s1 s2. ⟦Γ,High ⊢ c'; ⟨c',s1⟩ →* ⟨Skip,s2⟩⟧ ⟹ Γ ⊢ s1 ≈⇩L s2›
  from ‹Γ,High ⊢ while (b) c'› have "Γ,High ⊢ c'" by(auto elim:secComTyping.cases)
  from IH[OF this] 
  have "⋀s1 s2. ⟦⟨c',s1⟩ →* ⟨Skip,s2⟩⟧ ⟹ Γ ⊢ s1 ≈⇩L s2" .
  with ‹⟨while (b) c',s1⟩ →* ⟨Skip,s2⟩› ‹Γ,High ⊢ c'› 
  show ?case by(auto dest:WhileStepInduct)
qed



lemma CondHighCompositionality:
  assumes "Γ,High ⊢ if (b) c1 else c2"
  shows "nonInterference Γ (if (b) c1 else c2)"
proof(rule nonInterferenceI)
  fix s1 s2 s1' s2'
  assume "Γ ⊢ s1 ≈⇩L s2" and "⟨if (b) c1 else c2,s1⟩ →* ⟨Skip,s1'⟩" 
    and "⟨if (b) c1 else c2,s2⟩ →* ⟨Skip,s2'⟩"
  show "Γ ⊢ s1' ≈⇩L s2'"
  proof -
    from ‹Γ,High ⊢ if (b) c1 else c2› ‹⟨if (b) c1 else c2,s1⟩ →* ⟨Skip,s1'⟩›
    have "Γ ⊢ s1 ≈⇩L s1'" by(auto dest:highBodies)
    from ‹Γ,High ⊢ if (b) c1 else c2› ‹⟨if (b) c1 else c2,s2⟩ →* ⟨Skip,s2'⟩›
    have "Γ ⊢ s2 ≈⇩L s2'" by(auto dest:highBodies)
    with ‹Γ ⊢ s1 ≈⇩L s2› have "Γ ⊢ s1 ≈⇩L s2'" by(auto intro:lowEquivTransitive)
    from ‹Γ ⊢ s1 ≈⇩L s1'› have "Γ ⊢ s1' ≈⇩L s1" by(auto intro:lowEquivSymmetric)
    with ‹Γ ⊢ s1 ≈⇩L s2'› show ?thesis by(auto intro:lowEquivTransitive)
  qed
qed



lemma CondLowCompositionality:
  assumes "nonInterference Γ c1" and "nonInterference Γ c2" and "Γ ⊢ b : Low" 
  shows "nonInterference Γ (if (b) c1 else c2)"
proof(rule nonInterferenceI)
  fix s1 s2 s1' s2'
  assume "Γ ⊢ s1 ≈⇩L s2" and "⟨if (b) c1 else c2,s1⟩ →* ⟨Skip,s1'⟩" 
    and "⟨if (b) c1 else c2,s2⟩ →* ⟨Skip,s2'⟩"
  from ‹Γ ⊢ b : Low› ‹Γ ⊢ s1 ≈⇩L s2› have "⟦b⟧ s1 = ⟦b⟧ s2"
    by(auto intro:interpretLow2)
  from ‹⟨if (b) c1 else c2,s1⟩ →* ⟨Skip,s1'⟩› 
  have "⟦b⟧ s1 = Some true ∨ ⟦b⟧ s1 = Some false" by(auto dest:Cond_True_or_False)
  thus "Γ ⊢ s1' ≈⇩L s2'"
  proof
    assume "⟦b⟧ s1 = Some true"
    with ‹⟦b⟧ s1 = ⟦b⟧ s2› have "⟦b⟧ s2 = Some true" by(auto intro:CondTrue_reds)
    from ‹⟦b⟧ s1 = Some true› ‹⟨if (b) c1 else c2,s1⟩ →* ⟨Skip,s1'⟩›
    have "⟨c1,s1⟩ →* ⟨Skip,s1'⟩" by(auto intro:CondTrue_reds)
    from ‹⟦b⟧ s2 = Some true› ‹⟨if (b) c1 else c2,s2⟩ →* ⟨Skip,s2'⟩›
    have "⟨c1,s2⟩ →* ⟨Skip,s2'⟩" by(auto intro:CondTrue_reds)
    with ‹⟨c1,s1⟩ →* ⟨Skip,s1'⟩› ‹Γ ⊢ s1 ≈⇩L s2› ‹nonInterference Γ c1›
    show ?thesis by(auto simp:nonInterference_def)
  next
    assume "⟦b⟧ s1 = Some false"
    with ‹⟦b⟧ s1 = ⟦b⟧ s2› have "⟦b⟧ s2 = Some false" by(auto intro:CondTrue_reds)
    from ‹⟦b⟧ s1 = Some false› ‹⟨if (b) c1 else c2,s1⟩ →* ⟨Skip,s1'⟩›
    have "⟨c2,s1⟩ →* ⟨Skip,s1'⟩" by(auto intro:CondFalse_reds)
    from ‹⟦b⟧ s2 = Some false› ‹⟨if (b) c1 else c2,s2⟩ →* ⟨Skip,s2'⟩›
    have "⟨c2,s2⟩ →* ⟨Skip,s2'⟩" by(auto intro:CondFalse_reds)
    with ‹⟨c2,s1⟩ →* ⟨Skip,s1'⟩› ‹Γ ⊢ s1 ≈⇩L s2› ‹nonInterference Γ c2›
    show ?thesis by(auto simp:nonInterference_def)
  qed
qed


lemma WhileHighCompositionality:
  assumes "Γ,High ⊢ while (b) c'"
  shows "nonInterference Γ (while (b) c')"
proof(rule nonInterferenceI)
  fix s1 s2 s1' s2'
  assume "Γ ⊢ s1 ≈⇩L s2" and "⟨while (b) c',s1⟩ →* ⟨Skip,s1'⟩"
    and "⟨while (b) c',s2⟩ →* ⟨Skip,s2'⟩"
  show "Γ ⊢ s1' ≈⇩L s2'"
  proof -
    from ‹Γ,High ⊢ while (b) c'› ‹⟨while (b) c',s1⟩ →* ⟨Skip,s1'⟩›
    have "Γ ⊢ s1 ≈⇩L s1'" by(auto dest:highBodies)
    from ‹Γ,High ⊢ while (b) c'› ‹⟨while (b) c',s2⟩ →* ⟨Skip,s2'⟩›
    have "Γ ⊢ s2 ≈⇩L s2'" by(auto dest:highBodies)
    with ‹Γ ⊢ s1 ≈⇩L s2› have "Γ ⊢ s1 ≈⇩L s2'" by(auto intro:lowEquivTransitive)
    from ‹Γ ⊢ s1 ≈⇩L s1'› have "Γ ⊢ s1' ≈⇩L s1" by(auto intro:lowEquivSymmetric)
    with ‹Γ ⊢ s1 ≈⇩L s2'› show ?thesis by(auto intro:lowEquivTransitive)
  qed
qed



lemma WhileLowStepInduct:
  assumes  while1: "⟨while (b) c',s1⟩ →* ⟨Skip,s1'⟩"   
  and      while2: "⟨while (b) c',s2⟩→*⟨Skip,s2'⟩" 
  and      "Γ ⊢ b : Low"
  and      body:"⋀s1 s1' s2 s2'. ⟦⟨c',s1⟩ →* ⟨Skip,s1'⟩; ⟨c',s2⟩ →* ⟨Skip,s2'⟩;
                                   Γ ⊢ s1 ≈⇩L s2⟧  ⟹  Γ ⊢ s1' ≈⇩L s2'"
  and      le: "Γ ⊢ s1 ≈⇩L s2"
  shows    "Γ ⊢ s1' ≈⇩L s2'"
using while1 le while2
proof (induct arbitrary:s2 rule:while_reds_induct)
  case (false s1)
  from ‹Γ ⊢ b : Low› ‹Γ ⊢ s1 ≈⇩L s2› have "⟦b⟧ s1 = ⟦b⟧ s2" by(auto intro:interpretLow2)
  with ‹⟦b⟧ s1 = Some false› have "⟦b⟧ s2 = Some false" by simp
  with ‹⟨while (b) c',s2⟩→*⟨Skip,s2'⟩› have "s2 = s2'" by(auto intro:WhileFalse_reds)
  with ‹Γ ⊢ s1 ≈⇩L s2› show ?case by auto
next 
  case (true s1 s1'')
  note IH = ‹⋀s2''. ⟦Γ ⊢ s1'' ≈⇩L s2''; ⟨while (b) c',s2''⟩ →* ⟨Skip,s2'⟩⟧ 
    ⟹ Γ ⊢ s1' ≈⇩L s2'›
  from ‹Γ ⊢ b : Low› ‹Γ ⊢ s1 ≈⇩L s2› have "⟦b⟧ s1 = ⟦b⟧ s2" by(auto intro:interpretLow2)
  with ‹⟦b⟧ s1 = Some true› have "⟦b⟧ s2 = Some true" by simp
  with ‹⟨while (b) c',s2⟩ →* ⟨Skip,s2'⟩› obtain s2'' where "⟨c',s2⟩ →* ⟨Skip,s2''⟩"
    and "⟨while (b) c',s2''⟩ →* ⟨Skip,s2'⟩" by(auto dest:WhileTrue_reds)
  from body[OF ‹⟨c',s1⟩ →* ⟨Skip,s1''⟩› ‹⟨c',s2⟩ →* ⟨Skip,s2''⟩› ‹Γ ⊢ s1 ≈⇩L s2›]
  have "Γ ⊢ s1'' ≈⇩L s2''" .
  from IH[OF this ‹⟨while (b) c',s2''⟩ →* ⟨Skip,s2'⟩›] show ?case .
qed



lemma WhileLowCompositionality:
  assumes "nonInterference Γ c'" and "Γ ⊢ b : Low" and "Γ,Low ⊢ c'"
  shows "nonInterference Γ (while (b) c')"
proof(rule nonInterferenceI)
  fix s1 s2 s1' s2'
  assume "Γ ⊢ s1 ≈⇩L s2" and "⟨while (b) c',s1⟩ →* ⟨Skip,s1'⟩" 
    and "⟨while (b) c',s2⟩ →* ⟨Skip,s2'⟩"
  { fix s1 s2 s1'' s2''
    assume "⟨c',s1⟩ →* ⟨Skip,s1''⟩" and "⟨c',s2⟩ →* ⟨Skip,s2''⟩" 
      and  "Γ ⊢ s1 ≈⇩L s2"  
    with ‹nonInterference Γ c'› have "Γ ⊢ s1'' ≈⇩L s2''"
      by(auto simp:nonInterference_def)
  }
  hence "⋀s1 s1'' s2 s2''. ⟦⟨c',s1⟩ →* ⟨Skip,s1''⟩; ⟨c',s2⟩ →* ⟨Skip,s2''⟩;
                             Γ ⊢ s1 ≈⇩L s2⟧  ⟹  Γ ⊢ s1'' ≈⇩L s2''" by auto
  with ‹⟨while (b) c',s1⟩ →* ⟨Skip,s1'⟩› ‹⟨while (b) c',s2⟩ →* ⟨Skip,s2'⟩›
    ‹Γ ⊢ b : Low› ‹Γ ⊢ s1 ≈⇩L s2› show "Γ ⊢ s1' ≈⇩L s2'"
    by(auto intro:WhileLowStepInduct)
qed



text ‹and now: the main theorem:›

theorem secTypeImpliesNonInterference:
  "Γ,T ⊢ c ⟹ nonInterference Γ c"
proof (induct c arbitrary:T rule:com.induct)
  case Skip
  show ?case
  proof(rule nonInterferenceI)
    fix s1 s2 s1' s2'
    assume "Γ ⊢ s1 ≈⇩L s2" and "⟨Skip,s1⟩ →* ⟨Skip,s1'⟩" and "⟨Skip,s2⟩ →* ⟨Skip,s2'⟩"
    from ‹⟨Skip,s1⟩ →* ⟨Skip,s1'⟩› have "s1 = s1'" by(auto dest:Skip_reds)
    from ‹⟨Skip,s2⟩ →* ⟨Skip,s2'⟩› have "s2 = s2'" by(auto dest:Skip_reds)
    from ‹Γ ⊢ s1 ≈⇩L s2› and ‹s1 = s1'› and ‹s2 = s2'›
    show "Γ ⊢ s1' ≈⇩L s2'" by simp
  qed
next
  case (LAss V e)
  from ‹Γ,T ⊢ V:=e› 
  have varprem:"(Γ V = Some High) ∨ (Γ V = Some Low ∧ Γ ⊢ e : Low ∧ T = Low)"
    by (auto elim:secComTyping.cases)
  show ?case
  proof(rule nonInterferenceI)
    fix s1 s2 s1' s2'
    assume "Γ ⊢ s1 ≈⇩L s2" and "⟨V:=e,s1⟩ →* ⟨Skip,s1'⟩" and "⟨V:=e,s2⟩ →* ⟨Skip,s2'⟩"
    from ‹⟨V:=e,s1⟩ →* ⟨Skip,s1'⟩› have "s1' = s1(V:=⟦e⟧ s1)" by(auto intro:LAss_reds)
    from ‹⟨V:=e,s2⟩ →* ⟨Skip,s2'⟩› have "s2' = s2(V:=⟦e⟧ s2)" by(auto intro:LAss_reds)
    from varprem show "Γ ⊢ s1' ≈⇩L s2'"
    proof
      assume "Γ V = Some High"
      with ‹Γ ⊢ s1 ≈⇩L s2› ‹s1' = s1(V:=⟦e⟧ s1)› ‹s2' = s2(V:=⟦e⟧ s2)›
      show ?thesis by(auto intro:assignNIhighlemma)
    next
      assume "Γ V = Some Low ∧ Γ ⊢ e : Low ∧ T = Low"
      with ‹Γ ⊢ s1 ≈⇩L s2› ‹s1' = s1(V:=⟦e⟧ s1)› ‹s2' = s2(V:=⟦e⟧ s2)›
      show ?thesis by(auto intro:assignNIlowlemma)
    qed
  qed
next
  case (Seq c1 c2)
  note IH1 = ‹⋀T. Γ,T ⊢ c1 ⟹ nonInterference Γ c1›
  note IH2 = ‹⋀T. Γ,T ⊢ c2 ⟹ nonInterference Γ c2›
  show ?case
  proof (cases T)
    case High
    with ‹Γ,T ⊢ c1;;c2› have "Γ,High ⊢ c1" and "Γ,High ⊢ c2"
      by(auto elim:secComTyping.cases)
    from IH1[OF ‹Γ,High ⊢ c1›] have "nonInterference Γ c1" .
    moreover
    from IH2[OF ‹Γ,High ⊢ c2›] have "nonInterference Γ c2" .
    ultimately show ?thesis by (auto intro:SeqCompositionality)
  next
    case Low
    with ‹Γ,T ⊢ c1;;c2›
    have "(Γ,Low ⊢ c1 ∧ Γ,Low ⊢ c2) ∨ Γ,High ⊢ c1;;c2"
      by(auto elim:secComTyping.cases)
    thus ?thesis 
    proof
      assume "Γ,Low ⊢ c1 ∧ Γ,Low ⊢ c2"
      hence "Γ,Low ⊢ c1" and "Γ,Low ⊢ c2" by simp_all
      from IH1[OF ‹Γ,Low ⊢ c1›] have "nonInterference Γ c1" .
      moreover
      from IH2[OF ‹Γ,Low ⊢ c2›] have "nonInterference Γ c2" .
      ultimately show ?thesis by(auto intro:SeqCompositionality)
    next
      assume "Γ,High ⊢ c1;;c2"
      hence "Γ,High ⊢ c1" and "Γ,High ⊢ c2" by(auto elim:secComTyping.cases)
      from IH1[OF ‹Γ,High ⊢ c1›] have "nonInterference Γ c1" .
      moreover
      from IH2[OF ‹Γ,High ⊢ c2›] have "nonInterference Γ c2" .
      ultimately show ?thesis by(auto intro:SeqCompositionality)
    qed
  qed
next
  case (Cond b c1 c2)
  note IH1 = ‹⋀T. Γ,T ⊢ c1 ⟹ nonInterference Γ c1›
  note IH2 = ‹⋀T. Γ,T ⊢ c2 ⟹ nonInterference Γ c2›
  show ?case
  proof (cases T)
    case High
    with ‹Γ,T ⊢ if (b) c1 else c2› show ?thesis
      by(auto intro:CondHighCompositionality)
  next
    case Low
    with ‹Γ,T ⊢ if (b) c1 else c2› 
    have "(Γ ⊢ b : Low ∧ Γ,Low ⊢ c1 ∧Γ,Low ⊢ c2) ∨ Γ,High ⊢ if (b) c1 else c2"
      by(auto elim:secComTyping.cases)
    thus ?thesis
    proof
      assume "Γ ⊢ b : Low ∧ Γ,Low ⊢ c1 ∧ Γ,Low ⊢ c2"
      hence "Γ ⊢ b : Low" and "Γ,Low ⊢ c1" and "Γ,Low ⊢ c2" by simp_all
      from IH1[OF ‹Γ,Low ⊢ c1›] have "nonInterference Γ c1" .
      moreover
      from IH2[OF ‹Γ,Low ⊢ c2›] have "nonInterference Γ c2" .
      ultimately show ?thesis using ‹Γ ⊢ b : Low›
        by(auto intro:CondLowCompositionality)
    next
      assume "Γ,High ⊢ if (b) c1 else c2"
      thus ?thesis by(auto intro:CondHighCompositionality)
    qed
  qed
next
  case (While b c')
  note IH = ‹⋀T. Γ,T ⊢ c' ⟹ nonInterference Γ c'›
  show ?case
  proof(cases T)
    case High
    with ‹Γ,T ⊢ while (b) c'› show ?thesis by(auto intro:WhileHighCompositionality)
  next
    case Low
    with ‹Γ,T ⊢ while (b) c'› 
    have "(Γ ⊢ b : Low ∧ Γ,Low ⊢ c') ∨ Γ,High ⊢ while (b) c'"
      by(auto elim:secComTyping.cases)
    thus ?thesis
    proof
      assume "Γ ⊢ b : Low ∧ Γ,Low ⊢ c'"
      hence "Γ ⊢ b : Low" and "Γ,Low ⊢ c'" by simp_all
      moreover
      from IH[OF ‹Γ,Low ⊢ c'›] have "nonInterference Γ c'" .
      ultimately show ?thesis by(auto intro:WhileLowCompositionality)
    next
      assume "Γ,High ⊢ while (b) c'"
      thus ?thesis by(auto intro:WhileHighCompositionality)
    qed
  qed
qed

end