# 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
```