Theory Analysis_Tainting

theory Analysis_Tainting
imports SINVAR_Tainting SINVAR_BLPbasic
        SINVAR_TaintingTrusted SINVAR_BLPtrusted
begin

term SINVAR_Tainting.sinvar
term SINVAR_BLPbasic.sinvar


lemma tainting_imp_blp_cutcard: "∀ts v. nP v = ts ⟶ finite ts ⟹
  SINVAR_Tainting.sinvar G nP ⟹ SINVAR_BLPbasic.sinvar G ((λts. card (ts ∩ X)) ∘ nP)"
apply(simp add: SINVAR_Tainting.sinvar_def)
apply(clarify, rename_tac a b)
apply(erule_tac x="(a,b)" in ballE)
 apply(simp_all)
apply(subgoal_tac "finite (nP a ∩ X)")
 prefer 2 subgoal using finite_Int by blast
apply(subgoal_tac "finite (nP b ∩ X)")
 prefer 2 subgoal using finite_Int by blast
using card_mono by (metis Int_subset_iff order_refl subset_antisym)

lemma tainting_imp_blp_cutcard2: "finite X ⟹
  SINVAR_Tainting.sinvar G nP ⟹ SINVAR_BLPbasic.sinvar G ((λts. card (ts ∩ X)) ∘ nP)"
apply(simp add: SINVAR_Tainting.sinvar_def)
apply(clarify, rename_tac a b)
apply(erule_tac x="(a,b)" in ballE)
 apply(simp_all)
apply(subgoal_tac "finite (nP a ∩ X)")
 prefer 2 subgoal using finite_Int by blast
apply(subgoal_tac "finite (nP b ∩ X)")
 prefer 2 subgoal using finite_Int by blast
using card_mono by (metis Int_subset_iff order_refl subset_antisym)

lemma "∀ts v. nP v = ts ⟶ finite ts ⟹
  SINVAR_Tainting.sinvar G nP ⟹ SINVAR_BLPbasic.sinvar G (card ∘ nP)"
apply(drule(1) tainting_imp_blp_cutcard[where X=UNIV])
by(simp)


(*Stronger version*)
lemma "∀b ∈ snd ` edges G. finite (nP b) ⟹
  SINVAR_Tainting.sinvar G nP ⟹ SINVAR_BLPbasic.sinvar G (card ∘ nP)"
apply(simp add: SINVAR_Tainting.sinvar_def)
apply(clarify, rename_tac a b)
apply(erule_tac x="(a,b)" in ballE)
 apply(simp_all)
apply(case_tac "finite (nP a)")
 apply(case_tac [!] "finite (nP b)")
   using card_mono apply blast
  apply(simp_all)
done


text‹One tainting invariant is equal to many BLP invariants. 
     The BLP invariants are the projection of the tainting mapping for exactly one label›
lemma tainting_iff_blp:
  defines "extract ≡ λa ts. if a ∈ ts then 1::security_level else 0::security_level"
  shows "SINVAR_Tainting.sinvar G nP ⟷ (∀a. SINVAR_BLPbasic.sinvar G (extract a ∘ nP))"
proof
  show"SINVAR_Tainting.sinvar G nP ⟹ ∀a. SINVAR_BLPbasic.sinvar G (extract a ∘ nP)"
    apply(simp add: extract_def)
    apply(safe)
     apply simp
    apply(simp add: SINVAR_Tainting.sinvar_def)
    by fast
  next
    assume blp: "∀a. SINVAR_BLPbasic.sinvar G (extract a ∘ nP)"
    { fix v1 v2
      assume *: "(v1,v2)∈edges G"
      { fix a
        from blp * have "(if a ∈ nP v1 then 1::security_level else 0) ≤ (if a ∈ nP v2 then 1 else 0)"
          unfolding extract_def
          apply(simp)
          apply(erule_tac x=a in allE)
          apply(erule_tac x="(v1, v2)" in ballE)
           apply(simp_all)
          apply(simp split: if_split_asm)
          done
        hence "a ∈ nP v1 ⟹ a ∈ nP v2" by(simp split: if_split_asm)
      }
      from this have "nP v1 ⊆ nP v2" by auto
    }
    thus "SINVAR_Tainting.sinvar G nP" unfolding SINVAR_Tainting.sinvar_def by blast
qed


text‹If the labels are finite, the above can be generalized to arbitrary subsets of tainting labels.›
lemma tainting_iff_blp_extended:
  defines "extract ≡ λA ts. card (A ∩ ts)"
  assumes finite: "∀ts v. nP v = ts ⟶ finite ts"
  shows "SINVAR_Tainting.sinvar G nP ⟷ (∀A. SINVAR_BLPbasic.sinvar G (extract A ∘ nP))"
proof
  show "SINVAR_Tainting.sinvar G nP ⟹ ∀A. SINVAR_BLPbasic.sinvar G (extract A ∘ nP)"
    apply(simp add: extract_def)
    apply(safe)
    apply(simp add: SINVAR_Tainting.sinvar_def)
    apply(rename_tac A a b)
    apply(subgoal_tac "finite (A ∩ nP a)")
     prefer 2 subgoal using finite by blast
    apply(rule card_mono)
     apply(simp add: finite; fail)
    by blast
  next
    assume blp: "∀A. SINVAR_BLPbasic.sinvar G (extract A ∘ nP)"
    { fix v1 v2
      assume *: "(v1,v2)∈edges G"
      { fix A
        from blp * have "card (A ∩ nP v1) ≤ card (A ∩ nP v2)"
          unfolding extract_def
          apply(clarsimp)
          apply(erule_tac x=A in allE)
          apply(erule_tac x="(v1, v2)" in ballE)
           by(simp_all)
      }
      from this finite card_seteq have "nP v1 ⊆ nP v2" by (metis Int_absorb Int_lower1 inf.orderI) 
    }
    thus "SINVAR_Tainting.sinvar G nP" unfolding SINVAR_Tainting.sinvar_def by blast
qed


text‹
  Translated to the Bell LaPadula model with trust:
  security level is the number of tainted minus the untainted things
  We set the Trusted flag if a machine untaints things.
›
lemma "∀ts v. nP v = ts ⟶ finite (taints ts) ⟹
  SINVAR_TaintingTrusted.sinvar G nP ⟹
    SINVAR_BLPtrusted.sinvar G ((λ ts. ⦇security_level = card (taints ts - untaints ts), trusted = (untaints ts ≠ {})⦈ ) ∘ nP)"
apply(simp add: SINVAR_TaintingTrusted.sinvar_def)
apply(clarify, rename_tac a b)
apply(erule_tac x="(a,b)" in ballE)
 apply(simp_all)
apply(subgoal_tac "finite (taints (nP a) - untaints (nP a))")
 prefer 2 subgoal by blast
apply(rule card_mono)
 by blast+

lemma tainting_iff_blp_trusted:
  defines "project ≡ λa ts. ⦇
      security_level =
        if
          a ∈ (taints ts - untaints ts)
        then
          1::security_level
        else
          0::security_level
      , trusted = a ∈ untaints ts⦈"
  shows "SINVAR_TaintingTrusted.sinvar G nP ⟷ (∀a. SINVAR_BLPtrusted.sinvar G (project a ∘ nP))"
unfolding project_def
apply(rule iffI)
 subgoal
 apply(simp add: SINVAR_TaintingTrusted.sinvar_def)
 apply(clarify, rename_tac a b)
 apply(erule_tac x="(a,b)" in ballE)
  apply(simp_all)
 by blast
apply(simp)
apply(simp add: SINVAR_TaintingTrusted.sinvar_def)
apply(clarify, rename_tac a b taintlabel)
apply(erule_tac x=taintlabel in allE)
apply(erule_tac x="(a,b)" in ballE)
 apply(simp_all)
apply(simp split: if_split_asm)
using taints_wellformedness by blast




text‹If the labels are finite, the above can be generalized to arbitrary subsets of tainting labels.›
lemma tainting_iff_blp_trusted_extended:
  defines "project ≡ λA ts.
      ⦇
          security_level = card (A ∩ (taints ts - untaints ts))
        , trusted = (A ∩ untaints ts) ≠ {}
      ⦈"
  assumes finite: "∀ts v. nP v = ts ⟶ finite (taints ts)"
  shows "SINVAR_TaintingTrusted.sinvar G nP ⟷ (∀A. SINVAR_BLPtrusted.sinvar G (project A ∘ nP))"
unfolding project_def
apply(rule iffI)
 subgoal
 apply(simp add: SINVAR_TaintingTrusted.sinvar_def)
 apply(clarify, rename_tac a b)
 apply(erule_tac x="(a,b)" in ballE)
  apply(simp_all)
 apply(rule card_mono)
  using finite apply blast
 by blast
apply(simp)
apply(simp add: SINVAR_TaintingTrusted.sinvar_def)
apply(clarify, rename_tac a b taintlabel)
apply(erule_tac x="{taintlabel}" in allE)
apply(erule_tac x="(a,b)" in ballE)
 apply(simp_all)
apply(simp split: if_split_asm)
 using taints_wellformedness apply blast
using Diff_insert_absorb by fastforce


end