Theory API_Network
section ‹The CoSMeDis network of communicating nodes ›
text ‹This is the specification of an entire CoSMeDis network
of communicating nodes, as described
in Section IV.B of \<^cite>‹"cosmedis-SandP2017"›
NB: What that paper refers to as "nodes" are referred in this formalization
as "APIs".
›
theory API_Network
imports
"BD_Security_Compositional.Composing_Security_Network"
System_Specification
begin
locale Network =
fixes AIDs :: "apiID set"
assumes finite_AIDs: "finite AIDs"
begin
fun comOfO :: "apiID ⇒ (act × out) ⇒ com" where
"comOfO aid (COMact (comSendServerReq uid password aID req), ou) =
(if aid ≠ aID ∧ ou ≠ outErr then Send else Internal)"
| "comOfO aid (COMact (comConnectClient uID p aID sp), ou) =
(if aid ≠ aID ∧ ou ≠ outErr then Send else Internal)"
| "comOfO aid (COMact (comSendPost uID p aID nID), ou) =
(if aid ≠ aID ∧ ou ≠ outErr then Send else Internal)"
| "comOfO aid (COMact (comSendCreateOFriend uID p aID uID'), ou) =
(if aid ≠ aID ∧ ou ≠ outErr then Send else Internal)"
| "comOfO aid (COMact (comSendDeleteOFriend uID p aID uID'), ou) =
(if aid ≠ aID ∧ ou ≠ outErr then Send else Internal)"
| "comOfO aid (COMact (comReceiveClientReq aID req), ou) =
(if aid ≠ aID ∧ ou ≠ outErr then Recv else Internal)"
| "comOfO aid (COMact (comConnectServer aID sp), ou) =
(if aid ≠ aID ∧ ou ≠ outErr then Recv else Internal)"
| "comOfO aid (COMact (comReceivePost aID sp nID ntc uid v), ou) =
(if aid ≠ aID ∧ ou ≠ outErr then Recv else Internal)"
| "comOfO aid (COMact (comReceiveCreateOFriend aID sp uid uid'), ou) =
(if aid ≠ aID ∧ ou ≠ outErr then Recv else Internal)"
| "comOfO aid (COMact (comReceiveDeleteOFriend aID sp uid uid'), ou) =
(if aid ≠ aID ∧ ou ≠ outErr then Recv else Internal)"
| "comOfO _ _ = Internal"
fun comOf :: "apiID ⇒ (state, act, out) trans ⇒ com" where
"comOf aid (Trans _ a ou _) = comOfO aid (a, ou)"
fun syncO :: "apiID ⇒ (act × out) ⇒ apiID ⇒ (act × out) ⇒ bool" where
"syncO aid1 (COMact (comSendServerReq uid p aid req), ou1) aid2 (a2, ou2) =
(∃req2. a2 = (COMact (comReceiveClientReq aid1 req2)) ∧ ou1 = O_sendServerReq (aid2,req2) ∧ ou2 = outOK)"
| "syncO aid1 (COMact (comConnectClient uid p aid sp), ou1) aid2 (a2, ou2) =
(∃sp2. a2 = (COMact (comConnectServer aid1 sp2)) ∧ ou1 = O_connectClient (aid2,sp2) ∧ ou2 = outOK)"
| "syncO aid1 (COMact (comSendPost uid p aid nid), ou1) aid2 (a2, ou2) =
(∃sp2 nid2 ntc2 uid2 v. a2 = (COMact (comReceivePost aid1 sp2 nid2 ntc2 uid2 v)) ∧ ou1 = O_sendPost (aid2, sp2, nid2, ntc2, uid2, v) ∧ ou2 = outOK)"
| "syncO aid1 (COMact (comSendCreateOFriend uid p aid uid'), ou1) aid2 (a2, ou2) =
(∃sp2 uid2 uid2'. a2 = (COMact (comReceiveCreateOFriend aid1 sp2 uid2 uid2')) ∧ ou1 = O_sendCreateOFriend (aid2, sp2, uid2, uid2') ∧ ou2 = outOK)"
| "syncO aid1 (COMact (comSendDeleteOFriend uid p aid uid'), ou1) aid2 (a2, ou2) =
(∃sp2 uid2 uid2'. a2 = (COMact (comReceiveDeleteOFriend aid1 sp2 uid2 uid2')) ∧ ou1 = O_sendDeleteOFriend (aid2, sp2, uid2, uid2') ∧ ou2 = outOK)"
| "syncO _ _ _ _ = False"
fun cmpO :: "apiID ⇒ (act × out) ⇒ apiID ⇒ (act × out) ⇒ (apiID × act × out × apiID × act × out)" where
"cmpO aid1 obs1 aid2 obs2 = (aid1, fst obs1, snd obs1, aid2, fst obs2, snd obs2)"
fun sync :: "apiID ⇒ (state, act, out) trans ⇒ apiID ⇒ (state, act, out) trans ⇒ bool" where
"sync aid1 (Trans s1 a1 ou1 s1') aid2 (Trans s2 a2 ou2 s2') = syncO aid1 (a1, ou1) aid2 (a2, ou2)"
lemma syncO_cases:
assumes "syncO aid1 obs1 aid2 obs2"
obtains
(Req) uid p aid req1 req2
where "obs1 = (COMact (comSendServerReq uid p aid req1), O_sendServerReq (aid2,req2))"
and "obs2 = (COMact (comReceiveClientReq aid1 req2), outOK)"
| (Connect) uid p aid sp sp2
where "obs1 = (COMact (comConnectClient uid p aid sp), O_connectClient (aid2,sp2))"
and "obs2 = (COMact (comConnectServer aid1 sp2), outOK)"
| (Notice) uid p aid nid sp2 nid2 ntc2 own2 v
where "obs1 = (COMact (comSendPost uid p aid nid), O_sendPost (aid2, sp2, nid2, ntc2, own2, v))"
and "obs2 = (COMact (comReceivePost aid1 sp2 nid2 ntc2 own2 v), outOK)"
| (CFriend) uid p aid uid' sp2 uid2 uid2'
where "obs1 = (COMact (comSendCreateOFriend uid p aid uid'), O_sendCreateOFriend (aid2, sp2, uid2, uid2'))"
and "obs2 = (COMact (comReceiveCreateOFriend aid1 sp2 uid2 uid2'), outOK)"
| (DFriend) uid p aid uid' sp2 uid2 uid2'
where "obs1 = (COMact (comSendDeleteOFriend uid p aid uid'), O_sendDeleteOFriend (aid2, sp2, uid2, uid2'))"
and "obs2 = (COMact (comReceiveDeleteOFriend aid1 sp2 uid2 uid2'), outOK)"
using assms by (cases "(aid1,obs1,aid2,obs2)" rule: syncO.cases) auto
lemma sync_cases:
assumes "sync aid1 trn1 aid2 trn2"
and "validTrans trn1"
obtains
(Req) uid p aid req s1 s1' s2 s2'
where "trn1 = Trans s1 (COMact (comSendServerReq uid p aid req)) (O_sendServerReq (aid2,req)) s1'"
and "trn2 = Trans s2 (COMact (comReceiveClientReq aid1 req)) outOK s2'"
| (Connect) uid p aid sp s1 s1' s2 s2'
where "trn1 = Trans s1 (COMact (comConnectClient uid p aid sp)) (O_connectClient (aid2,sp)) s1'"
and "trn2 = Trans s2 (COMact (comConnectServer aid1 sp)) outOK s2'"
| (Notice) uid p aid nid sp2 nid2 ntc2 own2 v s1 s1' s2 s2'
where "trn1 = Trans s1 (COMact (comSendPost uid p aid nid)) (O_sendPost (aid2, sp2, nid2, ntc2, own2, v)) s1'"
and "trn2 = Trans s2 (COMact (comReceivePost aid1 sp2 nid2 ntc2 own2 v)) outOK s2'"
| (CFriend) uid p uid' sp s1 s1' s2 s2'
where "trn1 = Trans s1 (COMact (comSendCreateOFriend uid p aid2 uid')) (O_sendCreateOFriend (aid2, sp, uid, uid')) s1'"
and "trn2 = Trans s2 (COMact (comReceiveCreateOFriend aid1 sp uid uid')) outOK s2'"
| (DFriend) uid p aid uid' sp s1 s1' s2 s2'
where "trn1 = Trans s1 (COMact (comSendDeleteOFriend uid p aid2 uid')) (O_sendDeleteOFriend (aid2, sp, uid, uid')) s1'"
and "trn2 = Trans s2 (COMact (comReceiveDeleteOFriend aid1 sp uid uid')) outOK s2'"
using assms
by (cases trn1; cases trn2) (auto elim!: syncO_cases simp: com_defs split: if_splits)
fun tgtNodeOfO :: "apiID ⇒ (act × out) ⇒ apiID" where
"tgtNodeOfO _ (COMact (comSendServerReq uID p aID reqInfo), ou) = aID"
| "tgtNodeOfO _ (COMact (comReceiveClientReq aID reqInfo), ou) = aID"
| "tgtNodeOfO _ (COMact (comConnectClient uID p aID sp), ou) = aID"
| "tgtNodeOfO _ (COMact (comConnectServer aID sp), ou) = aID"
| "tgtNodeOfO _ (COMact (comSendPost uID p aID nID), ou) = aID"
| "tgtNodeOfO _ (COMact (comReceivePost aID sp nID title text v), ou) = aID"
| "tgtNodeOfO _ (COMact (comSendCreateOFriend uID p aID uID'), ou) = aID"
| "tgtNodeOfO _ (COMact (comReceiveCreateOFriend aID sp uid uid'), ou) = aID"
| "tgtNodeOfO _ (COMact (comSendDeleteOFriend uID p aID uID'), ou) = aID"
| "tgtNodeOfO _ (COMact (comReceiveDeleteOFriend aID sp uid uid'), ou) = aID"
| "tgtNodeOfO _ _ = undefined"
fun tgtNodeOf :: "apiID ⇒ (state, act, out) trans ⇒ apiID" where
"tgtNodeOf _ (Trans s (COMact (comSendServerReq uID p aID reqInfo)) ou s') = aID"
| "tgtNodeOf _ (Trans s (COMact (comReceiveClientReq aID reqInfo)) ou s') = aID"
| "tgtNodeOf _ (Trans s (COMact (comConnectClient uID p aID sp)) ou s') = aID"
| "tgtNodeOf _ (Trans s (COMact (comConnectServer aID sp)) ou s') = aID"
| "tgtNodeOf _ (Trans s (COMact (comSendPost uID p aID nID)) ou s') = aID"
| "tgtNodeOf _ (Trans s (COMact (comReceivePost aID sp nID title text v)) ou s') = aID"
| "tgtNodeOf _ (Trans s (COMact (comSendCreateOFriend uID p aID uID')) ou s') = aID"
| "tgtNodeOf _ (Trans s (COMact (comReceiveCreateOFriend aID sp uid uid')) ou s') = aID"
| "tgtNodeOf _ (Trans s (COMact (comSendDeleteOFriend uID p aID uID')) ou s') = aID"
| "tgtNodeOf _ (Trans s (COMact (comReceiveDeleteOFriend aID sp uid uid')) ou s') = aID"
| "tgtNodeOf _ _ = undefined"
abbreviation validTrans :: "apiID ⇒ (state, act, out) trans ⇒ bool" where
"validTrans aid ≡ System_Specification.validTrans"
sublocale TS_Network
where istate = "λ_. istate" and validTrans = validTrans and srcOf = "λ_. srcOf" and tgtOf = "λ_. tgtOf"
and nodes = AIDs and comOf = comOf and tgtNodeOf = tgtNodeOf
and sync = sync
proof (unfold_locales, goal_cases)
case (1) show ?case using finite_AIDs . next
case (2 aid trn)
from 2 show ?case
by (cases "(aid, trn)" rule: tgtNodeOf.cases) auto
qed
end
end