Session CoSMeDis

iv class="head">

Theory Prelim

section ‹Preliminaries›

theory Prelim
  imports
    "Fresh_Identifiers.Fresh_String"
    "Bounded_Deducibility_Security.Trivia"
begin


subsection ‹The basic types›

(*  This version of string is needed for code generation: *)
definition "emptyStr = STR ''''"

(* The users of the system: *)


datatype name = Nam String.literal
definition "emptyName ≡ Nam emptyStr"
datatype inform = Info String.literal
definition "emptyInfo ≡ Info emptyStr"

datatype user = Usr name inform
fun nameUser where "nameUser (Usr name info) = name"
fun infoUser where "infoUser (Usr name info) = info"
definition "emptyUser ≡ Usr emptyName emptyInfo"

typedecl raw_data
code_printing type_constructor raw_data ⇀ (Scala) "java.io.File"

(* Images (currently, pdf, to be changed): *)
datatype img  = emptyImg | Imag raw_data
(* Visibility outside the current api: either friends-only or public
 (i.e., exportable outside to the other apis): *)
datatype vis = Vsb String.literal
(* Accepted values: friend and public  *)
abbreviation "FriendV ≡ Vsb (STR ''friend'')"
(* abbreviation "InternalV ≡ Vsb (STR ''internal'')" *)
abbreviation "PublicV ≡ Vsb (STR ''public'')"
fun stringOfVis where "stringOfVis (Vsb str) = str"

(* A post consists of a string for title, a string for its text,
  a (possibly empty) image and a visibility specification: *)

datatype title = Tit String.literal
definition "emptyTitle ≡ Tit emptyStr"
datatype "text" = Txt String.literal
definition "emptyText ≡ Txt emptyStr"

datatype post = Pst title "text" img (* vis *)
(* Getters: *)
fun titlePost where "titlePost (Pst title text img) = title"
fun textPost where "textPost (Pst title text img) = text"
fun imgPost where "imgPost (Pst title text img) = img"
(* fun visPost where "visPost (Pst title text img vis) = vis" *)
(* Setters: *)
fun setTitlePost where "setTitlePost (Pst title text img) title' = Pst title' text img"
fun setTextPost where "setTextPost(Pst title text img) text' = Pst title text' img"
fun setImgPost where "setImgPost (Pst title text img) img' = Pst title text img'"
(* fun setVisPost where "setVisPost (Pst title text img vis) vis' = Pst title text img vis'" *)
(*  *)
definition emptyPost :: post where
"emptyPost ≡ Pst emptyTitle emptyText emptyImg" (*  FriendV" *)
(* initially set to the lowest visibility: friend *)

lemma titlePost_emptyPost[simp]: "titlePost emptyPost = emptyTitle"
and textPost_emptyPost[simp]: "textPost emptyPost = emptyText"
and imgPost_emptyPost[simp]: "imgPost emptyPost = emptyImg"
(* and visPost_emptyPost[simp]: "visPost emptyPost = FriendV" *)
unfolding emptyPost_def by simp_all

lemma set_get_post[simp]:
"titlePost (setTitlePost ntc title) = title"
"titlePost (setTextPost ntc text) = titlePost ntc"
"titlePost (setImgPost ntc img) = titlePost ntc"
(* "titlePost (setVisPost ntc vis) = titlePost ntc" *)
(* *)
"textPost (setTitlePost ntc title) = textPost ntc"
"textPost (setTextPost ntc text) = text"
"textPost (setImgPost ntc img) = textPost ntc"
(* "textPost (setVisPost ntc vis) = textPost ntc" *)
(* *)
"imgPost (setTitlePost ntc title) = imgPost ntc"
"imgPost (setTextPost ntc text) = imgPost ntc"
"imgPost (setImgPost ntc img) = img"
(* "imgPost (setVisPost ntc vis) = imgPost ntc" *)
(* *)
(*
"visPost (setTitlePost ntc title) = visPost ntc"
"visPost (setTextPost ntc text) = visPost ntc"
"visPost (setImgPost ntc img) = visPost ntc"
"visPost (setVisPost ntc vis) = vis"
*)
(* *)
by(cases ntc, auto)+

lemma setTextPost_absorb[simp]:
"setTitlePost (setTitlePost pst tit) tit1 = setTitlePost pst tit1"
"setTextPost (setTextPost pst txt) txt1 = setTextPost pst txt1"
"setImgPost (setImgPost pst img) img1 = setImgPost pst img1"
(* "setVisPost (setVisPost pst vis) vis1 = setVisPost pst vis1" *)
by (cases pst, auto)+

datatype password = Psw String.literal
definition "emptyPass ≡ Psw emptyStr"

datatype salt = Slt String.literal
definition "emptySalt ≡ Slt emptyStr"

(* Information associated to requests for registration: both for users and apis *)
datatype requestInfo = ReqInfo String.literal
definition "emptyRequestInfo ≡ ReqInfo emptyStr"


subsection ‹Identifiers›

datatype apiID = Aid String.literal
datatype userID = Uid String.literal
datatype postID = Pid String.literal

definition "emptyApiID ≡ Aid emptyStr"
definition "emptyUserID ≡ Uid emptyStr"
definition "emptyPostID ≡ Pid emptyStr"

(*  *)
fun apiIDAsStr where "apiIDAsStr (Aid str) = str"

definition "getFreshApiID apiIDs ≡ Aid (fresh (set (map apiIDAsStr apiIDs)) (STR ''1''))"

lemma ApiID_apiIDAsStr[simp]: "Aid (apiIDAsStr apiID) = apiID"
by (cases apiID) auto

lemma member_apiIDAsStr_iff[simp]: "str ∈ apiIDAsStr ` apiIDs ⟷ Aid str ∈ apiIDs"
by (metis ApiID_apiIDAsStr image_iff apiIDAsStr.simps)

lemma getFreshApiID: "¬ getFreshApiID apiIDs ∈∈ apiIDs"
using fresh_notIn[of "set (map apiIDAsStr apiIDs)"] unfolding getFreshApiID_def by auto

(*  *)
fun userIDAsStr where "userIDAsStr (Uid str) = str"

definition "getFreshUserID userIDs ≡ Uid (fresh (set (map userIDAsStr userIDs)) (STR ''2''))"

lemma UserID_userIDAsStr[simp]: "Uid (userIDAsStr userID) = userID"
by (cases userID) auto

lemma member_userIDAsStr_iff[simp]: "str ∈ userIDAsStr ` (set userIDs) ⟷ Uid str ∈∈ userIDs"
by (metis UserID_userIDAsStr image_iff userIDAsStr.simps)

lemma getFreshUserID: "¬ getFreshUserID userIDs ∈∈ userIDs"
using fresh_notIn[of "set (map userIDAsStr userIDs)"] unfolding getFreshUserID_def by auto

(*  *)
fun postIDAsStr where "postIDAsStr (Pid str) = str"

definition "getFreshPostID postIDs ≡ Pid (fresh (set (map postIDAsStr postIDs)) (STR ''3''))"

lemma PostID_postIDAsStr[simp]: "Pid (postIDAsStr postID) = postID"
by (cases postID) auto

lemma member_postIDAsStr_iff[simp]: "str ∈ postIDAsStr ` (set postIDs) ⟷ Pid str ∈∈ postIDs"
by (metis PostID_postIDAsStr image_iff postIDAsStr.simps)

lemma getFreshPostID: "¬ getFreshPostID postIDs ∈∈ postIDs"
using fresh_notIn[of "set (map postIDAsStr postIDs)"] unfolding getFreshPostID_def by auto

end
d>

Theory System_Specification

section ‹The CoSMeDis single node specification›

text ‹This is the specification of a CoSMeDis node, as described
in Sections II and IV.B of \cite{cosmedis-SandP2017}.
NB: What that paper refers to as "nodes" are referred in this formalization
as "APIs".

A CoSMeDis node extends CoSMed \cite{cosmed-itp2016,cosmed-jar2018,cosmed-AFP}
with inter-node communication actions.
›

theory System_Specification
  imports
    Prelim
    "Bounded_Deducibility_Security.IO_Automaton"
begin

text ‹An aspect not handled in this specification is the uniqueness of the node IDs. These
are assumed to be handled externally as follows: a node ID is an URI, and therefore is unique.›

declare List.insert[simp]

subsection ‹The state›

record state =
  admin :: userID
  (*  *)
  pendingUReqs :: "userID list"
  userReq :: "userID ⇒ requestInfo"
  userIDs :: "userID list"
  user :: "userID ⇒ user"
  pass :: "userID ⇒ password"
  (*  *)
  pendingFReqs :: "userID ⇒ userID list"
  friendReq :: "userID ⇒ userID ⇒ requestInfo"
  friendIDs :: "userID ⇒ userID list"
  (* Outer friendship, i.e., friendship with users of other (server) APIs. This will effectively
     mean access to the friend-only outer posts retrieved from that server.
     There are two lists:
      - friendship authorizations sent by users of this API, and
      - friendship authorizations received from other APIs. *)
  sentOuterFriendIDs :: "userID ⇒ (apiID × userID) list"
  recvOuterFriendIDs :: "userID ⇒ (apiID × userID) list"
  (*  *)
  postIDs :: "postID list"
  post :: "postID ⇒ post"
  owner :: "postID ⇒ userID"
  vis :: "postID ⇒ vis"
  (* The server-api IDs represents the apis whose posts can be read by this api. *)
  (* The following setting ensures that clashes on post IDs from different apis are harmless: *)
  (* Pending request sent by this API to other APIs with the wish that they become servers (and the current API
       becomes their client); this has to be approved by the respective APIs *)
  pendingSApiReqs :: "apiID list"
  sApiReq :: "apiID ⇒ requestInfo"
  serverApiIDs :: "apiID list"
  (* Password (key) to be used (by both parties) for communication with each server API. *)
  serverPass :: "apiID ⇒ password"
  outerPostIDs :: "apiID ⇒ postID list"
  outerPost :: "apiID ⇒ postID ⇒ post"
  outerOwner :: "apiID ⇒ postID ⇒ userID"
  outerVis :: "apiID ⇒ postID ⇒ vis"
  (*  *)
  (* The client-api IDs represents the apis that can read this api's posts *)
  (* Pending requests from APIs that want to become clients; this has to be approved by the admin *)
  pendingCApiReqs :: "apiID list"
  cApiReq :: "apiID ⇒ requestInfo"
  clientApiIDs :: "apiID list"
  (* Password (key) to be used (by both parties) for communication with each client API. *)
  clientPass :: "apiID ⇒ password"
  sharedWith :: "postID ⇒ (apiID × bool) list"
  (* for a post, stores the client apis with which the post was shared together with a boolean flag
     indicating whether the version the api has is up-to-date *)

(* The api IDs will be the URLs of the corresponding APIs *)
(* Note that only the client APIs need a password -- the server API are themselves contacted by this API. *)

(* Note that IDsOK refers only to the registered users, posts, server APIs and their served outerPosts,
and client apis. It does not refer to user IDs or api IDs contained in any pending requests.
*)
definition IDsOK :: "state ⇒ userID list ⇒ postID list ⇒ (apiID × postID list) list ⇒ apiID list ⇒ bool"
where
"IDsOK s uIDs pIDs saID_pIDs_s caIDs ≡
 list_all (λ uID. uID ∈∈ userIDs s) uIDs ∧
 list_all (λ pID. pID ∈∈ postIDs s) pIDs ∧
 list_all (λ (aID,pIDs). aID ∈∈ serverApiIDs s ∧
 list_all (λ pID. pID ∈∈ outerPostIDs s aID) pIDs) saID_pIDs_s ∧
 list_all (λ aID. aID ∈∈ clientApiIDs s) caIDs"


subsection ‹The actions›

subsubsection ‹Initialization of the system›


definition istate :: state
where
"istate ≡
 ⦇
  admin = emptyUserID,

  pendingUReqs = [],
  userReq = (λ uID. emptyRequestInfo),
  userIDs = [],
  user = (λ uID. emptyUser),
  pass = (λ uID. emptyPass),

  pendingFReqs = (λ uID. []),
  friendReq = (λ uID uID'. emptyRequestInfo),
  friendIDs = (λ uID. []),

  sentOuterFriendIDs = (λ uID. []),
  recvOuterFriendIDs = (λ uID. []),

  postIDs = [],
  post = (λ papID. emptyPost),
  owner = (λ pID. emptyUserID),
  vis = (λ pID. FriendV),

  pendingSApiReqs = [],
  sApiReq = (λ aID. emptyRequestInfo),
  serverApiIDs = [],
  serverPass = (λ aID. emptyPass),
  outerPostIDs = (λ aID. []),
  outerPost = (λ aID papID. emptyPost),
  outerOwner = (λ aID papID. emptyUserID),
  outerVis = (λ aID pID. FriendV),

  pendingCApiReqs = [],
  cApiReq = (λ aID. emptyRequestInfo),
  clientApiIDs = [],
  clientPass = (λ aID. emptyPass),
  sharedWith = (λpID. [])
 ⦈"


subsubsection ‹Starting action›

(* This initiates the current api. It has the following parameters:
  -- uID, p, name: the admin user id, name and password
*)
definition startSys ::
"state ⇒ userID ⇒ password ⇒ state"
where
"startSys s uID p ≡
 s ⦇admin := uID,
    userIDs := [uID],
    user := (user s) (uID := emptyUser),
    pass := (pass s) (uID := p)⦈"

definition e_startSys :: "state ⇒ userID ⇒ password ⇒  bool"
where
"e_startSys s uID p ≡ userIDs s = []"


subsubsection ‹Creation actions›


(* Create new user request: we allow users to choose their own IDs; they could be their email addresses. *)
definition createNUReq :: "state ⇒ userID ⇒ requestInfo ⇒ state"
where
"createNUReq s uID reqInfo ≡
 s ⦇pendingUReqs := pendingUReqs s @ [uID],
    userReq := (userReq s)(uID := reqInfo)
⦈"

definition e_createNUReq :: "state ⇒ userID ⇒ requestInfo ⇒ bool"
where
"e_createNUReq s uID requestInfo ≡
 admin s ∈∈ userIDs s ∧ ¬ uID ∈∈ userIDs s ∧ ¬ uID ∈∈ pendingUReqs s"
(* a new-user request can be created only if the api has started, i.e., if an admin exists *)

(* The admin actually creates a user by approving a pending new-user request.
E.g., the admin can add an  arbitrary password and send it by email to that user.
Then the user can change his password. *)
definition createUser :: "state ⇒ userID ⇒ password ⇒ userID ⇒ password ⇒ state"
where
"createUser s uID p uID' p' ≡
 s ⦇userIDs := uID' # (userIDs s),
    user := (user s) (uID' := emptyUser),
    pass := (pass s) (uID' := p'),
    pendingUReqs := remove1 uID' (pendingUReqs s),
    userReq := (userReq s)(uID := emptyRequestInfo)⦈"

definition e_createUser :: "state ⇒ userID ⇒ password ⇒ userID ⇒ password ⇒ bool"
where
"e_createUser s uID p uID' p' ≡
 IDsOK s [uID] [] [] [] ∧ pass s uID = p ∧ uID = admin s ∧ uID' ∈∈ pendingUReqs s"


(* Create post: note that post ID is an action parameter, and that the enabledness action
checks that it is fresh.
The API's interface will actually generate it, using getFresh. *)
definition createPost :: "state ⇒ userID ⇒ password ⇒ postID ⇒ state"
where
"createPost s uID p pID ≡
 s ⦇postIDs := pID # postIDs s,
    post := (post s) (pID := emptyPost),
    owner := (owner s) (pID := uID)⦈"
(* Recall from the initial state that the initial visibility is FriendV *)

definition e_createPost :: "state ⇒ userID ⇒ password ⇒ postID ⇒ bool"
where
"e_createPost s uID p pID ≡
 IDsOK s [uID] [] [] [] ∧ pass s uID = p ∧
 ¬ pID ∈∈ postIDs s"

(* Friendship: *)
(* Create friend request, namely uID Reqs friendship of uID': *)
definition createFriendReq :: "state ⇒ userID ⇒ password ⇒ userID ⇒ requestInfo ⇒ state"
where
"createFriendReq s uID p uID' req ≡
 let pfr = pendingFReqs s in
 s ⦇pendingFReqs := pfr (uID' := pfr uID' @ [uID]),
    friendReq := fun_upd2 (friendReq s) uID uID' req⦈"

definition e_createFriendReq :: "state ⇒ userID ⇒ password ⇒ userID ⇒ requestInfo ⇒ bool"
where
"e_createFriendReq s uID p uID' req ≡
 IDsOK s [uID,uID'] [] [] [] ∧ pass s uID = p ∧
 ¬ uID ∈∈ pendingFReqs s uID' ∧ ¬ uID ∈∈ friendIDs s uID'"

(* Create friend, by approving a friend request (namely uID approves the request from uID').
Friendship is symmetric, hence the two updates to "friend";
also, the friendship request is canceled upon approval.  *)
definition createFriend :: "state ⇒ userID ⇒ password ⇒ userID ⇒ state"
where
"createFriend s uID p uID' ≡
 let fr = friendIDs s; pfr = pendingFReqs s in
 s ⦇friendIDs := fr (uID := fr uID @ [uID'], uID' := fr uID' @ [uID]),
    pendingFReqs := pfr (uID := remove1 uID' (pfr uID), uID' := remove1 uID (pfr uID')),
    friendReq := fun_upd2 (fun_upd2 (friendReq s) uID' uID emptyRequestInfo) uID uID' emptyRequestInfo⦈"

definition e_createFriend :: "state ⇒ userID ⇒ password ⇒ userID ⇒ bool"
where
"e_createFriend s uID p uID' ≡
 IDsOK s [uID,uID'] [] [] [] ∧ pass s uID = p ∧
 uID' ∈∈ pendingFReqs s uID"


subsubsection ‹Deletion (removal) actions›

(* Delete friend:   *)
definition deleteFriend :: "state ⇒ userID ⇒ password ⇒ userID ⇒ state"
where
"deleteFriend s uID p uID' ≡
 let fr = friendIDs s in
 s ⦇friendIDs := fr (uID := removeAll uID' (fr uID), uID' := removeAll uID (fr uID'))⦈"


definition e_deleteFriend :: "state ⇒ userID ⇒ password ⇒ userID ⇒ bool"
where
"e_deleteFriend s uID p uID' ≡
 IDsOK s [uID,uID'] [] [] [] ∧ pass s uID = p ∧
 uID' ∈∈ friendIDs s uID"


subsubsection ‹Updating actions›

(* Users can update their passwords and names: *)
definition updateUser :: "state ⇒ userID ⇒ password ⇒ password ⇒ name ⇒ inform ⇒ state"
where
"updateUser s uID p p' name info ≡
 s ⦇user := (user s) (uID := Usr name info),
    pass := (pass s) (uID := p')⦈"

definition e_updateUser :: "state ⇒ userID ⇒ password ⇒ password ⇒ name ⇒ inform ⇒ bool"
where
"e_updateUser s uID p p' name info ≡
 IDsOK s [uID] [] [] [] ∧ pass s uID = p"

definition updatePost :: "state ⇒ userID ⇒ password ⇒ postID ⇒ post ⇒ state"
where
"updatePost s uID p pID pst ≡
 let sW = sharedWith s in
 s ⦇post := (post s) (pID := pst),
    sharedWith := sW (pID := map (λ (aID,_). (aID,False)) (sW pID))⦈"

definition e_updatePost :: "state ⇒ userID ⇒ password ⇒ postID ⇒ post ⇒ bool"
where
"e_updatePost s uID p pID pst ≡
 IDsOK s [uID] [pID] [] [] ∧ pass s uID = p ∧
 owner s pID = uID"

definition updateVisPost :: "state ⇒ userID ⇒ password ⇒ postID ⇒ vis ⇒ state"
where
"updateVisPost s uID p pID vs ≡
 s ⦇vis := (vis s) (pID := vs)⦈"

definition e_updateVisPost :: "state ⇒ userID ⇒ password ⇒ postID ⇒ vis ⇒ bool"
where
"e_updateVisPost s uID p pID vs ≡
 IDsOK s [uID] [pID] [] [] ∧ pass s uID = p ∧
 owner s pID = uID ∧ vs ∈ {FriendV, PublicV}"

(* Note: Of course, the outer posts cannot be updated from this API. *)


subsubsection ‹Reading actions›

(* Read new user request: *)
definition readNUReq :: "state ⇒ userID ⇒ password ⇒ userID ⇒ requestInfo"
where
"readNUReq s uID p uID' ≡ userReq s uID'"

definition e_readNUReq :: "state ⇒ userID ⇒ password ⇒ userID ⇒ bool"
where
"e_readNUReq s uID p uID' ≡
 IDsOK s [uID] [] [] [] ∧ pass s uID = p ∧
 uID = admin s ∧ uID' ∈∈ pendingUReqs s"

(* A user can read their name (and so can all the other users), but not the password: *)
definition readUser :: "state ⇒ userID ⇒ password ⇒ userID ⇒ name"
where
"readUser s uID p uID' ≡ nameUser (user s uID')"

definition e_readUser :: "state ⇒ userID ⇒ password ⇒ userID ⇒ bool"
where
"e_readUser s uID p uID' ≡
 IDsOK s [uID,uID'] [] [] [] ∧ pass s uID = p"

(* A user can check if he is the admin: *)
definition readAmIAdmin :: "state ⇒ userID ⇒ password ⇒ bool"
where
"readAmIAdmin s uID p ≡ uID = admin s"

definition e_readAmIAdmin :: "state ⇒ userID ⇒ password ⇒ bool"
where
"e_readAmIAdmin s uID p ≡
 IDsOK s [uID] [] [] [] ∧ pass s uID = p"

(* Reading posts: *)

definition readPost :: "state ⇒ userID ⇒ password ⇒ postID ⇒ post"
where
"readPost s uID p pID ≡ post s pID"

definition e_readPost :: "state ⇒ userID ⇒ password ⇒ postID ⇒ bool"
where
"e_readPost s uID p pID ≡
 IDsOK s [uID] [pID] [] [] ∧ pass s uID = p ∧
 (owner s pID = uID ∨ uID ∈∈ friendIDs s (owner s pID) ∨ vis s pID = PublicV)"

definition readOwnerPost :: "state ⇒ userID ⇒ password ⇒ postID ⇒ userID"
where
"readOwnerPost s uID p pID ≡ owner s pID"

definition e_readOwnerPost :: "state ⇒ userID ⇒ password ⇒ postID ⇒ bool"
where
"e_readOwnerPost s uID p pID ≡
 IDsOK s [uID] [pID] [] [] ∧ pass s uID = p ∧
 (admin s = uID ∨ owner s pID = uID ∨ uID ∈∈ friendIDs s (owner s pID) ∨ vis s pID = PublicV)"

definition readVisPost :: "state ⇒ userID ⇒ password ⇒ postID ⇒ vis"
where
"readVisPost s uID p pID ≡ vis s pID"

definition e_readVisPost :: "state ⇒ userID ⇒ password ⇒ postID ⇒ bool"
where
"e_readVisPost s uID p pID ≡
 IDsOK s [uID] [pID] [] [] ∧ pass s uID = p ∧
 (admin s = uID ∨ owner s pID = uID ∨ uID ∈∈ friendIDs s (owner s pID) ∨ vis s pID = PublicV)"

(* Reading outer posts: *)

definition readOPost :: "state ⇒ userID ⇒ password ⇒ apiID ⇒ postID ⇒ post"
where
"readOPost s uID p aID pID ≡ outerPost s aID pID"

definition e_readOPost :: "state ⇒ userID ⇒ password ⇒ apiID ⇒ postID ⇒ bool"
where
"e_readOPost s uID p aID pID ≡
 IDsOK s [uID] [] [(aID,[pID])] [] ∧ pass s uID = p ∧
 (admin s = uID ∨ (aID,outerOwner s aID pID) ∈∈ recvOuterFriendIDs s uID ∨ outerVis s aID pID = PublicV)"

definition readOwnerOPost :: "state ⇒ userID ⇒ password ⇒ apiID ⇒ postID ⇒ userID"
where
"readOwnerOPost s uID p aID pID ≡ outerOwner s aID pID"

definition e_readOwnerOPost :: "state ⇒ userID ⇒ password ⇒ apiID ⇒ postID ⇒ bool"
where
"e_readOwnerOPost s uID p aID pID ≡
 IDsOK s [uID] [] [(aID,[pID])] [] ∧ pass s uID = p ∧
 (admin s = uID ∨ (aID,outerOwner s aID pID) ∈∈ recvOuterFriendIDs s uID ∨ outerVis s aID pID = PublicV)"

definition readVisOPost :: "state ⇒ userID ⇒ password ⇒ apiID ⇒ postID ⇒ vis"
where
"readVisOPost s uID p aID pID ≡ outerVis s aID pID"

definition e_readVisOPost :: "state ⇒ userID ⇒ password ⇒ apiID ⇒ postID ⇒ bool"
where
"e_readVisOPost s uID p aID pID ≡
 let post = outerPost s aID pID in
 IDsOK s [uID] [] [(aID,[pID])] [] ∧ pass s uID = p ∧
 (admin s = uID ∨ (aID,outerOwner s aID pID) ∈∈ recvOuterFriendIDs s uID ∨
  outerVis s aID pID = PublicV)"



(* Friendship: *)
(* Read friendship request to me: *)
definition readFriendReqToMe :: "state ⇒ userID ⇒ password ⇒ userID ⇒ requestInfo"
where
"readFriendReqToMe s uID p uID' ≡ friendReq s uID' uID"

definition e_readFriendReqToMe :: "state ⇒ userID ⇒ password ⇒ userID ⇒ bool"
where
"e_readFriendReqToMe s uID p uID' ≡
 IDsOK s [uID,uID'] [] [] [] ∧ pass s uID = p ∧
 uID' ∈∈ pendingFReqs s uID"

(* Read friendship request from me: *)
definition readFriendReqFromMe :: "state ⇒ userID ⇒ password ⇒ userID ⇒ requestInfo"
where
"readFriendReqFromMe s uID p uID' ≡ friendReq s uID uID'"

definition e_readFriendReqFromMe :: "state ⇒ userID ⇒ password ⇒ userID ⇒ bool"
where
"e_readFriendReqFromMe s uID p uID' ≡
 IDsOK s [uID,uID'] [] [] [] ∧ pass s uID = p ∧
 uID ∈∈ pendingFReqs s uID'"

(* Read request posted to a desired server api: *)
definition readSApiReq :: "state ⇒ userID ⇒ password ⇒ apiID ⇒ requestInfo"
where
"readSApiReq s uID p uID' ≡ sApiReq s uID'"

definition e_readSApiReq :: "state ⇒ userID ⇒ password ⇒ apiID ⇒ bool"
where
"e_readSApiReq s uID p uID' ≡
 IDsOK s [uID] [] [] [] ∧ pass s uID = p ∧
 uID = admin s ∧ uID' ∈∈ pendingSApiReqs s"

(* Read request from possible client api: *)
definition readCApiReq :: "state ⇒ userID ⇒ password ⇒ apiID ⇒ requestInfo"
where
"readCApiReq s uID p uID' ≡ cApiReq s uID'"

definition e_readCApiReq :: "state ⇒ userID ⇒ password ⇒ apiID ⇒ bool"
where
"e_readCApiReq s uID p uID' ≡
 IDsOK s [uID] [] [] [] ∧ pass s uID = p ∧
 uID = admin s ∧ uID' ∈∈ pendingCApiReqs s"


subsubsection ‹Listing actions›

(* list pending new user Reqs: *)
definition listPendingUReqs :: "state ⇒ userID ⇒ password ⇒ userID list"
where
"listPendingUReqs s uID p ≡ pendingUReqs s"

definition e_listPendingUReqs :: "state ⇒ userID ⇒ password ⇒ bool"
where
"e_listPendingUReqs s uID p ≡
 IDsOK s [uID] [] [] [] ∧ pass s uID = p ∧ uID = admin s"

(* list all users of the system: *)
definition listAllUsers :: "state ⇒ userID ⇒ password ⇒ userID list"
where
"listAllUsers s uID p ≡ userIDs s"

definition e_listAllUsers :: "state ⇒ userID ⇒ password ⇒ bool"
where
"e_listAllUsers s uID p ≡ IDsOK s [uID] [] [] [] ∧ pass s uID = p"

(* List a user's friends: *)
definition listFriends :: "state ⇒ userID ⇒ password ⇒ userID ⇒ userID list"
where
"listFriends s uID p uID' ≡ friendIDs s uID'"

definition e_listFriends :: "state ⇒ userID ⇒ password ⇒ userID ⇒ bool"
where
"e_listFriends s uID p uID' ≡
 IDsOK s [uID,uID'] [] [] [] ∧ pass s uID = p ∧
 (uID = uID' ∨ uID ∈∈ friendIDs s uID')"

(* List the outer friendship authorizations sent by a user: *)
definition listSentOuterFriends :: "state ⇒ userID ⇒ password ⇒ userID ⇒ (apiID × userID) list"
where
"listSentOuterFriends s uID p uID' ≡ sentOuterFriendIDs s uID'"

definition e_listSentOuterFriends :: "state ⇒ userID ⇒ password ⇒ userID ⇒ bool"
where
"e_listSentOuterFriends s uID p uID' ≡
 IDsOK s [uID,uID'] [] [] [] ∧ pass s uID = p ∧
 (uID = uID' ∨ uID ∈∈ friendIDs s uID')"

(* List the outer friendship authorizations received by a user: *)
definition listRecvOuterFriends :: "state ⇒ userID ⇒ password ⇒ (apiID × userID) list"
where
"listRecvOuterFriends s uID p ≡ recvOuterFriendIDs s uID"

definition e_listRecvOuterFriends :: "state ⇒ userID ⇒ password ⇒ bool"
where
"e_listRecvOuterFriends s uID p ≡
 IDsOK s [uID] [] [] [] ∧ pass s uID = p"

(* list posts internal to the api: *)
definition listInnerPosts :: "state ⇒ userID ⇒ password ⇒ (userID × postID) list"
where
"listInnerPosts s uID p ≡
  [(owner s pID, pID).
    pID ← postIDs s,
    vis s pID ≠ FriendV ∨ uID ∈∈ friendIDs s (owner s pID) ∨ uID = owner s pID
  ]"

definition e_listInnerPosts :: "state ⇒ userID ⇒ password ⇒ bool"
where
"e_listInnerPosts s uID p ≡ IDsOK s [uID] [] [] [] ∧ pass s uID = p"

(* list posts from other apis: *)
definition listOuterPosts :: "state ⇒ userID ⇒ password ⇒ (apiID × postID) list"
where
"listOuterPosts s uID p ≡
  [(saID, pID).
    saID ← serverApiIDs s,
    pID ← outerPostIDs s saID,
    outerVis s saID pID = PublicV ∨ (saID, outerOwner s saID pID) ∈∈ recvOuterFriendIDs s uID
  ]"

definition e_listOuterPosts :: "state ⇒ userID ⇒ password ⇒ bool"
where
"e_listOuterPosts s uID p ≡ IDsOK s [uID] [] [] [] ∧ pass s uID = p"

(* List all the api clients who have already received this post: *)
definition listClientsPost :: "state ⇒ userID ⇒ password ⇒ postID ⇒ (apiID × bool) list"
where
"listClientsPost s uID p pID ≡ sharedWith s pID"

(* Only the admin can see these: *)
definition e_listClientsPost :: "state ⇒ userID ⇒ password ⇒ postID ⇒ bool"
where
"e_listClientsPost s uID p pID ≡
 IDsOK s [uID] [pID] [] [] ∧ pass s uID = p ∧ uID = admin s"


(* list the pending Reqs from the current API to other APIs for them to become servers:  *)
definition listPendingSApiReqs :: "state ⇒ userID ⇒ password ⇒ apiID list"
where
"listPendingSApiReqs s uID p ≡ pendingSApiReqs s"

definition e_listPendingSApiReqs :: "state ⇒ userID ⇒ password ⇒ bool"
where
"e_listPendingSApiReqs s uID p ≡
 IDsOK s [uID] [] [] [] ∧ pass s uID = p ∧ uID = admin s"

(* list the IDs of the server apis: *)
definition listServerAPIs :: "state ⇒ userID ⇒ password ⇒ apiID list"
where
"listServerAPIs s uID p ≡ serverApiIDs s"

definition e_listServerAPIs :: "state ⇒ userID ⇒ password ⇒ bool"
where
"e_listServerAPIs s uID p ≡
 IDsOK s [uID] [] [] [] ∧ pass s uID = p ∧ uID = admin s"


(* list the pending Reqs from APIs that want to become clients of the current API:  *)
definition listPendingCApiReqs :: "state ⇒ userID ⇒ password ⇒ apiID list"
where
"listPendingCApiReqs s uID p ≡ pendingCApiReqs s"

definition e_listPendingCApiReqs :: "state ⇒ userID ⇒ password ⇒ bool"
where
"e_listPendingCApiReqs s uID p ≡
 IDsOK s [uID] [] [] [] ∧ pass s uID = p ∧ uID = admin s"

(* list the IDs of the client apis: *)
definition listClientAPIs :: "state ⇒ userID ⇒ password ⇒ apiID list"
where
"listClientAPIs s uID p ≡ clientApiIDs s"

definition e_listClientAPIs :: "state ⇒ userID ⇒ password ⇒ bool"
where
"e_listClientAPIs s uID p ≡
 IDsOK s [uID] [] [] [] ∧ pass s uID = p ∧ uID = admin s"


subsubsection ‹Actions of communication with other APIs›

(* Note: Some of the communication actions are special in the following sense:
The initiator (the api's admin or, in the case of create outer friend, an arbitrary user, uID)
is different from the observer (another api, aID).  *)

(* The next 4 actions implement the protocol of connecting a server and a client:
-- It starts with the synchronized sendServerReq (with potential client as sender) and
  receiveClientReq (with potential server as receiver)
-- It finishes with the synchronized connectClient (with potential server as sender) and
 connectServer (with potential client as receiver)
 *)


(* Send request to potential server.
 sendServerReq s uID p aID reqInfo does the following: User uID (the admin)
send request to api aID wishing to subscribe to this server;
 In the implementation, the request info along with the URL of the current api (i.e., this api's ID)
 will be sent to the given api aID. *)
definition sendServerReq :: "state ⇒ userID ⇒ password ⇒ apiID ⇒ requestInfo ⇒ (apiID × requestInfo) × state"
where
"sendServerReq s uID p aID reqInfo ≡
 ((aID,reqInfo),
  s ⦇pendingSApiReqs := pendingSApiReqs s @ [aID],
     sApiReq := (sApiReq s) (aID := reqInfo)⦈)"

definition e_sendServerReq :: "state ⇒ userID ⇒ password ⇒ apiID ⇒ requestInfo ⇒ bool"
where
"e_sendServerReq s uID p aID reqInfo ≡
 IDsOK s [uID] [] [] [] ∧ pass s uID = p ∧
 uID = admin s ∧ ¬ aID ∈∈ pendingSApiReqs s"

(* Receive request from potential client.
receiveClientReq s aID reqInfo does the following: receives registration request from
potential client api aID (which is a URL) with request info reqInfo. This action is
not trigered from any user of the current API -- it is an even coming from outside.
*)

definition receiveClientReq :: "state ⇒ apiID ⇒ requestInfo ⇒ state"
where
"receiveClientReq s aID reqInfo ≡
 s ⦇pendingCApiReqs := pendingCApiReqs s @ [aID],
    cApiReq := (cApiReq s) (aID := reqInfo)⦈"

definition e_receiveClientReq :: "state ⇒ apiID ⇒ requestInfo ⇒ bool"
where
"e_receiveClientReq s aID reqInfo ≡
 ¬ aID ∈∈ pendingCApiReqs s ∧ admin s ∈∈ userIDs s"

(* Connect a client that had made a registration request.
connectClient s uID p aID cp does the following: The user uID (the admin)
picks up an api id aID from the list of pending requests and registers it as a client.
At the same time, it issues a password cp for the client, stores it and sends it to aID.
*)

definition connectClient :: "state ⇒ userID ⇒ password ⇒ apiID ⇒ password ⇒ (apiID × password) × state"
where
"connectClient s uID p aID cp ≡
 ((aID, cp),
  s ⦇clientApiIDs := (aID # clientApiIDs s),
     clientPass := (clientPass s) (aID := cp),
     pendingCApiReqs := remove1 aID (pendingCApiReqs s),
     cApiReq := (cApiReq s)(aID := emptyRequestInfo)⦈
 )"

definition e_connectClient :: "state ⇒ userID ⇒ password ⇒ apiID ⇒ password ⇒ bool"
where
"e_connectClient s uID p aID cp ≡
 IDsOK s [uID] [] [] [] ∧ pass s uID = p ∧
 uID = admin s ∧
 aID ∈∈ pendingCApiReqs s ∧ ¬ aID ∈∈ clientApiIDs s"

(* Connect server api
connectServer s aID sp does the following: receives the password sp issued
by the potential server aID and stores it. It will be used for communicating with that server.
Of course, this action only succeeds if a request to aID had really been posted (which was
recorded in pendingSApiReqs).
*)
definition connectServer :: "state ⇒ apiID ⇒ password ⇒ state"
where
"connectServer s aID sp ≡
 s ⦇serverApiIDs := (aID # serverApiIDs s),
    serverPass := (serverPass s) (aID := sp),
    pendingSApiReqs := remove1 aID (pendingSApiReqs s),
    sApiReq := (sApiReq s)(aID := emptyRequestInfo)⦈"

definition e_connectServer :: "state ⇒ apiID ⇒ password ⇒ bool"
where
"e_connectServer s aID sp ≡
 aID ∈∈ pendingSApiReqs s ∧ ¬ aID ∈∈ serverApiIDs s"

(* The next 2 actions represent server-client communication (always from server to client):
-- The server sends a post via sendPost
-- The client receives it via receivePost
Note that, since only the server sends messages to the client, it is the server who authenticates itself.
 *)

(* Send a post and its owner's ID (as well as the server credentials for communicating with that
client) to a client api. Also, recall that the post has now been shared with that client.  *)
definition sendPost ::
"state ⇒ userID ⇒ password ⇒ apiID ⇒ postID ⇒ (apiID × password × postID × post × userID × vis) × state"
where
"sendPost s uID p aID pID ≡
 ((aID, clientPass s aID, pID, post s pID, owner s pID, vis s pID),
  s⦇sharedWith := (sharedWith s) (pID := insert2 aID True (sharedWith s pID))⦈)"

definition e_sendPost :: "state ⇒ userID ⇒ password ⇒ apiID ⇒ postID ⇒ bool"
where
"e_sendPost s uID p aID pID ≡
 IDsOK s [uID] [pID] [] [aID] ∧ pass s uID = p ∧
 uID = admin s ∧ aID ∈∈ clientApiIDs s"

(* Receive a post and its owner's ID (as well as the server credentials) from a server api. *)
definition receivePost :: "state ⇒ apiID ⇒ password ⇒ postID ⇒ post ⇒ userID ⇒ vis ⇒ state"
where
"receivePost s aID sp pID pst uID vs ≡
 let opIDs = outerPostIDs s in
 s ⦇outerPostIDs := opIDs (aID :=  List.insert pID (opIDs aID)),
    outerPost := fun_upd2 (outerPost s) aID pID pst,
    outerOwner := fun_upd2 (outerOwner s) aID pID uID,
    outerVis := fun_upd2 (outerVis s) aID pID vs⦈"

definition e_receivePost :: "state ⇒ apiID ⇒ password ⇒ postID ⇒ post ⇒ userID ⇒ vis ⇒ bool"
where
"e_receivePost s aID sp pID nt uID vs ≡
 IDsOK s [] [] [(aID,[])] [] ∧ serverPass s aID = sp"


(* Create outer friend; unlike inner friendship, outer friendship is not necessarily symmetric.
It is always established from a user of a server to a user of a client, the former giving
unilateral access to the latter at his friend-only posts. These unilateral friendship permissions
are stored on the client.*)

(* sendCreateOFriend s uID p aID uID' means: User uID (of current api), with password p,
  sends an I-set-you-as-my-friend note to the presumptive user uID' on client api aID.
  The request uses the server credentials for the given client, as customary. *)
definition sendCreateOFriend ::
  "state ⇒ userID ⇒ password ⇒ apiID ⇒ userID ⇒ (apiID × password × userID × userID) × state"
where
"sendCreateOFriend s uID p aID uID' ≡
 let ofr = sentOuterFriendIDs s in
 ((aID, clientPass s aID, uID, uID'),
  s ⦇sentOuterFriendIDs := ofr (uID := ofr uID @ [(aID,uID')])⦈)"

(* Note that the server (who issues the note) cannot check if uID' is a valid user on the client.
This will be checked on the client api only.*)
definition e_sendCreateOFriend :: "state ⇒ userID ⇒ password ⇒ apiID ⇒ userID ⇒ bool"
where
"e_sendCreateOFriend s uID p caID uID' ≡
 IDsOK s [uID] [] [] [caID] ∧ pass s uID = p ∧
 ¬ (caID,uID') ∈∈ sentOuterFriendIDs s uID"

(* receiveCreateOFriend s sp saID uID uID' means: The current api receives, from
 one of its registered server apis aAID with password sp, an I-set-you-as-my-friend
 note from aAID's presumptive user uID to the current api's user uID'. The effect
 is that the current api will mark (saID,uID) in the list of outer friends of uID'
 (hence will allow uID' access to friend-only outer posts from uID). *)

definition receiveCreateOFriend :: "state ⇒ apiID ⇒ password ⇒ userID ⇒ userID ⇒ state"
where
"receiveCreateOFriend s saID sp uID uID' ≡
 let ofr = recvOuterFriendIDs s in
 s ⦇recvOuterFriendIDs := ofr (uID' := ofr uID' @ [(saID,uID)])⦈"

definition e_receiveCreateOFriend :: "state ⇒ apiID ⇒ password ⇒ userID ⇒ userID ⇒ bool"
where
"e_receiveCreateOFriend s saID sp uID uID' ≡
 IDsOK s [] [] [(saID,[])] [] ∧ serverPass s saID = sp ∧
 ¬ (saID,uID) ∈∈ recvOuterFriendIDs s uID'"


(* Deletion of outer friends *)

definition sendDeleteOFriend ::
  "state ⇒ userID ⇒ password ⇒ apiID ⇒ userID ⇒ (apiID × password × userID × userID) × state"
where
"sendDeleteOFriend s uID p aID uID' ≡
 let ofr = sentOuterFriendIDs s in
 ((aID, clientPass s aID, uID, uID'),
  s ⦇sentOuterFriendIDs := ofr (uID := remove1 (aID,uID') (ofr uID))⦈)"

definition e_sendDeleteOFriend :: "state ⇒ userID ⇒ password ⇒ apiID ⇒ userID ⇒ bool"
where
"e_sendDeleteOFriend s uID p caID uID' ≡
 IDsOK s [uID] [] [] [caID] ∧ pass s uID = p ∧
 (caID,uID') ∈∈ sentOuterFriendIDs s uID"

definition receiveDeleteOFriend :: "state ⇒ apiID ⇒ password ⇒ userID ⇒ userID ⇒ state"
where
"receiveDeleteOFriend s saID sp uID uID' ≡
 let ofr = recvOuterFriendIDs s in
 s ⦇recvOuterFriendIDs := ofr (uID' := remove1 (saID,uID) (ofr uID'))⦈"

definition e_receiveDeleteOFriend :: "state ⇒ apiID ⇒ password ⇒ userID ⇒ userID ⇒ bool"
where
"e_receiveDeleteOFriend s saID sp uID uID' ≡
 IDsOK s [] [] [(saID,[])] [] ∧ serverPass s saID = sp ∧
 (saID,uID) ∈∈ recvOuterFriendIDs s uID'"




subsection ‹The step function›

datatype out =
  (* Outputs for creation and update actions, as well as for other actions with errors: *)
  outOK | outErr |
  (* Outputs for reading actions: *)
  outBool bool| outName name |
  outPost post | outVis vis |
  outReq requestInfo |
  (* Outputs for listing actions: *)
  outUID "userID" | outUIDL "userID list" |
  outAIDL "apiID list"  |  outAIDBL "(apiID × bool) list"  |
  outUIDPIDL "(userID × postID)list" | outAIDPIDL "(apiID × postID)list" |
  outAIDUIDL "(apiID × userID) list" |
  (* Outputs specific to communication actions: *)
  O_sendServerReq "apiID × requestInfo" | O_connectClient "apiID × password" |
  O_sendPost "apiID × password × postID × post × userID × vis" |
  O_sendCreateOFriend "apiID × password × userID × userID" |
  O_sendDeleteOFriend "apiID × password × userID × userID"


(* The content from outAIDPIDTT outputs: *)
fun from_O_sendPost where
 "from_O_sendPost (O_sendPost antt) = antt"
|"from_O_sendPost _ = undefined"


(* Start actions (only one, but wrapped for uniformity): *)
datatype sActt =
  sSys userID password

lemmas s_defs =
e_startSys_def startSys_def

fun sStep :: "state ⇒ sActt ⇒ out * state" where
"sStep s (sSys uID p) =
 (if e_startSys s uID p
    then (outOK, startSys s uID p)
    else (outErr, s))"

fun sUserOfA :: "sActt ⇒ userID" where
 "sUserOfA (sSys uID p) = uID"

(* Creation actions: *)
datatype cActt =
  cNUReq userID requestInfo
 |cUser userID password userID password
 |cPost userID password postID
 |cFriendReq userID password userID requestInfo
 |cFriend userID password userID

lemmas c_defs =
e_createNUReq_def createNUReq_def
e_createUser_def createUser_def
e_createPost_def createPost_def
e_createFriendReq_def createFriendReq_def
e_createFriend_def createFriend_def