Theory Syntactic_Criteria

theory Syntactic_Criteria
  imports Compositionality
begin

context PL_Indis
begin

(* Table: Compositionality of during-execution noninterferences *)

lemma noWhile[intro]:
  "noWhile (Atm atm)"
  "noWhile c1 ⟹ noWhile c2 ⟹ noWhile (Seq c1 c2)"
  "noWhile c1 ⟹ noWhile c2 ⟹ noWhile (If tst c1 c2)"
  "noWhile c1 ⟹ noWhile c2 ⟹ noWhile (Par c1 c2)"
  by auto

lemma discr[intro]:
  "presAtm atm ⟹ discr (Atm atm)"
  "discr c1 ⟹ discr c2 ⟹ discr (Seq c1 c2)"
  "discr c1 ⟹ discr c2 ⟹ discr (If tst c1 c2)"
  "discr c ⟹ discr (While tst c)"
  "discr c1 ⟹ discr c2 ⟹ discr (Par c1 c2)"
  by auto

lemma siso[intro]:
  "compatAtm atm ⟹ siso (Atm atm)"
  "siso c1 ⟹ siso c2 ⟹ siso (Seq c1 c2)"
  "compatTst tst ⟹ siso c1 ⟹ siso c2 ⟹ siso (If tst c1 c2)"
  "compatTst tst ⟹ siso c ⟹ siso (While tst c)"
  "siso c1 ⟹ siso c2 ⟹ siso (Par c1 c2)"
  by auto

lemma Sbis[intro]:
  "compatAtm atm ⟹ Atm atm ≈s Atm atm"
  "c1 ≈s c1 ⟹ c2 ≈s c2 ⟹ Seq c1 c2 ≈s Seq c1 c2"
  "compatTst tst ⟹ c1 ≈s c1 ⟹ c2 ≈s c2 ⟹ If tst c1 c2 ≈s If tst c1 c2"
  "compatTst tst ⟹ c ≈s c ⟹ While tst c ≈s While tst c"
  "c1 ≈s c1 ⟹ c2 ≈s c2 ⟹ Par c1 c2 ≈s Par c1 c2"
  by auto

lemma ZObisT[intro]:
  "compatAtm atm ⟹ Atm atm ≈01T Atm atm"
  "c1 ≈01T c1 ⟹ c2 ≈01T c2 ⟹ Seq c1 c2 ≈01T Seq c1 c2"
  "compatTst tst ⟹ c1 ≈01T c1 ⟹ c2 ≈01T c2 ⟹ If tst c1 c2 ≈01T If tst c1 c2"
  "compatTst tst ⟹ c ≈01T c ⟹ While tst c ≈01T While tst c"
  "c1 ≈01T c1 ⟹ c2 ≈01T c2 ⟹ Par c1 c2 ≈01T Par c1 c2"
  by auto

lemma BisT[intro]:
  "compatAtm atm ⟹ Atm atm ≈T Atm atm"
  "c1 ≈T c1 ⟹ c2 ≈T c2 ⟹ Seq c1 c2 ≈T Seq c1 c2"
  "compatTst tst ⟹ c1 ≈T c1 ⟹ c2 ≈T c2 ⟹ If tst c1 c2 ≈T If tst c1 c2"
  "compatTst tst ⟹ c ≈T c ⟹ While tst c ≈T While tst c"
  "c1 ≈T c1 ⟹ c2 ≈T c2 ⟹ Par c1 c2 ≈T Par c1 c2"
  by auto

lemma WbisT[intro]:
  "compatAtm atm ⟹ Atm atm ≈wT Atm atm"
  "c1 ≈wT c1 ⟹ c2 ≈wT c2 ⟹ Seq c1 c2 ≈wT Seq c1 c2"
  "compatTst tst ⟹ c1 ≈wT c1 ⟹ c2 ≈wT c2 ⟹ If tst c1 c2 ≈wT If tst c1 c2"
  "compatTst tst ⟹ c ≈wT c ⟹ While tst c ≈wT While tst c"
  "c1 ≈wT c1 ⟹ c2 ≈wT c2 ⟹ Par c1 c2 ≈wT Par c1 c2"
  by auto

lemma ZObis[intro]:
  "compatAtm atm ⟹ Atm atm ≈01 Atm atm"
  "c1 ≈01T c1 ⟹ c2 ≈01 c2 ⟹ Seq c1 c2 ≈01 Seq c1 c2"
  "c1 ≈01 c1 ⟹ discr c2 ⟹ Seq c1 c2 ≈01 Seq c1 c2"
  "compatTst tst ⟹ c1 ≈01 c1 ⟹ c2 ≈01 c2 ⟹ If tst c1 c2 ≈01 If tst c1 c2"
  "c1 ≈01 c1 ⟹ c2 ≈01 c2 ⟹ Par c1 c2 ≈01 Par c1 c2"
  by auto

lemma Wbis[intro]:
  "compatAtm atm ⟹ Atm atm ≈w Atm atm"
  "c1 ≈wT c1 ⟹ c2 ≈w c2 ⟹ Seq c1 c2 ≈w Seq c1 c2"
  "c1 ≈w c1 ⟹ discr c2 ⟹ Seq c1 c2 ≈w Seq c1 c2"
  "compatTst tst ⟹ c1 ≈w c1 ⟹ c2 ≈w c2 ⟹ If tst c1 c2 ≈w If tst c1 c2"
  "c1 ≈w c1 ⟹ c2 ≈w c2 ⟹ Par c1 c2 ≈w Par c1 c2"
  by auto

(* Graph: The cleaned-up graph of implcations between security notions *)


lemma discr_noWhile_WbisT[intro]: "discr c ⟹ noWhile c ⟹ c ≈wT c"
  by auto

lemma siso_ZObis[intro]: "siso c ⟹ c ≈01 c"
  by auto

lemma WbisT_Wbis[intro]: "c ≈wT c ⟹ c ≈w c"
  by auto

lemma ZObis_Wbis[intro]: "c ≈01 c ⟹ c ≈w c"
  by auto

lemma discr_BisT[intro]: "discr c ⟹ c ≈T c"
  by auto

lemma WbisT_BisT[intro]: "c ≈wT c ⟹ c ≈T c"
  using bis_incl by auto

lemma ZObisT_ZObis[intro]: "c ≈01T c ⟹ c ≈01 c"
  by auto

lemma siso_ZObisT[intro]: "siso c ⟹ c ≈01T c"
  by auto

primrec SC_discr where
  "SC_discr (Atm atm)      ⟷ presAtm atm"
| "SC_discr (Seq c1 c2)    ⟷ SC_discr c1 ∧ SC_discr c2"
| "SC_discr (If tst c1 c2) ⟷ SC_discr c1 ∧ SC_discr c2"
| "SC_discr (While tst c)  ⟷ SC_discr c"
| "SC_discr (Par c1 c2)    ⟷ SC_discr c1 ∧ SC_discr c2"

primrec SC_siso where
  "SC_siso (Atm atm)      ⟷ compatAtm atm"
| "SC_siso (Seq c1 c2)    ⟷ SC_siso c1 ∧ SC_siso c2"
| "SC_siso (If tst c1 c2) ⟷ compatTst tst ∧ SC_siso c1 ∧ SC_siso c2"
| "SC_siso (While tst c)  ⟷ compatTst tst ∧ SC_siso c"
| "SC_siso (Par c1 c2)    ⟷ SC_siso c1 ∧ SC_siso c2"

primrec SC_WbisT where
  "SC_WbisT (Atm atm)      ⟷ compatAtm atm"
| "SC_WbisT (Seq c1 c2)    ⟷ (SC_WbisT c1 ∧ SC_WbisT c2) ∨
                              (noWhile (Seq c1 c2) ∧ SC_discr (Seq c1 c2)) ∨ 
                              SC_siso (Seq c1 c2)"
| "SC_WbisT (If tst c1 c2) ⟷ (if compatTst tst
                              then (SC_WbisT c1 ∧ SC_WbisT c2)
                              else ((noWhile (If tst c1 c2) ∧ SC_discr (If tst c1 c2)) ∨ 
                                    SC_siso (If tst c1 c2)))"
| "SC_WbisT (While tst c)  ⟷ (if compatTst tst
                              then SC_WbisT c
                              else ((noWhile (While tst c) ∧ SC_discr (While tst c)) ∨ 
                                    SC_siso (While tst c)))"
| "SC_WbisT (Par c1 c2)    ⟷ (SC_WbisT c1 ∧ SC_WbisT c2) ∨
                              (noWhile (Par c1 c2) ∧ SC_discr (Par c1 c2)) ∨ 
                              SC_siso (Par c1 c2)"

primrec SC_ZObis where
  "SC_ZObis (Atm atm)      ⟷ compatAtm atm"
| "SC_ZObis (Seq c1 c2)    ⟷ (SC_siso c1 ∧ SC_ZObis c2) ∨
                              (SC_ZObis c1 ∧ SC_discr c2) ∨
                              SC_discr (Seq c1 c2) ∨ 
                              SC_siso (Seq c1 c2)"
| "SC_ZObis (If tst c1 c2) ⟷ (if compatTst tst
                              then (SC_ZObis c1 ∧ SC_ZObis c2)
                              else (SC_discr (If tst c1 c2) ∨ 
                                    SC_siso (If tst c1 c2)))"
| "SC_ZObis (While tst c)  ⟷ SC_discr (While tst c) ∨ 
                              SC_siso (While tst c)"
| "SC_ZObis (Par c1 c2)    ⟷ (SC_ZObis c1 ∧ SC_ZObis c2) ∨
                              SC_discr (Par c1 c2) ∨ 
                              SC_siso (Par c1 c2)"

primrec SC_Wbis where
  "SC_Wbis (Atm atm)      ⟷ compatAtm atm"
| "SC_Wbis (Seq c1 c2)    ⟷ (SC_WbisT c1 ∧ SC_Wbis c2) ∨
                             (SC_Wbis c1 ∧ SC_discr c2) ∨
                             SC_ZObis (Seq c1 c2) ∨ 
                             SC_WbisT (Seq c1 c2)"
| "SC_Wbis (If tst c1 c2) ⟷ (if compatTst tst
                             then (SC_Wbis c1 ∧ SC_Wbis c2)
                             else (SC_ZObis (If tst c1 c2) ∨ 
                                   SC_WbisT (If tst c1 c2)))"
| "SC_Wbis (While tst c)  ⟷ SC_ZObis (While tst c) ∨ 
                             SC_WbisT (While tst c)"
| "SC_Wbis (Par c1 c2)    ⟷ (SC_Wbis c1 ∧ SC_Wbis c2) ∨
                             SC_ZObis (Par c1 c2) ∨ 
                             SC_WbisT (Par c1 c2)"

primrec SC_BisT where
  "SC_BisT (Atm atm)      ⟷ compatAtm atm"
| "SC_BisT (Seq c1 c2)    ⟷ (SC_BisT c1 ∧ SC_BisT c2) ∨
                             SC_discr (Seq c1 c2) ∨ 
                             SC_WbisT (Seq c1 c2)"
| "SC_BisT (If tst c1 c2) ⟷ (if compatTst tst
                             then (SC_BisT c1 ∧ SC_BisT c2)
                             else (SC_discr (If tst c1 c2) ∨ 
                                   SC_WbisT (If tst c1 c2)))"
| "SC_BisT (While tst c)  ⟷ (if compatTst tst
                             then SC_BisT c
                             else (SC_discr (While tst c) ∨ 
                                   SC_WbisT (While tst c)))"
| "SC_BisT (Par c1 c2)    ⟷ (SC_BisT c1 ∧ SC_BisT c2) ∨
                             SC_discr (Par c1 c2) ∨ 
                             SC_WbisT (Par c1 c2)"

theorem SC_discr[intro]: "SC_discr c ⟹ discr c"
  by (induct c) auto

theorem SC_siso[intro]: "SC_siso c ⟹ siso c"
  by (induct c) auto

theorem SC_siso_imp_SC_WbisT[intro]: "SC_siso c ⟹ SC_WbisT c"
  by (induct c) auto

theorem SC_discr_imp_SC_WbisT[intro]: "noWhile c ⟹ SC_discr c ⟹ SC_WbisT c"
  by (induct c) (auto simp: presAtm_compatAtm)

theorem SC_WbisT[intro]: "SC_WbisT c ⟹ c ≈wT c"
  by (induct c) (auto split: if_split_asm)

theorem SC_discr_imp_SC_ZObis[intro]: "SC_discr c ⟹ SC_ZObis c"
  by (induct c) (auto simp: presAtm_compatAtm)

theorem SC_siso_imp_SC_ZObis[intro]: "SC_siso c ⟹ SC_ZObis c"
  by (induct c) auto
  
theorem SC_ZObis[intro]: "SC_ZObis c ⟹ c ≈01 c"
  by (induct c) (auto split: if_split_asm intro: discr_ZObis)

theorem SC_ZObis_imp_SC_Wbis[intro]: "SC_ZObis c ⟹ SC_Wbis c"
  by (induct c) auto

theorem SC_WbisT_imp_SC_Wbis[intro]: "SC_WbisT c ⟹ SC_Wbis c"
  by (induct c) auto

theorem SC_Wbis[intro]: "SC_Wbis c ⟹ c ≈w c"
  by (induct c) (auto split: if_split_asm intro: discr_ZObis)

theorem SC_discr_imp_SC_BisT[intro]: "SC_discr c ⟹ SC_BisT c"
  by (induct c) (auto simp: presAtm_compatAtm)

theorem SC_WbisT_imp_SC_BisT[intro]: "SC_WbisT c ⟹ SC_BisT c"
  by (induct c) auto

theorem SC_ZObis_imp_SC_BisT[intro]: "SC_ZObis c ⟹ SC_BisT c"
  by (induct c) auto

theorem SC_Wbis_imp_SC_BisT[intro]: "SC_Wbis c ⟹ SC_BisT c"
  by (induct c) (auto split: if_split_asm)

theorem SC_BisT[intro]: "SC_BisT c ⟹ c ≈T c"
  by (induct c) (auto split: if_split_asm)

(* reductions *)

theorem SC_WbisT_While: "SC_WbisT (While tst c) ⟷ SC_WbisT c ∧ compatTst tst"
  by simp

theorem SC_ZObis_While: "SC_ZObis (While tst c) ⟷ (compatTst tst ∧ SC_siso c) ∨ SC_discr c"
  by auto

theorem SC_ZObis_If: "SC_ZObis (If tst c1 c2) ⟷ (if compatTst tst then SC_ZObis c1 ∧ SC_ZObis c2 else SC_discr c1 ∧ SC_discr c2)"
  by simp

theorem SC_WbisT_Seq: "SC_WbisT (Seq c1 c2)  ⟷ (SC_WbisT c1 ∧ SC_WbisT c2)"
  by auto

theorem SC_ZObis_Seq: "SC_ZObis (Seq c1 c2) ⟷ (SC_siso c1 ∧ SC_ZObis c2) ∨
                              (SC_ZObis c1 ∧ SC_discr c2)"
  by auto

theorem SC_Wbis_Seq: "SC_Wbis (Seq c1 c2) ⟷ (SC_WbisT c1 ∧ SC_Wbis c2) ∨ (SC_Wbis c1 ∧ SC_discr c2)"
  by auto

theorem SC_BisT_Par:
  "SC_BisT (Par c1 c2)    ⟷ (SC_BisT c1 ∧ SC_BisT c2)"
  by auto

end

end