Theory Independent_Post_RECEIVER

theory Independent_Post_RECEIVER
  imports
    "Independent_Post_Observation_Setup_RECEIVER"
    "Independent_Post_Value_Setup_RECEIVER"
    "Bounded_Deducibility_Security.Compositional_Reasoning"
begin

subsubsection ‹Receiver declassification bound›

context Post_RECEIVER
begin


fun T :: "(state,act,out) trans ⇒ bool" where
"T (Trans s a ou s') ⟷
 (∃ uid ∈ UIDs.
   uid ∈∈ userIDs s' ∧ PID ∈∈ outerPostIDs s' AID ∧
   (uid = admin s' ∨
    (AID,outerOwner s' AID PID) ∈∈ recvOuterFriendIDs s' uid ∨
    outerVis s' AID PID = PublicV))"

definition B :: "value list ⇒ value list ⇒ bool" where
"B vl vl1 ≡ length vl = length vl1"

sublocale BD_Security_IO where
istate = istate and step = step and
φ = φ and f = f and γ = γ and g = g and T = T and B = B
done

subsubsection ‹Receiver unwinding proof›

lemma reach_PublicV_imples_FriendV[simp]:
assumes "reach s"
and "vis s pID ≠ PublicV"
shows "vis s pID = FriendV"
using assms reach_vis by auto

lemma reachNT_state:
assumes "reachNT s"
shows
"¬ (∃ uid ∈ UIDs.
   uid ∈∈ userIDs s ∧ PID ∈∈ outerPostIDs s AID ∧
   (uid = admin s ∨
    (AID,outerOwner s AID PID) ∈∈ recvOuterFriendIDs s uid ∨
     outerVis s AID PID = PublicV))"
using assms proof induct
  case (Step trn) thus ?case
  by (cases trn) auto
qed (simp add: istate_def)


(* major *) lemma eqButPID_step_γ_out:
assumes ss1: "eqButPID s s1"
and step: "step s a = (ou,s')" and step1: "step s1 a = (ou1,s1')"
and sT: "reachNT s" and T: "¬ T (Trans s a ou s')"
and s1: "reach s1"
and γ: "γ (Trans s a ou s')"
shows "ou = ou1"
proof-
  have s'T: "reachNT s'" using step sT T using reachNT_PairI by blast
  note op = reachNT_state[OF s'T]
  note [simp] = all_defs
  note s = reachNT_reach[OF sT]
  note willUse =
  step step1 γ
  op
  reach_vis[OF s]
  eqButPID_stateSelectors[OF ss1] (* eqButPID_postSelectors[OF ss1] *)
  eqButPID_actions[OF ss1]
  eqButPID_update[OF ss1] (* eqButPID_setTextPost[OF ss1] *) eqButPID_not_PID[OF ss1]
  show ?thesis
  proof (cases a)
    case (Sact x1)
    with willUse show ?thesis by (cases x1) auto
  next
    case (Cact x2)
    with willUse show ?thesis by (cases x2) auto
  next
    case (Dact x3)
    with willUse show ?thesis by (cases x3) auto
  next
    case (Uact x4)
    with willUse show ?thesis by (cases x4) auto
  next
    case (Ract x5)
    with willUse show ?thesis
    proof (cases x5)
      case (rOPost uid p aid pid)
      with Ract willUse show ?thesis by (cases "aid = AID ∧ pid = PID") auto
    qed auto
  next
    case (Lact x6)
    with willUse show ?thesis by (cases x6) auto
  next
    case (COMact x7)
    with willUse show ?thesis by (cases x7) auto
  qed
qed


definition Δ0 :: "state ⇒ value list ⇒ state ⇒ value list ⇒ bool" where
"Δ0 s vl s1 vl1 ≡
 ¬ AID ∈∈ serverApiIDs s ∧
 s = s1 ∧
 length vl = length vl1"

definition Δ1 :: "state ⇒ value list ⇒ state ⇒ value list ⇒ bool" where
"Δ1 s vl s1 vl1 ≡
 AID ∈∈ serverApiIDs s ∧
 eqButPID s s1 ∧
 length vl = length vl1"

lemma istate_Δ0:
assumes B: "B vl vl1"
shows "Δ0 istate vl istate vl1"
using assms unfolding Δ0_def B_def istate_def by auto

lemma unwind_cont_Δ0: "unwind_cont Δ0 {Δ0,Δ1}"
proof(rule, simp)
  let ?Δ = "λs vl s1 vl1. Δ0 s vl s1 vl1 ∨ Δ1 s vl s1 vl1"
  fix s s1 :: state and vl vl1 :: "value list"
  assume rsT: "reachNT s" and rs1: "reach s1" and "Δ0 s vl s1 vl1"
  hence rs: "reach s" and ss1: "s1 = s" and l: "length vl = length vl1"
  and AID: "¬ AID ∈∈ serverApiIDs s"
  using reachNT_reach unfolding Δ0_def by auto
  show "iaction ?Δ s vl s1 vl1 ∨
        ((vl = [] ⟶ vl1 = []) ∧ reaction ?Δ s vl s1 vl1)" (is "?iact ∨ (_ ∧ ?react)")
  proof-
    have ?react proof
      fix a :: act and ou :: out and s' :: state and vl'
      let ?trn = "Trans s a ou s'"  let ?trn1 = "Trans s1 a ou s'"
      assume step: "step s a = (ou, s')" and T: "¬ T ?trn" and c: "consume ?trn vl vl'"
      show "match ?Δ s s1 vl1 a ou s' vl' ∨ ignore ?Δ s s1 vl1 a ou s' vl'" (is "?match ∨ ?ignore")
      proof-
        have φ: "¬ φ ?trn" using AID step unfolding φ_def2(* [OF step] *) by (auto simp: u_defs com_defs)
        hence vl': "vl' = vl" using c φ unfolding consume_def by simp
        have ?match proof(cases "∃ p. a = COMact (comConnectServer AID p) ∧ ou = outOK")
          case True
          then obtain p where a: "a = COMact (comConnectServer AID p)" and ou: "ou = outOK" by auto
          have AID': "AID ∈∈ serverApiIDs s'"
          using step AID unfolding a ou by (auto simp: com_defs)
          note uid = reachNT_state[OF rsT]
          show ?thesis proof
            show "validTrans ?trn1" unfolding ss1 using step by simp
          next
            show "consume ?trn1 vl1 vl1" using φ unfolding consume_def ss1 by auto
          next
            show "γ ?trn = γ ?trn1" unfolding ss1 by simp
          next
            assume "γ ?trn" thus "g ?trn = g ?trn1" unfolding ss1 by simp
          next
            have "Δ1 s' vl' s' vl1" using l AID' c unfolding ss1 Δ1_def vl' by auto
            thus "?Δ s' vl' s' vl1" by simp
          qed
        next
          case False note a = False
          have AID': "¬ AID ∈∈ serverApiIDs s'"
            using step AID a
            apply(cases a)
            subgoal for x1 apply(cases x1) apply(fastforce simp: s_defs)+ .
            subgoal for x2 apply(cases x2) apply(fastforce simp: c_defs)+ .
            subgoal for x3 apply(cases x3) apply(fastforce simp: d_defs)+ .
            subgoal for x4 apply(cases x4) apply(fastforce simp: u_defs)+ .
            subgoal by auto
            subgoal by auto
            subgoal for x7 apply(cases x7) apply(fastforce simp: com_defs)+ .
            done
          show ?thesis proof
            show "validTrans ?trn1" unfolding ss1 using step by simp
          next
            show "consume ?trn1 vl1 vl1" using φ unfolding consume_def ss1 by auto
          next
            show "γ ?trn = γ ?trn1" unfolding ss1 by simp
          next
            assume "γ ?trn" thus "g ?trn = g ?trn1" unfolding ss1 by simp
          next
            have "Δ0 s' vl' s' vl1" using a AID' l unfolding Δ0_def vl' ss1 by simp
            thus "?Δ s' vl' s' vl1" by simp
          qed
        qed
        thus ?thesis by simp
      qed
    qed
  thus ?thesis using l by auto
  qed
qed

lemma unwind_cont_Δ1: "unwind_cont Δ1 {Δ1}"
proof(rule, simp)
  let ?Δ = "λs vl s1 vl1. Δ1 s vl s1 vl1"
  fix s s1 :: state and vl vl1 :: "value list"
  assume rsT: "reachNT s" and rs1: "reach s1" and "Δ1 s vl s1 vl1"
  hence rs: "reach s" and ss1: "eqButPID s s1"
  and l: "length vl = length vl1" and AID: "AID ∈∈ serverApiIDs s"
  using reachNT_reach unfolding Δ1_def by auto
  have AID1: "AID ∈∈ serverApiIDs s1" using eqButPID_stateSelectors[OF ss1] AID by auto

  show "iaction ?Δ s vl s1 vl1 ∨
        ((vl = [] ⟶ vl1 = []) ∧ reaction ?Δ s vl s1 vl1)" (is "?iact ∨ (_ ∧ ?react)")
  proof-
    have ?react proof
      fix a :: act and ou :: out and s' :: state and vl'
      let ?trn = "Trans s a ou s'"
      assume step: "step s a = (ou, s')" and T: "¬ T ?trn" and c: "consume ?trn vl vl'"
      show "match ?Δ s s1 vl1 a ou s' vl' ∨ ignore ?Δ s s1 vl1 a ou s' vl'" (is "?match ∨ ?ignore")
      proof-
        have ?match proof(cases "∃ p pst uid vs. a = COMact (comReceivePost AID p PID pst uid vs) ∧ ou = outOK")
          case True
          then obtain p pst uid vs where
          a: "a = COMact (comReceivePost AID p PID pst uid vs)" and ou: "ou = outOK" by auto
          have p: "p = serverPass s AID" using comReceivePost_out[OF step a ou] .
          have p1: "p = serverPass s1 AID" using p ss1 eqButPID_stateSelectors by auto
          have φ: "φ ?trn" using a ou step φ_def2 by auto
          obtain v where vl: "vl = v # vl'" and f: "f ?trn = v"
          using c φ unfolding consume_def by (cases vl) auto
          have AID': "AID ∈∈ serverApiIDs s'" using step AID unfolding a ou by (auto simp: com_defs)
          note uid = reachNT_state[OF rsT]
          obtain v1 vl1' where vl1: "vl1 = v1 # vl1'" using l unfolding vl by (cases vl1) auto
          obtain pst1 where v1: "v1 = PValR pst1" by (cases v1) auto
          define a1 where a1: "a1 ≡ COMact (comReceivePost AID p PID pst1 uid vs)"
          obtain s1' where step1: "step s1 a1 = (outOK, s1')" using AID1 unfolding a1 p1 by (simp add: com_defs)
          have s's1': "eqButPID s' s1'" using comReceivePost_step_eqButPID[OF a _ step step1 ss1] a1 by simp
          let ?trn1 = "Trans s1 a1 outOK s1'"
          have φ1: "φ ?trn1" unfolding φ_def2(* [OF step1] *) unfolding a1 by auto
          have f1: "f ?trn1 = v1" unfolding a1 v1 by simp
          show ?thesis proof
            show "validTrans ?trn1" using step1 by simp
          next
            show "consume ?trn1 vl1 vl1'" using φ1 f1 unfolding consume_def ss1 vl1 by simp
          next
            show "γ ?trn = γ ?trn1" unfolding a a1 by simp
          next
            assume "γ ?trn" thus "g ?trn = g ?trn1" unfolding a a1 ou by simp
          next
            show "Δ1 s' vl' s1' vl1'" using l AID' c s's1' unfolding Δ1_def vl vl1 by simp
          qed
        next
          case False note a = False
          obtain s1' ou1 where step1: "step s1 a = (ou1, s1')" by fastforce
          let ?trn1 = "Trans s1 a ou1 s1'"
          have φ: "¬ φ ?trn" using a step φ_def2 by auto
          have φ1: "¬ φ ?trn1" using φ ss1 step step1 eqButPID_step_φ by blast
          have s's1': "eqButPID s' s1'" using ss1 step step1 eqButPID_step by blast
          have ouou1: "γ ?trn ⟹ ou = ou1" using eqButPID_step_γ_out ss1 step step1 T rs1 rsT by blast
          have AID': "AID ∈∈ serverApiIDs s'" using AID step rs using IDs_mono by auto
          have vl': "vl' = vl" using c φ unfolding consume_def by simp
          show ?thesis proof
            show "validTrans ?trn1" using step1 by simp
          next
            show "consume ?trn1 vl1 vl1" using φ1 unfolding consume_def ss1 by auto
          next
            show 1: "γ ?trn = γ ?trn1" unfolding ss1 by simp
          next
            assume "γ ?trn" hence "ou = ou1" using ouou1 by auto
            thus "g ?trn = g ?trn1" using ouou1 by (cases a) auto
          next
            show "Δ1 s' vl' s1' vl1" using a l s's1' AID' unfolding Δ1_def vl' by simp
          qed
        qed
        thus ?thesis by simp
      qed
    qed
  thus ?thesis using l by auto
  qed
qed

definition Gr where
"Gr =
 {
 (Δ0, {Δ0,Δ1}),
 (Δ1, {Δ1})
 }"


theorem Post_secure: secure
apply (rule unwind_decomp_secure_graph[of Gr Δ0])
unfolding Gr_def
apply (simp, smt insert_subset order_refl)
using istate_Δ0 unwind_cont_Δ0 unwind_cont_Δ1
unfolding Gr_def by auto


end (* context Post_RECEIVER *)

end