Theory BasicSecurityPredicates

theory BasicSecurityPredicates
imports Views "../Basics/Projection"
begin

(*Auxiliary predicate capturing that a a set of traces consists 
only of traces of a given set of events *)
definition areTracesOver :: "('e list) set ⇒ 'e set ⇒ bool "
where
"areTracesOver Tr E ≡ 
  ∀ τ ∈ Tr. (set τ) ⊆ E"



(* Basic Security Predicates are properties of sets of traces
 that are parameterized with a view *)
type_synonym 'e BSP = "'e V_rec ⇒ (('e list) set) ⇒ bool"

(* Basic Security Predicates are valid if and only if they are closure property of sets of traces 
for arbitrary views and sets of traces *)
definition BSP_valid :: "'e BSP ⇒ bool"
where 
"BSP_valid bsp ≡ 
  ∀𝒱 Tr E. ( isViewOn 𝒱 E ∧ areTracesOver Tr E ) 
              ⟶ (∃ Tr'. Tr' ⊇ Tr  ∧ bsp 𝒱 Tr')"

(* Removal of Confidential Events (R) *)
definition R :: "'e BSP"
where
"R 𝒱 Tr ≡ 
  ∀τ∈Tr. ∃τ'∈Tr. τ' ↿ C⇘𝒱⇙ = [] ∧ τ' ↿ V⇘𝒱⇙ = τ ↿ V⇘𝒱⇙"

lemma BSP_valid_R: "BSP_valid R" 
proof -
  {  
    fix 𝒱::"('e V_rec)" 
    fix Tr E
    assume "isViewOn 𝒱 E"
    and "areTracesOver Tr E"     
    let ?Tr'="{t. (set t) ⊆ E}"
    have "?Tr'⊇ Tr" 
      by (meson Ball_Collect ‹areTracesOver Tr E› areTracesOver_def)
    moreover
    have "R 𝒱 ?Tr'" 
      proof -
        {
          fix τ
          assume "τ ∈ {t. (set t) ⊆ E}"
          let ?τ'="τ↿(V⇘𝒱⇙)"
          have "?τ' ↿ C⇘𝒱⇙ = []  ∧ ?τ' ↿ V⇘𝒱⇙ = τ ↿ V⇘𝒱⇙" 
            using ‹isViewOn 𝒱 E›  disjoint_projection projection_idempotent 
            unfolding isViewOn_def V_valid_def VC_disjoint_def  by metis
          moreover
          from ‹τ ∈ {t. (set t) ⊆ E}› have "?τ' ∈ ?Tr'" using ‹isViewOn 𝒱 E›
            unfolding isViewOn_def
            by (simp add: list_subset_iff_projection_neutral projection_commute) 
          ultimately 
          have " ∃τ'∈{t. set t ⊆ E}. τ' ↿ C⇘𝒱⇙ = [] ∧ τ' ↿ V⇘𝒱⇙ = τ ↿ V⇘𝒱⇙" 
            by auto
        }
        thus ?thesis unfolding R_def
          by auto
      qed  
    ultimately
    have  "∃ Tr'. Tr' ⊇ Tr  ∧ R 𝒱 Tr'"
      by auto
  }
  thus ?thesis 
    unfolding BSP_valid_def by auto
qed
    
(* Deletion of Confidential Events (D) *)
definition D :: "'e BSP"
where
"D 𝒱 Tr ≡ 
  ∀α β. ∀c∈C⇘𝒱⇙. ((β @ [c] @ α) ∈ Tr ∧ α↿C⇘𝒱⇙ = []) 
    ⟶ (∃α' β'. ((β' @ α') ∈ Tr ∧ α'↿V⇘𝒱⇙ = α↿V⇘𝒱⇙ ∧ α'↿C⇘𝒱⇙ = []
                  ∧ β'↿(V⇘𝒱⇙ ∪ C⇘𝒱⇙) = β↿(V⇘𝒱⇙ ∪ C⇘𝒱⇙)))"

lemma BSP_valid_D: "BSP_valid D"
proof -
  {  
    fix 𝒱::"('e V_rec)" 
    fix Tr E
    assume "isViewOn 𝒱 E"
    and "areTracesOver Tr E"     
    let ?Tr'="{t. (set t) ⊆ E}"
    have "?Tr'⊇ Tr" 
      by (meson Ball_Collect ‹areTracesOver Tr E› areTracesOver_def)
    moreover
    have "D 𝒱 ?Tr'"
      unfolding D_def by auto
    ultimately
    have  "∃ Tr'. Tr' ⊇ Tr  ∧ D 𝒱 Tr'" 
      by auto
  }
  thus ?thesis 
    unfolding BSP_valid_def by auto
qed

(* Insertion of Confidential Events (I) *)
definition I :: "'e BSP"
where
"I 𝒱 Tr ≡ 
  ∀α β. ∀c∈C⇘𝒱⇙. ((β @ α) ∈ Tr ∧ α↿C⇘𝒱⇙ = []) 
    ⟶ (∃α' β'. ((β' @ [c] @ α') ∈ Tr ∧ α'↿V⇘𝒱⇙ = α↿V⇘𝒱⇙ ∧ α'↿C⇘𝒱⇙ = []
                     ∧ β'↿(V⇘𝒱⇙ ∪ C⇘𝒱⇙) = β↿(V⇘𝒱⇙ ∪ C⇘𝒱⇙)))"

lemma BSP_valid_I: "BSP_valid I"
proof -
  {  
    fix 𝒱::"('e V_rec)" 
    fix Tr E
    assume "isViewOn 𝒱 E"
    and "areTracesOver Tr E"     
    let ?Tr'="{t. (set t) ⊆ E}"
    have "?Tr'⊇ Tr"
      by (meson Ball_Collect ‹areTracesOver Tr E› areTracesOver_def)
    moreover
    have "I 𝒱 ?Tr'" using ‹isViewOn 𝒱 E› 
      unfolding isViewOn_def I_def by auto
    ultimately
    have  "∃ Tr'. Tr' ⊇ Tr  ∧ I 𝒱 Tr'"
      by auto
  }
  thus ?thesis
    unfolding BSP_valid_def by auto
qed


(* ρ-Admissibility *)
type_synonym 'e Rho = "'e V_rec ⇒ 'e set"

definition 
Adm :: "'e V_rec ⇒ 'e Rho ⇒ ('e list) set ⇒ 'e list ⇒ 'e ⇒ bool"
where 
"Adm 𝒱 ρ Tr β e ≡
   ∃γ. ((γ @ [e]) ∈ Tr ∧ γ↿(ρ 𝒱) = β↿(ρ 𝒱))"

(* Insertion of Admissible Confidential Events (IA) *)
definition IA :: "'e Rho ⇒ 'e BSP"
where
"IA ρ 𝒱 Tr ≡ 
  ∀α β. ∀c∈C⇘𝒱⇙. ((β @ α) ∈ Tr ∧ α↿C⇘𝒱⇙ = [] ∧ (Adm 𝒱 ρ Tr β c)) 
    ⟶ (∃ α' β'. ((β' @ [c] @ α') ∈ Tr) ∧ α'↿V⇘𝒱⇙ = α↿V⇘𝒱⇙ 
                    ∧ α'↿C⇘𝒱⇙ = [] ∧ β'↿(V⇘𝒱⇙ ∪ C⇘𝒱⇙) = β↿(V⇘𝒱⇙ ∪ C⇘𝒱⇙))" 

lemma BSP_valid_IA: "BSP_valid (IA ρ) "
proof -
  {  
    fix 𝒱 :: "('a V_rec)"
    fix Tr E
    assume "isViewOn 𝒱 E"
    and "areTracesOver Tr E"     
    let ?Tr'="{t. (set t) ⊆ E}"
    have "?Tr'⊇ Tr"
      by (meson Ball_Collect ‹areTracesOver Tr E› areTracesOver_def)
    moreover
    have "IA ρ 𝒱 ?Tr'" using ‹isViewOn 𝒱 E›
      unfolding isViewOn_def IA_def by auto
    ultimately
    have  "∃ Tr'. Tr' ⊇ Tr  ∧ IA ρ 𝒱 Tr'"
      by auto
  }
  thus ?thesis
    unfolding BSP_valid_def by auto
qed


(* Backwards Strict Deletion of Confidential Events (BSD) *)
definition BSD :: "'e BSP"
where
"BSD 𝒱 Tr ≡ 
  ∀α β. ∀c∈C⇘𝒱⇙. ((β @ [c] @ α) ∈ Tr ∧ α↿C⇘𝒱⇙ = []) 
    ⟶ (∃α'. ((β @ α') ∈ Tr ∧ α'↿V⇘𝒱⇙ = α↿V⇘𝒱⇙ ∧ α'↿C⇘𝒱⇙ = []))"

lemma BSP_valid_BSD: "BSP_valid BSD"
proof -
  {  
    fix 𝒱::"('e V_rec)" 
    fix Tr E
    assume "isViewOn 𝒱 E"
    and "areTracesOver Tr E"     
    let ?Tr'="{t. (set t) ⊆ E}"
    have "?Tr'⊇ Tr"
      by (meson Ball_Collect ‹areTracesOver Tr E› areTracesOver_def)
    moreover
    have "BSD 𝒱 ?Tr'"
      unfolding BSD_def by auto
    ultimately
    have  "∃ Tr'. Tr' ⊇ Tr  ∧ BSD 𝒱 Tr'"
      by auto
  }
  thus ?thesis
    unfolding BSP_valid_def by auto
qed

(* Backwards Strict Insertion of Confidential Events (BSI) *)
definition BSI :: "'e BSP"
where
"BSI 𝒱 Tr ≡ 
  ∀α β. ∀c∈C⇘𝒱⇙. ((β @ α) ∈ Tr ∧ α↿C⇘𝒱⇙ = []) 
    ⟶ (∃α'. ((β @ [c] @ α') ∈ Tr ∧ α'↿V⇘𝒱⇙ = α↿V⇘𝒱⇙ ∧ α'↿C⇘𝒱⇙ = []))"

lemma BSP_valid_BSI: "BSP_valid BSI"
proof -
  {  
    fix 𝒱::"('e V_rec)" 
    fix Tr E
    assume "isViewOn 𝒱 E"
    and "areTracesOver Tr E"     
    let ?Tr'="{t. (set t) ⊆ E}"
    have "?Tr'⊇ Tr"
      by (meson Ball_Collect ‹areTracesOver Tr E› areTracesOver_def)
    moreover
    have "BSI 𝒱 ?Tr'" using ‹isViewOn 𝒱 E›
      unfolding isViewOn_def BSI_def by auto
    ultimately
    have  "∃ Tr'. Tr' ⊇ Tr  ∧ BSI 𝒱 Tr'"
      by auto
  }
  thus ?thesis
    unfolding BSP_valid_def by auto
qed

(* Backwards Strict Insertion of Admissible Confidential Events (BSIA) *)
definition BSIA :: "'e Rho ⇒ 'e BSP"
where 
"BSIA ρ 𝒱 Tr ≡ 
  ∀α β. ∀c∈C⇘𝒱⇙. ((β @ α) ∈ Tr ∧ α↿C⇘𝒱⇙ = [] ∧ (Adm 𝒱 ρ Tr β c)) 
    ⟶ (∃α'. ((β @ [c] @ α') ∈ Tr ∧ α'↿V⇘𝒱⇙ = α↿V⇘𝒱⇙ ∧ α'↿C⇘𝒱⇙ = []))"

lemma BSP_valid_BSIA: "BSP_valid (BSIA ρ) "
proof -
  {  
    fix 𝒱 :: "('a V_rec)"
    fix Tr E
    assume "isViewOn 𝒱 E"
    and "areTracesOver Tr E"     
    let ?Tr'="{t. (set t) ⊆ E}"
    have "?Tr'⊇ Tr"
      by (meson Ball_Collect ‹areTracesOver Tr E› areTracesOver_def)
    moreover
    have "BSIA ρ 𝒱 ?Tr'" using ‹isViewOn 𝒱 E›
      unfolding isViewOn_def BSIA_def by auto
    ultimately
    have  "∃ Tr'. Tr' ⊇ Tr  ∧ BSIA ρ 𝒱 Tr'"
      by auto
  }
  thus ?thesis
    unfolding BSP_valid_def by auto
qed

(* Forward Correctable BSPs *)
record 'e Gamma =
  Nabla :: "'e set"
  Delta :: "'e set"
  Upsilon :: "'e set"

(* syntax abbreviations for Gamma *)
abbreviation GammaNabla :: "'e Gamma ⇒ 'e set"
(‹∇⇘_⇙› [100] 1000)
where
"∇⇘Γ⇙ ≡ (Nabla Γ)"

abbreviation GammaDelta :: "'e Gamma ⇒ 'e set"
(‹Δ⇘_⇙› [100] 1000)
where
"Δ⇘Γ⇙ ≡ (Delta Γ)"

abbreviation GammaUpsilon :: "'e Gamma ⇒ 'e set"
(‹Υ⇘_⇙› [100] 1000)
where
"Υ⇘Γ⇙ ≡ (Upsilon Γ)"


(* Forward Correctable Deletion of Confidential Events (FCD) *)
definition FCD :: "'e Gamma ⇒ 'e BSP"
where
"FCD Γ 𝒱 Tr ≡ 
  ∀α β. ∀c∈(C⇘𝒱⇙ ∩ Υ⇘Γ⇙). ∀v∈(V⇘𝒱⇙ ∩ ∇⇘Γ⇙). 
    ((β @ [c,v] @ α) ∈ Tr ∧ α ↿ C⇘𝒱⇙ = []) 
      ⟶ (∃α'. ∃δ'. (set δ') ⊆ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙) 
                      ∧ ((β @ δ' @ [v] @ α') ∈ Tr  
                      ∧ α'↿V⇘𝒱⇙ = α↿V⇘𝒱⇙ ∧ α'↿C⇘𝒱⇙ = []))"

lemma BSP_valid_FCD: "BSP_valid (FCD Γ)"
proof -
  {  
    fix 𝒱::"('a V_rec)" 
    fix Tr E
    assume "isViewOn 𝒱 E"
    and "areTracesOver Tr E"     
    let ?Tr'="{t. (set t) ⊆ E}"
    have "?Tr'⊇ Tr" 
      by (meson Ball_Collect ‹areTracesOver Tr E› areTracesOver_def)
    moreover
    have "FCD Γ 𝒱 ?Tr'"
      proof -
        {
          fix α β c v
          assume  "c ∈ C⇘𝒱⇙ ∩ Υ⇘Γ⇙"
             and  "v ∈V⇘𝒱⇙ ∩ ∇⇘Γ⇙"
             and  "β @ [c ,v] @ α ∈ ?Tr'"
             and  "α ↿ C⇘𝒱⇙ = []"
          let ?α'="α" and ?δ'="[]"  
          from ‹β @ [c ,v] @ α ∈ ?Tr'› have "β @ ?δ' @ [v] @ ?α' ∈ ?Tr'"
            by auto 
          hence  "(set ?δ') ⊆ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙) ∧ ((β @ ?δ' @ [v] @ ?α') ∈ ?Tr'  
                      ∧ ?α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙ ∧ ?α' ↿ C⇘𝒱⇙ = [])"   
            using ‹isViewOn 𝒱 E› ‹α ↿ C⇘𝒱⇙ = []› 
            unfolding isViewOn_def ‹α ↿ C⇘𝒱⇙ = []› by auto
          hence "∃α'. ∃δ'. (set δ') ⊆ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙) ∧ ((β @ δ' @ [v] @ α') ∈ ?Tr'  
            ∧ α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙ ∧ α' ↿ C⇘𝒱⇙ = [])"
            by blast
        }
        thus ?thesis
          unfolding FCD_def by auto 
      qed
    ultimately
    have  "∃ Tr'. Tr' ⊇ Tr  ∧ FCD Γ 𝒱 Tr'"
      by auto
  }
  thus ?thesis
    unfolding BSP_valid_def by auto
qed

(* Forward Correctable Insertion of Confidential Events (FCI) *)
definition FCI :: "'e Gamma ⇒ 'e BSP"
where
"FCI Γ 𝒱 Tr ≡ 
  ∀α β. ∀c∈(C⇘𝒱⇙ ∩ Υ⇘Γ⇙). ∀v∈(V⇘𝒱⇙ ∩ ∇⇘Γ⇙). 
    ((β @ [v] @ α) ∈ Tr ∧ α↿C⇘𝒱⇙ = []) 
      ⟶ (∃α'. ∃δ'. (set δ') ⊆ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙) 
                      ∧ ((β @ [c] @ δ' @ [v] @ α') ∈ Tr  
                      ∧ α'↿V⇘𝒱⇙ = α↿V⇘𝒱⇙ ∧ α'↿C⇘𝒱⇙ = []))"

lemma BSP_valid_FCI: "BSP_valid (FCI Γ)"
proof -
  {  
    fix 𝒱::"('a V_rec)" 
    fix Tr E
    assume "isViewOn 𝒱 E"
    and "areTracesOver Tr E"     
    let ?Tr'="{t. (set t) ⊆ E}"
    have "?Tr'⊇ Tr" 
      by (meson Ball_Collect ‹areTracesOver Tr E› areTracesOver_def)
    moreover
    have "FCI Γ 𝒱 ?Tr'"
      proof -
        {
          fix α β c v
          assume  "c ∈ C⇘𝒱⇙ ∩ Υ⇘Γ⇙"
             and  "v ∈V⇘𝒱⇙ ∩ ∇⇘Γ⇙"
             and  "β @ [v] @ α ∈ ?Tr'"
             and  "α ↿ C⇘𝒱⇙ = []"
          let ?α'="α" and ?δ'="[]"  
          from ‹c ∈ C⇘𝒱⇙ ∩ Υ⇘Γ⇙› have" c ∈ E" 
            using ‹isViewOn 𝒱 E›
            unfolding isViewOn_def by auto
          with  ‹β @ [v] @ α ∈ ?Tr'› have "β @ [c] @ ?δ' @ [v] @ ?α' ∈ ?Tr'" 
            by auto 
          hence  "(set ?δ') ⊆ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙) ∧ ((β @ [c] @ ?δ' @ [v] @ ?α') ∈ ?Tr'  
                      ∧ ?α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙ ∧ ?α' ↿ C⇘𝒱⇙ = [])"   
           using ‹isViewOn 𝒱 E› ‹α ↿ C⇘𝒱⇙ = []›  unfolding isViewOn_def ‹α ↿ C⇘𝒱⇙ = []› by auto
         hence 
           "∃α'. ∃δ'. (set δ') ⊆ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙) ∧ ((β @ [c] @ δ' @ [v] @ α') ∈ ?Tr'  
            ∧ α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙ ∧ α' ↿ C⇘𝒱⇙ = [])" 
            by blast
        }
        thus ?thesis
          unfolding FCI_def by auto 
      qed
    ultimately
    have  "∃ Tr'. Tr' ⊇ Tr  ∧ FCI Γ 𝒱 Tr'" 
      by auto
  }
  thus ?thesis 
    unfolding BSP_valid_def by auto
qed

(* Forward correctable Insertion of Admissible Confidential Events (FCIA) *)
definition FCIA :: "'e Rho ⇒ 'e Gamma ⇒ 'e BSP"
where
"FCIA ρ Γ 𝒱 Tr ≡ 
  ∀α β. ∀c∈(C⇘𝒱⇙ ∩ Υ⇘Γ⇙). ∀v∈(V⇘𝒱⇙ ∩ ∇⇘Γ⇙).
    ((β @ [v] @ α) ∈ Tr ∧ α↿C⇘𝒱⇙ = [] ∧ (Adm 𝒱 ρ Tr β c)) 
      ⟶ (∃α'. ∃δ'. (set δ') ⊆ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙) 
                      ∧ ((β @ [c] @ δ' @ [v] @ α') ∈ Tr  
                      ∧ α'↿V⇘𝒱⇙ = α↿V⇘𝒱⇙ ∧ α'↿C⇘𝒱⇙ = []))"

lemma BSP_valid_FCIA: "BSP_valid (FCIA ρ Γ) "
proof -
  {  
    fix 𝒱 :: "('a V_rec)"
    fix Tr E
    assume "isViewOn 𝒱 E"
    and "areTracesOver Tr E"     
    let ?Tr'="{t. (set t) ⊆ E}"
    have "?Tr'⊇ Tr"
      by (meson Ball_Collect ‹areTracesOver Tr E› areTracesOver_def)
    moreover
    have "FCIA ρ Γ 𝒱 ?Tr'"
    proof -
        {
          fix α β c v
          assume  "c ∈ C⇘𝒱⇙ ∩ Υ⇘Γ⇙"
             and  "v ∈V⇘𝒱⇙ ∩ ∇⇘Γ⇙"
             and  "β @ [v] @ α ∈ ?Tr'"
             and  "α ↿ C⇘𝒱⇙ = []"
          let ?α'="α" and ?δ'="[]"  
          from ‹c ∈ C⇘𝒱⇙ ∩ Υ⇘Γ⇙› have" c ∈ E" 
            using ‹isViewOn 𝒱 E› unfolding isViewOn_def by auto
          with  ‹β @ [v] @ α ∈ ?Tr'› have "β @ [c] @ ?δ' @ [v] @ ?α' ∈ ?Tr'"
            by auto 
          hence  "(set ?δ') ⊆ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙) ∧ ((β @ [c] @ ?δ' @ [v] @ ?α') ∈ ?Tr'  
                      ∧ ?α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙ ∧ ?α' ↿ C⇘𝒱⇙ = [])"   
            using ‹isViewOn 𝒱 E› ‹α ↿ C⇘𝒱⇙ = []›  
            unfolding isViewOn_def ‹α ↿ C⇘𝒱⇙ = []› by auto
          hence 
            "∃α'. ∃δ'. (set δ') ⊆ (N⇘𝒱⇙ ∩ Δ⇘Γ⇙) ∧ ((β @ [c] @ δ' @ [v] @ α') ∈ ?Tr'  
            ∧ α' ↿ V⇘𝒱⇙ = α ↿ V⇘𝒱⇙ ∧ α' ↿ C⇘𝒱⇙ = [])" 
            by blast
        }
        thus ?thesis
          unfolding FCIA_def by auto 
      qed
    ultimately
    have  "∃ Tr'. Tr' ⊇ Tr  ∧ FCIA ρ Γ 𝒱 Tr'"
      by auto
  }
  thus ?thesis
    unfolding BSP_valid_def by auto
qed

(* Strict Removal of Confidential Events (SR) *)
definition SR :: "'e BSP"
where
"SR 𝒱 Tr ≡ ∀τ∈Tr. τ ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) ∈ Tr"

lemma "BSP_valid SR"
proof -
  {  
    fix 𝒱::"('e V_rec)" 
    fix Tr E
    assume "isViewOn 𝒱 E"
    and "areTracesOver Tr E"     
    let ?Tr'="{t. ∃τ ∈ Tr. t=τ↿(V⇘𝒱⇙ ∪ N⇘𝒱⇙)} ∪ Tr"
    have "?Tr'⊇ Tr" 
      by blast
    moreover
    have "SR 𝒱 ?Tr'" unfolding SR_def 
      proof
        fix τ
        assume "τ ∈ ?Tr'"
        {
          from ‹τ ∈ ?Tr'› have "(∃t∈Tr. τ = t ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)) ∨ τ ∈ Tr"
            by auto
          hence "τ ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) ∈ ?Tr'" 
            proof 
              assume "∃t∈Tr. τ = t ↿(V⇘𝒱⇙ ∪ N⇘𝒱⇙)" 
              hence "∃t∈Tr. τ ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙)= t ↿(V⇘𝒱⇙ ∪ N⇘𝒱⇙)" 
                using projection_idempotent by metis
              thus ?thesis 
                by auto
            next
              assume "τ ∈ Tr" 
              thus ?thesis 
                by auto
            qed  
        }  
        thus "τ ↿ (V⇘𝒱⇙ ∪ N⇘𝒱⇙) ∈ ?Tr'" 
          by auto
      qed
    ultimately
    have "∃ Tr'. Tr' ⊇ Tr  ∧ SR 𝒱 Tr'" 
      by auto
  }
  thus ?thesis 
    unfolding BSP_valid_def by auto
qed

(* Strict Deletion of Confidential Events (SD) *)
definition SD :: "'e BSP"
where
"SD 𝒱 Tr ≡ 
  ∀α β. ∀c∈C⇘𝒱⇙. ((β @ [c] @ α) ∈ Tr ∧ α↿C⇘𝒱⇙ = []) ⟶ β @ α ∈ Tr"

lemma "BSP_valid SD"
proof -
  {  
    fix 𝒱::"('e V_rec)" 
    fix Tr E
    assume "isViewOn 𝒱 E"
    and "areTracesOver Tr E"     
    let ?Tr'="{t. (set t) ⊆ E}"
    have "?Tr'⊇ Tr" by (meson Ball_Collect ‹areTracesOver Tr E› areTracesOver_def)
    moreover
    have "SD 𝒱 ?Tr'" unfolding SD_def by auto
    ultimately
    have  "∃ Tr'. Tr' ⊇ Tr  ∧ SD 𝒱 Tr'" by auto
  }
  thus ?thesis unfolding BSP_valid_def by auto
qed
 
(* Strict Insertion of Confidential Events (SI) *)
definition SI :: "'e BSP"
where
"SI 𝒱 Tr ≡ 
  ∀α β. ∀c∈C⇘𝒱⇙. ((β @ α) ∈ Tr ∧ α ↿ C⇘𝒱⇙ = []) ⟶ β @ [c] @ α ∈ Tr"

lemma "BSP_valid SI"
proof -
  {  
    fix 𝒱::"('a V_rec)" 
    fix Tr E
    assume "isViewOn 𝒱 E"
    and "areTracesOver Tr E"     
    let ?Tr'="{t. (set t) ⊆ E}"
    have "?Tr'⊇ Tr"
      by (meson Ball_Collect ‹areTracesOver Tr E› areTracesOver_def)
    moreover
    have "SI 𝒱 ?Tr'" 
      using ‹isViewOn 𝒱 E› 
      unfolding isViewOn_def SI_def by auto
    ultimately
    have  "∃ Tr'. Tr' ⊇ Tr  ∧ SI 𝒱 Tr'" 
      by auto
  }
  thus ?thesis 
    unfolding BSP_valid_def by auto
qed

(* Strict Insertion of Admissible Confidential Events (SIA) *)
definition SIA :: "'e Rho ⇒ 'e BSP"
where
"SIA ρ 𝒱 Tr ≡ 
  ∀α β. ∀c∈C⇘𝒱⇙. ((β @ α) ∈ Tr ∧ α ↿ C⇘𝒱⇙ = [] ∧ (Adm 𝒱 ρ Tr β c)) 
    ⟶ (β @ [c] @ α) ∈ Tr" 

lemma "BSP_valid (SIA ρ) "
proof -
  {  
    fix 𝒱 :: "('a V_rec)"
    fix Tr E
    assume "isViewOn 𝒱 E"
    and "areTracesOver Tr E"     
    let ?Tr'="{t. (set t) ⊆ E}"
    have "?Tr'⊇ Tr" 
      by (meson Ball_Collect ‹areTracesOver Tr E› areTracesOver_def)
    moreover
    have "SIA ρ 𝒱 ?Tr'" 
      using ‹isViewOn 𝒱 E› 
      unfolding isViewOn_def SIA_def by auto
    ultimately
    have  "∃ Tr'. Tr' ⊇ Tr  ∧ SIA ρ 𝒱 Tr'" 
      by auto
  }
  thus ?thesis 
    unfolding BSP_valid_def by auto
qed

end