Theory PropertyLibrary

theory PropertyLibrary
imports InformationFlowProperties "../SystemSpecification/EventSystems" "../Verification/Basics/BSPTaxonomy"
begin

(* The following properties assume a partition of the
event set into a set of low events (L) and a set of high
events (H), where low events are visible *)
definition 
HighInputsConfidential :: "'e set ⇒ 'e set ⇒ 'e set ⇒ 'e V_rec"
where 
"HighInputsConfidential L H IE ≡ ⦇ V=L, N=H-IE, C=H ∩ IE ⦈"

definition HighConfidential :: "'e set ⇒ 'e set ⇒ 'e V_rec"
where 
"HighConfidential L H ≡ ⦇ V=L, N={}, C=H ⦈"

fun interleaving :: "'e list ⇒ 'e list ⇒ ('e list) set"
where
"interleaving t1 [] = {t1}" |
"interleaving [] t2 = {t2}" | 
"interleaving (e1 # t1) (e2 # t2) = 
  {t. (∃t'. t=(e1 # t') ∧ t' ∈ interleaving t1 (e2 #t2))}
  ∪ {t. (∃t'. t=(e2 # t') ∧ t' ∈ interleaving (e1 # t1) t2)}"


(* Generalized Noninterference [McC87] *)
(* MAKS representation *)
definition GNI :: "'e set ⇒ 'e set ⇒ 'e set ⇒ 'e IFP_type"
where 
"GNI L H IE ≡ ( {HighInputsConfidential L H IE}, {BSD, BSI})"

lemma GNI_valid: "L ∩ H = {} ⟹ IFP_valid (L ∪ H) (GNI L H IE)"
  unfolding IFP_valid_def GNI_def HighInputsConfidential_def isViewOn_def 
    V_valid_def VN_disjoint_def VC_disjoint_def NC_disjoint_def
  using BasicSecurityPredicates.BSP_valid_BSD BasicSecurityPredicates.BSP_valid_BSI 
  by auto
    
(* Literature representation *)
definition litGNI :: "'e set ⇒ 'e set ⇒ 'e set ⇒ ('e list) set ⇒ bool"
where 
"litGNI L H IE Tr ≡ 
  ∀ t1 t2 t3. 
    t1 @ t2 ∈ Tr ∧ t3 ↿ (L ∪ (H - IE)) = t2 ↿ (L ∪ (H - IE))
     ⟶ (∃ t4. t1 @ t4 ∈ Tr ∧ t4↿(L ∪ (H ∩ IE)) = t3↿(L ∪ (H ∩ IE)))"  

(* Interleaving-based Generalized Noninterference [ZL97] *)
(* MAKS representation *) 
definition IBGNI :: "'e set ⇒ 'e set ⇒ 'e set ⇒ 'e IFP_type"
where "IBGNI L H IE ≡ ( {HighInputsConfidential L H IE}, {D, I})"

lemma IBGNI_valid: "L ∩ H = {} ⟹ IFP_valid (L ∪ H) (IBGNI L H IE)"
  unfolding IFP_valid_def IBGNI_def HighInputsConfidential_def isViewOn_def 
    V_valid_def VN_disjoint_def VC_disjoint_def NC_disjoint_def
  using BasicSecurityPredicates.BSP_valid_D BasicSecurityPredicates.BSP_valid_I 
  by auto    

(* Literature representation *) 
definition 
litIBGNI :: "'e set ⇒ 'e set ⇒ 'e set ⇒ ('e list) set ⇒ bool"  
where 
"litIBGNI L H IE Tr ≡ 
  ∀ τ_l ∈ Tr. ∀ t_hi t. 
    (set t_hi) ⊆ (H ∩ IE)  ∧ t ∈ interleaving t_hi (τ_l ↿ L) 
      ⟶ (∃ τ' ∈ Tr. τ' ↿ (L ∪ (H ∩ IE)) = t)"  

(* Forward Correctability [JT88] *)
(* MAKS representation *)  
definition FC :: "'e set ⇒ 'e set ⇒ 'e set ⇒ 'e IFP_type"
where 
"FC L H IE ≡ 
  ( {HighInputsConfidential L H IE}, 
  {BSD, BSI, (FCD ⦇ Nabla=IE, Delta={}, Upsilon=IE ⦈), 
             (FCI ⦇ Nabla=IE, Delta={}, Upsilon=IE ⦈ )})"

lemma FC_valid: "L ∩ H = {} ⟹ IFP_valid (L ∪ H) (FC L H IE)"
  unfolding IFP_valid_def FC_def HighInputsConfidential_def isViewOn_def 
    V_valid_def VN_disjoint_def VC_disjoint_def NC_disjoint_def
  using BasicSecurityPredicates.BSP_valid_BSD BasicSecurityPredicates.BSP_valid_BSI
    BasicSecurityPredicates.BSP_valid_FCD BasicSecurityPredicates.BSP_valid_FCI
  by auto  

(* Literature representation *)
definition litFC :: "'e set ⇒ 'e set ⇒ 'e set ⇒ ('e list) set ⇒ bool"
where 
"litFC L H IE Tr ≡ 
  ∀t_1 t_2. ∀ hi ∈ (H ∩ IE). 
  (
    (∀ li ∈ (L ∩ IE). 
      t_1 @ [li] @ t_2 ∈ Tr ∧ t_2 ↿ (H ∩ IE) = [] 
      ⟶ (∃ t_3. t_1 @ [hi] @ [li] @ t_3 ∈ Tr 
                   ∧ t_3 ↿ L = t_2 ↿ L ∧ t_3 ↿ (H ∩ IE) = [] ))
      ∧ (t_1 @ t_2 ∈ Tr ∧ t_2 ↿ (H ∩ IE) = [] 
         ⟶ (∃ t_3. t_1 @ [hi]  @ t_3 ∈ Tr 
                      ∧ t_3 ↿ L = t_2 ↿ L ∧ t_3 ↿ (H ∩ IE) = [] ))
     ∧ (∀ li ∈ (L ∩ IE). 
          t_1 @ [hi] @ [li] @ t_2 ∈ Tr ∧ t_2 ↿ (H ∩ IE) = [] 
           ⟶ (∃ t_3. t_1 @ [li] @ t_3 ∈ Tr 
                        ∧ t_3 ↿ L = t_2 ↿ L ∧ t_3 ↿ (H ∩ IE) = [] )) 
          ∧ (t_1 @ [hi]  @ t_2 ∈ Tr ∧ t_2 ↿ (H ∩ IE) = [] 
             ⟶ (∃ t_3. t_1  @ t_3 ∈ Tr 
                          ∧ t_3 ↿ L = t_2 ↿ L ∧ t_3 ↿ (H ∩ IE) = [] ))
  )"  

(* Nondeducibility for outputs [GN88] *)
(* MAKS representation *)
definition NDO :: "'e set ⇒ 'e set ⇒ 'e set ⇒ 'e IFP_type"
where 
"NDO UI L H ≡ 
  ( {HighConfidential L H}, {BSD, (BSIA (λ 𝒱. C⇘𝒱⇙ ∪ (V⇘𝒱⇙ ∩ UI)))})"

lemma NDO_valid: "L ∩ H = {} ⟹ IFP_valid (L ∪ H) (NDO UI L H)"
  unfolding IFP_valid_def NDO_def HighConfidential_def isViewOn_def 
    V_valid_def VN_disjoint_def VC_disjoint_def NC_disjoint_def
  using BasicSecurityPredicates.BSP_valid_BSD
        BasicSecurityPredicates.BSP_valid_BSIA[of "(λ 𝒱. C⇘𝒱⇙ ∪ (V⇘𝒱⇙ ∩ UI))"]
  by auto 
  
(* Literature representation *)
definition litNDO :: "'e set ⇒ 'e set ⇒ 'e set ⇒ ('e list) set ⇒ bool"
where 
"litNDO UI L H Tr ≡ 
  ∀τ_l ∈ Tr. ∀ τ_hlui ∈ Tr.  ∀ t. 
    t↿L = τ_l↿L ∧ t↿(H ∪ (L ∩ UI)) = τ_hlui↿(H ∪ (L ∩ UI)) ⟶ t ∈ Tr"  
  
(* Noninference [ZL97] *)
(* MAKS representation *)  
definition NF :: "'e set ⇒ 'e set ⇒ 'e IFP_type"
where 
"NF L H ≡ ( {HighConfidential L H}, {R})"

lemma NF_valid: "L ∩ H = {} ⟹ IFP_valid (L ∪ H) (NF L H)"
  unfolding IFP_valid_def NF_def HighConfidential_def isViewOn_def 
    V_valid_def VN_disjoint_def VC_disjoint_def NC_disjoint_def
  using BasicSecurityPredicates.BSP_valid_R
  by auto     

(* Literature representation *)  
definition litNF :: "'e set ⇒ 'e set ⇒ ('e list) set ⇒ bool"
where 
"litNF L H Tr ≡ ∀τ ∈ Tr. τ ↿ L ∈ Tr"


(* Generalized Noninference [ZL97] *)
(* MAKS representation *)
definition GNF :: "'e set ⇒ 'e set ⇒ 'e set ⇒ 'e IFP_type"
where 
"GNF L H IE ≡ ( {HighInputsConfidential L H IE}, {R})"

lemma GNF_valid: "L ∩ H = {} ⟹ IFP_valid (L ∪ H) (GNF L H IE)"
  unfolding IFP_valid_def GNF_def HighInputsConfidential_def isViewOn_def 
    V_valid_def VN_disjoint_def VC_disjoint_def NC_disjoint_def
  using BasicSecurityPredicates.BSP_valid_R
  by auto       

(* Literature representation *)
definition litGNF :: "'e set ⇒ 'e set ⇒ 'e set ⇒ ('e list) set ⇒ bool"
where 
"litGNF L H IE Tr ≡ 
  ∀τ ∈ Tr. ∃τ' ∈ Tr. τ'↿ (H ∩ IE) = [] ∧ τ'↿ L = τ ↿ L"  
  
(* Separability [ZL97] *)
(* MAKS representation *)  
definition SEP :: "'e set ⇒ 'e set ⇒ 'e IFP_type"
where 
"SEP L H ≡ ( {HighConfidential L H}, {BSD, (BSIA (λ 𝒱. C⇘𝒱⇙))})"

lemma SEP_valid: "L ∩ H = {} ⟹ IFP_valid (L ∪ H) (SEP L H)"
  unfolding IFP_valid_def SEP_def HighConfidential_def isViewOn_def 
    V_valid_def VN_disjoint_def VC_disjoint_def NC_disjoint_def
  using BasicSecurityPredicates.BSP_valid_BSD
        BasicSecurityPredicates.BSP_valid_BSIA[of "λ 𝒱. C⇘𝒱⇙"]
  by auto     
    
(* Literature representation *)
definition litSEP :: "'e set ⇒ 'e set ⇒ ('e list) set ⇒ bool"
where 
"litSEP L H Tr ≡ 
  ∀τ_l ∈ Tr. ∀ τ_h ∈ Tr. 
    interleaving (τ_l ↿ L) (τ_h ↿ H) ⊆ {τ ∈ Tr . τ ↿ L = τ_l ↿ L} "  

(* Perfect Security Property [ZL97] *)
(* MAKS representation *)
definition PSP :: "'e set ⇒ 'e set ⇒ 'e IFP_type"
where 
"PSP L H ≡ 
  ( {HighConfidential L H}, {BSD, (BSIA (λ 𝒱. C⇘𝒱⇙ ∪ N⇘𝒱⇙ ∪ V⇘𝒱⇙))})"

lemma PSP_valid: "L ∩ H = {} ⟹ IFP_valid (L ∪ H) (PSP L H)"
  unfolding IFP_valid_def PSP_def HighConfidential_def isViewOn_def 
    V_valid_def VN_disjoint_def VC_disjoint_def NC_disjoint_def
  using BasicSecurityPredicates.BSP_valid_BSD
        BasicSecurityPredicates.BSP_valid_BSIA[of "λ 𝒱. C⇘𝒱⇙ ∪ N⇘𝒱⇙ ∪ V⇘𝒱⇙"]
  by auto         

(* Literature representation *)
definition litPSP :: "'e set ⇒ 'e set ⇒ ('e list) set ⇒ bool"
where 
"litPSP L H Tr ≡ 
  (∀τ ∈ Tr. τ ↿ L ∈ Tr) 
    ∧ (∀ α β. (β @ α) ∈ Tr ∧ (α ↿ H) = [] 
                ⟶ (∀ h ∈ H. β @ [h] ∈ Tr ⟶ β @ [h] @ α ∈ Tr))"  

end