Theory DYNAMIC_Post_Value_Setup_ISSUER

(* The value setup for post confidentiality *)
theory DYNAMIC_Post_Value_Setup_ISSUER
  imports
    "../Safety_Properties"
    "Post_Observation_Setup_ISSUER"
    "Post_Unwinding_Helper_ISSUER"
begin

subsection ‹Variation with dynamic declassification trigger›

text ‹This section formalizes the ``dynamic'' variation of one
post confidentiality properties, as described in \<^cite>‹‹Appendix C› in "cosmedis-SandP2017"›.
›

locale Post = ObservationSetup_ISSUER
begin

subsubsection‹Issuer value setup›

datatype "value" =
  isPVal: PVal post ― ‹updating the post content locally›
| isPValS: PValS (tgtAPI: apiID) post ― ‹sending the post to another node›
| isOVal: OVal bool ― ‹change in the dynamic declassification trigger condition›

text ‹The dynamic declassification trigger condition holds, i.e.~the access window to the
confidential information is open, when the post is public or one of the observers is the
administrator, the post's owner, or a friend of the post's owner.›

definition "open" where
"open s ≡
 ∃ uid ∈ UIDs.
   uid ∈∈ userIDs s ∧ PID ∈∈ postIDs s ∧
   (uid = admin s ∨ uid = owner s PID ∨ uid ∈∈ friendIDs s (owner s PID) ∨
    vis s PID = PublicV)"

sublocale Issuer_State_Equivalence_Up_To_PID .

lemma eqButPID_open:
assumes "eqButPID s s1"
shows "open s ⟷ open s1"
using eqButPID_stateSelectors[OF assms] (* eqButPID_postSelectors[OF assms] *)
unfolding open_def by auto

lemma not_open_eqButPID:
assumes 1: "¬ open s" and 2: "eqButPID s s1"
shows "¬ open s1"
using 1 unfolding eqButPID_open[OF 2] .

lemma step_isCOMact_open:
assumes "step s a = (ou, s')"
and "isCOMact a"
shows "open s' = open s"
using assms proof (cases a)
  case (COMact ca) then show ?thesis using assms by (cases ca) (auto simp: open_def com_defs)
qed auto

lemma validTrans_isCOMact_open:
assumes "validTrans trn"
and "isCOMact (actOf trn)"
shows "open (tgtOf trn) = open (srcOf trn)"
using assms step_isCOMact_open by (cases trn) auto



lemma list_all_isOVal_filter_isPValS:
"list_all isOVal vl ⟹ filter (Not o isPValS) vl = vl"
by (induct vl) auto

lemma list_all_Not_isOVal_OVal_True:
assumes "list_all (Not ∘ isOVal) ul"
and "ul @ vll = OVal True # vll'"
shows "ul = []"
using assms by (cases ul) auto

lemma list_all_filter_isOVal_isPVal_isPValS:
assumes "list_all (Not ∘ isOVal) ul"
and "filter isPValS ul = []" and "filter isPVal ul = []"
shows "ul = []"
using assms value.exhaust_disc by (induct ul) auto

lemma filter_list_all_isPValS_isOVal:
assumes "list_all (Not ∘ isOVal) ul" and "filter isPVal ul = []"
shows "list_all isPValS ul"
using assms value.exhaust_disc by (induct ul) auto

lemma filter_list_all_isPVal_isOVal:
assumes "list_all (Not ∘ isOVal) ul" and "filter isPValS ul = []"
shows "list_all isPVal ul"
using assms value.exhaust_disc by (induct ul) auto

lemma list_all_isPValS_Not_isOVal_filter:
assumes "list_all isPValS ul" shows "list_all (Not ∘ isOVal) ul ∧ filter isPVal ul = []"
using assms value.exhaust_disc by (induct ul) auto

lemma filter_isTValS_Nil:
"filter isPValS vl = [] ⟷
 list_all (λ v. isPVal v ∨ isOVal v) vl"
proof(induct vl)
  case (Cons v vl)
  thus ?case by (cases v) auto
qed auto

(*   ******  *)
fun φ :: "(state,act,out) trans ⇒ bool" where
"φ (Trans _ (Uact (uPost uid p pid pst)) ou _) = (pid = PID ∧ ou = outOK)"
|
"φ (Trans _ (COMact (comSendPost uid p aid pid)) ou _) = (pid = PID ∧ ou ≠ outErr)"
(* Added during strengthening: saying ≠ outErr is simpler than actually describing the output, which essentially
   takes some parameters from the post and some values from the state. *)
|
"φ (Trans s _ _ s') = (open s ≠ open s')"

lemma φ_def2:
assumes "step s a = (ou,s')"
shows
"φ (Trans s a ou s') ⟷
 (∃uid p pst. a = Uact (uPost uid p PID pst) ∧ ou = outOK) ∨
 (∃uid p aid. a = COMact (comSendPost uid p aid PID) ∧ ou ≠ outErr) ∨
  open s ≠ open s'"
using assms by (cases "Trans s a ou s'" rule: φ.cases) (auto simp: all_defs open_def)

lemma uTextPost_out:
assumes 1: "step s a = (ou,s')" and a: "a = Uact (uPost uid p PID pst)" and 2: "ou = outOK"
shows "uid = owner s PID ∧ p = pass s uid"
using 1 2 unfolding a by (auto simp: u_defs)

lemma comSendPost_out:
assumes 1: "step s a = (ou,s')" and a: "a = COMact (comSendPost uid p aid PID)"
  and 2: "ou ≠ outErr"
shows "ou = O_sendPost (aid, clientPass s aid, PID, post s PID, owner s PID, vis s PID)
       ∧ uid = admin s ∧ p = pass s (admin s)"
using 1 2 unfolding a by (auto simp: com_defs)

lemma step_open_isCOMact:
assumes "step s a = (ou,s')"
and "open s ≠ open s'"
shows "¬ isCOMact a ∧ ¬ (∃ ua. isuPost ua ∧ a = Uact ua)"
  using assms unfolding open_def
  apply(cases a)
  subgoal by (auto simp: all_defs)
  subgoal by (auto simp: all_defs)
  subgoal by (auto simp: all_defs)
  subgoal for x4 by (cases x4) (auto simp: all_defs)
  subgoal by (auto simp: all_defs)
  subgoal by (auto simp: all_defs)
  subgoal for x7 by (cases x7) (auto simp: all_defs)
  done

lemma φ_def3:
assumes "step s a = (ou,s')"
shows
"φ (Trans s a ou s') ⟷
 (∃pst. a = Uact (uPost (owner s PID) (pass s (owner s PID)) PID pst) ∧ ou = outOK)
 ∨
 (∃aid. a = COMact (comSendPost (admin s) (pass s (admin s)) aid PID) ∧
        ou = O_sendPost (aid, clientPass s aid, PID, post s PID, owner s PID, vis s PID))
 ∨
 open s ≠ open s' ∧ ¬ isCOMact a ∧ ¬ (∃ ua. isuPost ua ∧ a = Uact ua)"
unfolding φ_def2[OF assms]
using comSendPost_out[OF assms] uTextPost_out[OF assms]
step_open_isCOMact[OF assms]
by blast

fun f :: "(state,act,out) trans ⇒ value" where
"f (Trans s (Uact (uPost uid p pid pst)) _ s') =
 (if pid = PID then PVal pst else OVal (open s'))"  (* else undefined  *)
|
"f (Trans s (COMact (comSendPost uid p aid pid)) (O_sendPost (_, _, _, pst, _)) s') =
 (if pid = PID then PValS aid pst else OVal (open s'))" (* else undefined  *)
|
"f (Trans s _ _ s') = OVal (open s')"

lemma f_open_OVal:
assumes "step s a = (ou,s')"
and "open s ≠ open s' ∧ ¬ isCOMact a ∧ ¬ (∃ ua. isuPost ua ∧ a = Uact ua)"
shows "f (Trans s a ou s') = OVal (open s')"
using assms by (cases "Trans s a ou s'" rule: f.cases) auto

lemma f_eq_PVal:
assumes "step s a = (ou,s')" and "φ (Trans s a ou s')"
and "f (Trans s a ou s') = PVal pst"
shows "a = Uact (uPost (owner s PID) (pass s (owner s PID)) PID pst)"
using assms by (cases "Trans s a ou s'" rule: f.cases) (auto simp: u_defs com_defs)

lemma f_eq_PValS:
assumes "step s a = (ou,s')" and "φ (Trans s a ou s')"
and "f (Trans s a ou s') = PValS aid pst"
shows "a = COMact (comSendPost (admin s) (pass s (admin s)) aid PID)"
using assms by (cases "Trans s a ou s'" rule: f.cases) (auto simp: com_defs)

lemma f_eq_OVal:
assumes "step s a = (ou,s')" and "φ (Trans s a ou s')"
and "f (Trans s a ou s') = OVal b"
shows "open s' ≠ open s"
using assms by (auto simp: φ_def2 com_defs)

lemma uPost_comSendPost_open_eq:
assumes step: "step s a = (ou, s')"
and a: "a = Uact (uPost uid p pid pst) ∨ a = COMact (comSendPost uid p aid pid)"
shows "open s' = open s"
using assms a unfolding open_def
by (cases a) (auto simp: u_defs com_defs)

lemma step_open_φ_f_PVal_γ:
assumes s: "reach s"
and step: "step s a = (ou, s')"
and PID: "PID ∈ set (postIDs s)"
and op: "¬ open s" and fi: "φ (Trans s a ou s')" and f: "f (Trans s a ou s') = PVal pst"
shows "¬ γ (Trans s a ou s')"
proof-
  have a: "a = Uact (uPost (owner s PID) (pass s (owner s PID)) PID pst)"
  using f_eq_PVal[OF step fi f] .
  have ou: "ou = outOK" using fi op unfolding a φ_def2[OF step] by auto
  have "owner s PID ∈∈ userIDs s" using s by (simp add: PID reach_owner_userIDs)
  hence "owner s PID ∉ UIDs" using op PID unfolding open_def by auto
  thus ?thesis unfolding a by simp
qed

lemma Uact_uPaperC_step_eqButPID:
assumes a: "a = Uact (uPost uid p PID pst)"
and "step s a = (ou,s')"
shows "eqButPID s s'"
using assms unfolding eqButPID_def eeqButPID_def eeqButPID_F_def
by (auto simp: all_defs split: if_splits)

lemma eqButPID_step_φ_imp:
assumes ss1: "eqButPID s s1"
and step: "step s a = (ou,s')" and step1: "step s1 a = (ou1,s1')"
and φ: "φ (Trans s a ou s')"
shows "φ (Trans s1 a ou1 s1')"
proof-
  have s's1': "eqButPID s' s1'"
  using eqButPID_step local.step ss1 step1 by blast
  show ?thesis using step step1 φ eqButPID_open[OF ss1] eqButPID_open[OF s's1']
  using eqButPID_stateSelectors[OF ss1]
  unfolding φ_def2[OF step] φ_def2[OF step1]
  by (auto simp: all_defs)
qed

lemma eqButPID_step_φ:
assumes s's1': "eqButPID s s1"
and step: "step s a = (ou,s')" and step1: "step s1 a = (ou1,s1')"
shows "φ (Trans s a ou s') = φ (Trans s1 a ou1 s1')"
by (metis eqButPID_step_φ_imp eqButPID_sym assms)


end



end