Theory Post_RECEIVER
theory Post_RECEIVER
imports
"Bounded_Deducibility_Security.Compositional_Reasoning"
"Post_Observation_Setup_RECEIVER"
"Post_Value_Setup_RECEIVER"
begin
subsubsection ‹Declassification bound›
text ‹We verify that a group of users of some node ‹i›,
allowed to take normal actions to the system and observe their outputs
\emph{and additionally allowed to observe communication},
can learn nothing about the updates to a post received from a remote node ‹j›
beyond the number of updates
unless:
\begin{itemize}
\item either a user in the group is the administrator
\item or a user in the group becomes a remote friend of the post's owner
\item or the group has at least one registered user and the post is being marked as "public"
\end{itemize}
See \<^cite>‹"cosmedis-SandP2017"› for more details.
›
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 ‹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)
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_actions[OF ss1]
eqButPID_update[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 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 ≡ COMact (comReceivePost AID p PID pst1 uid vs)" note a1 = this
obtain s1' where step1: "step s1 a1 = (outOK, s1')" using AID1 unfolding a1_def 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 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
end