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