***(

 Formal Specification of the Group Diffie-Hellman Protocol (GDH.2) 
 as Part of the Cliques Toolkit (Version 1.0)

 Author: Mark-Oliver Stehr

 High-level remarks:
 - the cliques toolkit implements join, merge, leave, and refresh protocols (but not the
   initial key distribution, because groups begin their life as singletons)
 - although the cliques toolkit implements further protocols, we currently focus on GDH.2
 - the abstract specification has been obtained by reverse engineering from the C source
 - the spec genuinely models the cliques API, which is uniform for all cliques protocols and 
   makes the toolkit independent of the underlying communication system
 - current specification does not model authentication via digital signatures
   (this could be done in a separate layer or inside the cliques spec)
 - also timestamps and epochs (to prevent replay attacks) are currently not modelled
 - we currently abstract from low-level details such as Diffie-Hellmann parameters

 Remarks on Specification:
 - The document "the design of a group agreement API" alone was not sufficient to figure out the details
   (it seems to be incomplete, possibly out of date, and contains some errors).
 - I don't fully understand how the implementation of the join protocol works. To get it working the current 
   specification deviates from the implementation in one point (see rule for clq-proc-join).
 - The implementation uses explicit authentification using digital signatures rather then implicit authentication 
   as the paper "the design of a group agreement API" seems to suggest (see Kij). Even the comments in the source 
   code refer to these Kij (very confusing), but the actual code does not use them. 
 - Some sanity checks performed in the implementation are omitted, but could be easily added.

)

mod CLIQUES is

protecting NAT .
protecting STRING .

var i : Nat .

--- groups

sort Group .

op group : String -> Group .

var group group' : Group .

--- agents

sort Agent .

op  agent : String -> Agent .

var agent agent' : Agent .
var joiningagent leavingagent : Agent .
var controller newcontroller : Agent .
var member member' : Agent .
var newmember : Agent .

--- list of agents

sort AgentList .
op sAgentList : Agent -> AgentList .
op eAgentList : -> AgentList .
op __ : AgentList AgentList -> AgentList [assoc id: eAgentList] .

var agentlist agentlist' : AgentList .
var memberlist memberlist' : AgentList .
var joiningagents leavingagents mergingagents : AgentList .
var received received' : AgentSet .

op  contains : AgentList Agent -> Bool .
eq  contains(eAgentList, agent') = false .
eq  contains((sAgentList(agent) agentlist), agent') = 
      (agent' == agent) or contains(agentlist, agent') .

op  contains : AgentList AgentList -> Bool .
eq  contains(agentlist, eAgentList) = false .
eq  contains(agentlist, (sAgentList(agent') agentlist')) = 
      contains(agentlist, agent') or contains(agentlist, agentlist') .

op  add : AgentList Agent -> AgentList .
eq  add(agentlist,agent) = (agentlist sAgentList(agent)) .

op  add : AgentList AgentList -> AgentList .
eq  add(agentlist,agentlist') = (agentlist agentlist') .

op  add' : AgentList Agent -> AgentList .
ceq add'(agentlist,agent) = agentlist 
    if contains(agentlist, agent) .
ceq add'(agentlist,agent) = (agentlist sAgentList(agent)) 
    if not(contains(agentlist, agent)) .

op  remove : AgentList Agent -> AgentList .
eq  remove(eAgentList,agent) = eAgentList .
ceq remove((sAgentList(agent) agentlist),agent') = remove(agentlist,agent')
    if (agent' == agent) .
ceq remove((sAgentList(agent) agentlist),agent') = (sAgentList(agent) remove(agentlist,agent'))
    if (agent' =/= agent) .

op  remove : AgentList AgentList -> AgentList .
eq  remove(agentlist, eAgentList) = agentlist .
eq  remove(agentlist, (sAgentList(agent') agentlist')) = 
    remove(remove(agentlist, agent'), agentlist') .

op  subset : AgentList AgentList -> Bool .
eq  subset(eAgentList,agentlist') = true .
eq  subset((sAgentList(agent) agentlist), agentlist') = 
     contains(agentlist',agent) and subset(agentlist,agentlist') .

op  len : AgentList -> Nat .
eq  len(eAgentList) = 0 .
eq  len(sAgentList(agent) agentlist) = 1 + len(agentlist) .

op  ith : AgentList Nat ~> Agent .
eq  ith((sAgentList(agent) agentlist), 1) = agent .
eq  ith((sAgentList(agent) agentlist), (s i)) = ith(agentlist,i) .

op  index : AgentList Agent ~> Nat .
ceq index((sAgentList(agent) agentlist), agent') = 1 
    if agent == agent' .
ceq index((sAgentList(agent) agentlist), agent') = 1 + index(agentlist,agent') 
    if agent =/= agent' .

op  last : AgentList ~> Agent .
eq  last(agentlist sAgentList(agent)) = agent .

op  last : AgentList Nat ~> Agent .
eq  last(agentlist sAgentList(agent), 1) = agent .
eq  last(agentlist sAgentList(agent), (s i)) = last(agentlist, i) .

op  first : AgentList ~> Agent .
eq  first(sAgentList(agent) agentlist) = agent .

op  next : AgentList Agent ~> Agent .
ceq next(sAgentList(agent) agentlist, agent') = first(agentlist)
    if agent == agent' .
ceq next(sAgentList(agent) agentlist, agent') = next(agentlist, agent')
    if agent =/= agent' .

--- set of agents

sort AgentSet .
op  sAgentSet : Agent -> AgentSet .
op  eAgentSet : -> AgentSet .
op  __ : AgentSet AgentSet -> AgentSet [assoc comm id: eAgentSet] .

var agentset agentset' : AgentSet .
var memberset memberset' : AgentSet .
var members members' : AgentSet .

op  contains : AgentSet Agent -> Bool .
eq  contains(eAgentSet, agent') = false .
eq  contains((sAgentSet(agent) agentset), agent') = 
     (agent' == agent) or contains(agentset, agent') .

op  add : AgentSet Agent -> AgentSet .
eq  add(agentset,agent) = (agentset sAgentSet(agent)) .

op  add : AgentSet AgentSet -> AgentSet .
eq  add(agentset,agentset') = (agentset agentset') .

op  add' : AgentSet Agent -> AgentSet .
ceq add'(agentset,agent) = agentset 
    if contains(agentset, agent) .
ceq add'(agentset,agent) = (agentset sAgentSet(agent)) 
    if not(contains(agentset, agent)) .

op  remove : AgentSet Agent -> AgentSet .
eq  remove(eAgentSet,agent) = eAgentSet .
ceq remove((sAgentSet(agent) agentset),agent') = remove(agentset,agent')
    if (agent' == agent) .
ceq remove((sAgentSet(agent) agentset),agent') = (sAgentSet(agent) remove(agentset,agent'))
    if (agent' =/= agent) .

op  remove : AgentSet AgentSet -> AgentSet .
eq  remove(agentset, eAgentSet) = agentset .
eq  remove(agentset, (sAgentSet(agent') agentset')) = 
    remove(remove(agentset, agent'), agentset') .

op  subset : AgentSet AgentSet -> Bool .
eq  subset(eAgentSet,agentset') = true .
eq  subset((sAgentSet(agent) agentset), agentset') = 
    contains(agentset',agent) and subset(agentset,agentset') .

op  set : AgentList -> AgentSet .
eq  set(eAgentList) = eAgentSet .
eq  set(sAgentList(agent)) = sAgentSet(agent) .
ceq set(agentlist agentlist') = set(agentlist) set(agentlist')
    if agentlist =/= eAgentList and agentlist' =/= eAgentList .

--- cyclic groups for public key cryptography
--- the specification is kept abstract, 
--- i.e. we do not confine ourselves to any concrete groups

sort PartialKey . --- group of partial keys and full keys (group secrets)

--- Assume p = k * q + 1 for some small k, and large primes p,q
--- PartialKey should be the unique subgroup of Z_p (i.e. compute modulo p) of prime order q

op idPartialKey : -> PartialKey .
op _*_ : PartialKey PartialKey -> PartialKey [assoc comm id: idPartialKey] .
op inv : PartialKey -> PartialKey .
eq inv(x:PartialKey) * x:PartialKey = idPartialKey .

var partialkey partialkey' : PartialKey .

sort KeyShare . --- group of key contributions

--- x == y iff alpha ^ x == alpha ^ y defines an equivalence 
--- and we have x = y mod q => x == y (because alpha ^ q = id)

--- Hence KeyShare should be the group Z_q (i.e. modulo q) of exponents

var keyshare keyshare' : KeyShare .
var newkeyshare : KeyShare .

op idKeyShare : -> KeyShare .
op _*_ : KeyShare KeyShare -> KeyShare [assoc comm id: idKeyShare] .
op inv : KeyShare -> KeyShare .
eq inv(x:KeyShare) * x:KeyShare = idKeyShare .

op random : Nat -> KeyShare . --- constructor for meta-variables

---

op alpha : -> PartialKey . --- generator of PartialKey group

op _^_ : PartialKey KeyShare -> PartialKey .
eq  x:PartialKey ^ idKeyShare = x:PartialKey .
eq (x:PartialKey ^ y:KeyShare) ^ z:KeyShare = x:PartialKey ^ (y:KeyShare * z:KeyShare) .

--- cliques API data types

sort Params .
op params Nat Nat Nat : -> Params . --- Diffie-Hellman parameters

sort PrivPubKey .
op key : Nat Nat -> PrivPubKey . --- pivate/public key pair

--- group members

sort GroupMember .

op groupmember : 
     Agent --- member name
     PartialKey --- last partial key for this member
  -> GroupMember .

op member : GroupMember -> Agent .
eq member(groupmember(member,partialkey)) = member .

op partialkey : GroupMember -> PartialKey .
eq partialkey(groupmember(member,partialkey)) = partialkey .

var groupmember groupmember' : GroupMember .

--- list of group member

sort GroupMemberList .
op sGroupMemberList : GroupMember -> GroupMemberList .
op eGroupMemberList : -> GroupMemberList .
op __ : GroupMemberList GroupMemberList -> GroupMemberList [assoc id: eGroupMemberList] .

var groupmemberlist groupmemberlist' groupmemberlist'' : GroupMemberList .

op contains : GroupMemberList GroupMember -> Bool .
eq contains(eGroupMemberList, groupmember') = false .
eq contains((sGroupMemberList(groupmember) groupmemberlist), groupmember') = 
     (groupmember' == groupmember) or contains(groupmemberlist, groupmember') .

op add : GroupMemberList GroupMember -> GroupMemberList .
eq add(groupmemberlist,groupmember) = (groupmemberlist sGroupMemberList(groupmember)) .

op  add' : GroupMemberList GroupMember -> GroupMemberList .
ceq add'(groupmemberlist,groupmember) = groupmemberlist 
    if contains(groupmemberlist, groupmember) .
ceq add'(groupmemberlist,groupmember) = (groupmemberlist sGroupMemberList(groupmember)) 
    if not(contains(groupmemberlist, groupmember)) .

op  remove : GroupMemberList GroupMember -> GroupMemberList .
eq  remove(eGroupMemberList,groupmember) = eGroupMemberList .
ceq remove((sGroupMemberList(groupmember) groupmemberlist),groupmember') = remove(groupmemberlist,groupmember')
    if (groupmember' == groupmember) .
ceq remove((sGroupMemberList(groupmember) groupmemberlist),groupmember') = (sGroupMemberList(groupmember) remove(groupmemberlist,groupmember'))
    if (groupmember' =/= groupmember) .

op subset : GroupMemberList GroupMemberList -> Bool .
eq subset(eGroupMemberList,groupmemberlist') = true .
eq subset((sGroupMemberList(groupmember) groupmemberlist), groupmemberlist') = 
    contains(groupmemberlist',groupmember) and subset(groupmemberlist,groupmemberlist') .

op ith : GroupMemberList Nat -> GroupMember .
eq ith(sGroupMemberList(groupmember) groupmemberlist, 0) = groupmember .
eq ith(sGroupMemberList(groupmember) groupmemberlist, (s i)) = ith(groupmemberlist,i) .

op  lookup : GroupMemberList Agent ~> PartialKey .
ceq lookup(sGroupMemberList(groupmember) groupmemberlist, member) = 
    partialkey(groupmember)
    if member(groupmember) == member .
ceq lookup(sGroupMemberList(groupmember) groupmemberlist, member) = 
    lookup(groupmemberlist,member)
    if member(groupmember) =/= member .

op  members : GroupMemberList -> AgentList .
eq  members(eGroupMemberList) = eAgentList .
eq  members(sGroupMemberList(groupmember) groupmemberlist) = 
    sAgentList(member(groupmember)) members(groupmemberlist) .
 
--- specific ops

op is-controller : GroupMemberList Agent -> Bool .
eq is-controller(eGroupMemberList, member) = false .
eq is-controller(groupmemberlist sGroupMemberList(groupmember), member) = 
   member(groupmember) == member . 

op contains : GroupMemberList Agent -> Bool .
eq contains(eGroupMemberList, agent) = false .
eq contains((sGroupMemberList(groupmember) groupmemberlist), agent) = 
     member(groupmember) == agent or contains(groupmemberlist, agent) .

op remove : GroupMemberList Agent -> GroupMemberList .
eq remove(eGroupMemberList, member') = eGroupMemberList .
ceq remove((sGroupMemberList(groupmember(member,partialkey)) groupmemberlist), member') =
    remove(groupmemberlist, member')
    if member == member' .
ceq remove((sGroupMemberList(groupmember(member,partialkey)) groupmemberlist), member') =
    (sGroupMemberList(groupmember(member, partialkey)) remove(groupmemberlist, member'))
    if member =/= member' .

op remove : GroupMemberList AgentList -> GroupMemberList .
eq remove(groupmemberlist, eAgentList) = groupmemberlist .
eq remove(groupmemberlist, (sAgentList(agent') agentlist')) = 
   remove(remove(groupmemberlist, agent'), agentlist') .

op extend : GroupMemberList Agent -> GroupMemberList .
eq extend(groupmemberlist, member) =
    (groupmemberlist sGroupMemberList(groupmember(member,idPartialKey))) .

op extend : GroupMemberList AgentList -> GroupMemberList .
eq extend(groupmemberlist, eAgentList) = groupmemberlist .
eq extend(groupmemberlist, (sAgentList(agent') agentlist')) = 
   extend(extend(groupmemberlist, agent'), agentlist') .

--- updating partial keys

op add-keyshare : GroupMemberList KeyShare -> GroupMemberList .
eq add-keyshare(eGroupMemberList, keyshare) = 
   eGroupMemberList .
eq add-keyshare((sGroupMemberList(groupmember(member,partialkey)) groupmemberlist), keyshare) =
   (sGroupMemberList(groupmember(member, partialkey ^ keyshare)) add-keyshare(groupmemberlist, keyshare)) .

op add-keyshare-except : GroupMemberList Agent KeyShare -> GroupMemberList .
eq  add-keyshare-except(eGroupMemberList, member', keyshare) = 
    eGroupMemberList .
ceq add-keyshare-except((sGroupMemberList(groupmember(member,partialkey)) groupmemberlist), member', keyshare) =
    (sGroupMemberList(groupmember(member, partialkey)) add-keyshare-except(groupmemberlist, member', keyshare)) 
    if member == member' .
ceq add-keyshare-except((sGroupMemberList(groupmember(member,partialkey)) groupmemberlist), member', keyshare) =
    (sGroupMemberList(groupmember(member, partialkey ^ keyshare)) add-keyshare-except(groupmemberlist, member', keyshare)) 
    if member =/= member' .

op overwrite-partialkey : GroupMemberList Agent PartialKey -> GroupMemberList .
eq  overwrite-partialkey(eGroupMemberList, member', partialkey') = 
    eGroupMemberList .
ceq overwrite-partialkey((sGroupMemberList(groupmember(member,partialkey)) groupmemberlist), member', partialkey') =
    (sGroupMemberList(groupmember(member, partialkey')) overwrite-partialkey(groupmemberlist, member', partialkey')) 
    if member == member' .
ceq overwrite-partialkey((sGroupMemberList(groupmember(member,partialkey)) groupmemberlist), member', partialkey') =
    (sGroupMemberList(groupmember(member, partialkey)) overwrite-partialkey(groupmemberlist, member', partialkey'))
    if member =/= member' .

--- tokens, i.e. messages exchanged by the GDH protocol

sort MessageType .

op new-member-message : -> MessageType .
op key-update-message : -> MessageType .
op merge-key-update-message : -> MessageType .
op merge-broadcast-message : -> MessageType .
op merge-factor-out-message : -> MessageType .
op mass-join-message : -> MessageType .

sort Token .

op token : 
   Agent --- sender name
   Group --- group name
   MessageType --- message type
---   Timestamp --- message time stamp
---   Epoch --- message sequence number
   GroupMemberList --- group member list
  -> Token .

var token token' : Token .

var messagetype : MessageType .
var sender : Agent .

op group : Token -> Group .
eq group(token(sender,group,messagetype,groupmemberlist)) = group .

op messagetype : Token -> MessageType .
eq messagetype(token(sender,group,messagetype,groupmemberlist)) = messagetype .

op sender : Token -> Agent .
eq sender(token(sender,group,messagetype,groupmemberlist)) = sender .

op groupmemberlist : Token -> GroupMemberList .
eq groupmemberlist(token(sender,group,messagetype,groupmemberlist)) = groupmemberlist .

sort Epoch .
op epoch : Nat -> Epoch . --- message sequence number

sort Timestamp .
op timestamp : Nat -> Timestamp . --- message time stamp

sort PartialKeyHash .
op dummy-groupsecrethash : -> PartialKeyHash .

--- context associated with each member in each group

sort Context .

op context : 
     KeyShare --- session random number
     PartialKey --- group shared key
---     PartialKeyHash --- hash of group shared key
     GroupMemberList --- list of current group members
---     Params --- Diffie-Hellman parameters
---     PrivPubKey --- private and public key 
---     Epoch --- last message sequence number used
  -> Context .

--- in the cliques API member name and group name are part of the context
--- in the spec we prefer to pull them out and give them explicitly together with the context
--- this seems semantically clearer since the pair (member, group) serves as an identifier

var context context' context'' context''' : Context .

var groupsecret groupsecret' : PartialKey .

op is-controller : Context Agent ~> Bool .
eq is-controller(context, member) = is-controller(groupmemberlist(context), member) .

op members : Context -> AgentList .
eq members(context(keyshare,groupsecret,groupmemberlist)) = members(groupmemberlist) .

op keyshare : Context -> KeyShare .
eq keyshare(context(keyshare,groupsecret,groupmemberlist)) = keyshare .

op groupsecret : Context -> PartialKey .
eq groupsecret(context(keyshare,groupsecret,groupmemberlist)) = groupsecret .

op groupmemberlist : Context -> GroupMemberList .
eq groupmemberlist(context(keyshare,groupsecret,groupmemberlist)) = groupmemberlist .

op update : Context GroupMemberList -> Context .
eq update(context(keyshare,groupsecret,groupmemberlist), groupmemberlist') =
          context(keyshare,groupsecret,groupmemberlist') .

op update : Context KeyShare GroupMemberList -> Context .
eq update(context(keyshare,groupsecret,groupmemberlist), keyshare', groupmemberlist') =
          context(keyshare',groupsecret,groupmemberlist') .

op update : Context PartialKey GroupMemberList -> Context .
eq update(context(keyshare,groupsecret,groupmemberlist), groupsecret', groupmemberlist') =
          context(keyshare,groupsecret',groupmemberlist') .

op update : Context PartialKey -> Context .
eq update(context(keyshare,groupsecret,groupmemberlist), groupsecret') =
          context(keyshare,groupsecret',groupmemberlist) .

op update : Context KeyShare -> Context .
eq update(context(keyshare,groupsecret,groupmemberlist), keyshare') =
          context(keyshare',groupsecret,groupmemberlist) .

op remove : Context Agent -> Context .
eq remove(context(keyshare,groupsecret,groupmemberlist), agent) =
      context(keyshare,groupsecret,remove(groupmemberlist,agent)) .

op remove : Context AgentList -> Context .
eq remove(context(keyshare,groupsecret,groupmemberlist), agentlist) =
      context(keyshare,groupsecret,remove(groupmemberlist,agentlist)) .

op extend : Context AgentList -> Context .
eq extend(context(keyshare,groupsecret,groupmemberlist), agentlist) =
          context(keyshare,groupsecret,extend(groupmemberlist,agentlist)) .

--- cliques API operations

--- join operation

--- perform step 1 of join:
--- clq-proc-join (clq process join) is called by the current
--- controller to hand over group context to a new member (who will
--- become the next controller).  context is modified.

op clq-proc-join-req : --- called by current controller
     Agent   --- context member name
     Group   --- context group name 
     Context --- context of user
     Agent   --- member name
  -> State .

op clq-proc-join-ack : 
     Agent   --- context member name
     Group   --- context group name 
     Context --- updated context
     Token   --- output token 
  -> State .

--- perfom step 2 of join:
--- clq-join is called by a new group member who has received a
--- new-member-message from the current controller.

op clq-join-req : --- called by new member
     Agent   --- member name
     Group   --- group name 
     Token   --- input token 
  -> State .
      
op clq-join-ack : 
     Agent   --- context member name
     Group   --- context group name 
     Context --- created context for new user
     Token   --- output token 
  -> State .

--- perform last step of join:
--- clq-update-ctx is called by a member upon reception of a
--- key-update-message (or merge-key-update-message) from the current
--- group controller

op clq-update-ctx-req : --- called by every group member
     Agent   --- context member name
     Group   --- context group name 
     Context --- current context of member
     Token   --- input token
  -> State .

op clq-update-ctx-ack : 
     Agent   --- context member name
     Group   --- context group name 
     Context --- updated context of member
  -> State .

--- clq-first-user: Called by the first user in the group only.
--- Everybody else has to call clq-join.

op clq-first-user-req : --- called by first member of a group
     Agent   --- first member name
     Group   --- group name
  -> State .

op clq-first-user-ack : 
     Agent   --- context member name
     Group   --- context group name 
     Context --- created context
  -> State .

--- clq-new-user: Called by new users in a merge operation.

op clq-new-user-req : 
     Agent   --- member name
     Group   --- group name
  -> State .

op clq-new-user-ack : 
     Agent   --- context member name
     Group   --- context group name 
     Context --- created context
  -> State .

--- leave operation

--- perform step 1 of leave:
--- clq-leave is called by every group member right after a member
--- leaves the group or a partition occurs (i.e. several members
--- left). This function will remove all the valid members in
--- member list from the group member list. It does NOT depend on the
--- type of the user.  Once all the deletion has been achieved, then
--- if the user is the controller then an output token will be
--- generated.  Only the members that are found in the
--- group_members_list will be deleted. Any invalid member in
--- member list will be ignored.

op clq-leave-req : --- called by every group member
     Agent     --- context member name
     Group     --- context group name 
     Context   --- current group context
     AgentList --- list of members leaving
  -> State .

op clq-leave-ack-controller : 
     Agent     --- context member name
     Group     --- context group name 
     Context   --- updated group context
     Token     --- output token
  -> State .

op clq-leave-ack-not-controller : 
     Agent     --- context member name
     Group     --- context group name 
     Context   --- updated group context
  -> State .

op clq-leave-ack-not-member : 
     Agent     --- context member name
     Group     --- context group name 
  -> State .

--- key refresh operation

--- perform step 1 of key refresh:
--- clq-refresh-key is called by the controller only, when
--- group secret needs to be updated.

op clq-refresh-key-req :  --- called by controller
     Agent   --- context member name
     Group   --- context group name 
     Context --- current group context
     Token   --- output token
  -> State .

op clq-refresh-key-ack : 
     Agent   --- context member name
     Group   --- context group name 
     Context --- modified group context
  -> State .

--- merge operation

--- perform steps 1 and 2 of merge:
--- clq-update-key is called by every new user (who are part of the
--- merge operation) and the group controller. If the group controller
--- is the one calling this function then member list will be
--- passed. Otherwise, for every other user an input token will be
--- passed.  The last new member calling this function will not add
--- his/her keyshare.  Last partial keys of old members in the group
--- remain in the context of the current controller, but they will not
--- be encoded in the token.

op clq-update-key-first-req : 
     Agent     --- context member name
     Group     --- context group name 
     Context   --- current group context
     AgentList --- list of new member names
  -> State .

op clq-update-key-first-ack : 
     Agent   --- context member name
     Group   --- context group name 
     Context --- updated context
     Token   --- output token
  -> State .

op clq-update-key-intermediate-req : 
     Agent   --- context member name
     Group   --- context group name 
     Context --- current group context (empty group memberlist)
     Token   --- input token
  -> State .

op clq-update-key-intermediate-ack : 
     Agent   --- context member name
     Group   --- context group name 
     Context --- updated context
     Token   --- output token
  -> State .

op clq-update-key-last-req : 
     Agent   --- context member name
     Group   --- context group name 
     Context --- current group context (empty group memberlist)
     Token   --- input token
  -> State .

op clq-update-key-last-ack : 
     Agent   --- context member name
     Group   --- context group name 
     Context --- updated context
     Token   --- output token
  -> State .

--- perfrom step 4 of merge:
--- clq-factor-out is called by every member in the group except by
--- the last new member upon recepction of a merge-broadcast
--- message. Although the last new member doesn't have to call this
--- function because he/she is the one that generates that message, if
--- he/she does, then the function will return (no side effects will
--- occur).  During this operation context is not modified (but epoch
--- is).

op clq-factor-out-req : --- called by every group member (except last one)
     Agent   --- context member name
     Group   --- context group name 
     Context --- current member context
     Token   --- input token
  -> State .

op clq-factor-out-ack : 
     Agent   --- context member name
     Group   --- context group name 
     Context --- updated group context
     Token   --- output token
  -> State .

op clq-factor-out-ack : 
     Agent   --- context member name
     Group   --- context group name 
     Context --- updated group context (unchanged)
  -> State .

--- perform step 5 of merge
--- clq-merge: The last step of the merge operation. The controller
--- upon reception of the indiviual factor-out messages should call
--- this function. After he/she receives all the messages, an output
--- token will be generated. This token should be broadcasted to the
--- entire group.

op clq-merge-req : --- called by last new member
     Agent    --- context member name
     Group    --- context group name 
     Context  --- current group context
     Agent    --- name of sender of input token
     Token    --- input token
     AgentSet --- messages have been received from these members
  -> State .

op clq-merge-ack : 
     Agent    --- context member name
     Group    --- context group name 
     Context  --- modified group context
     AgentSet --- messages have been received from these members
  -> State .

op clq-merge-ack : 
     Agent    --- context member name
     Group    --- context group name 
     Context  --- modified group context
     AgentSet --- messages have been received from these members
     Token    --- output token
  -> State .

--- distributed state

sort State .

op eState : -> State .
op __ : State State -> State 
        [assoc comm id: eState format (d ni d)] .

op fresh : Nat -> State . --- generator for fresh indices (used to generate fresh  meta-variables written random(i))

var var : Nat .

--- first user

rl  clq-first-user-req(member,group) =>
    clq-first-user-ack(member,group,context(idKeyShare,idPartialKey,sGroupMemberList(groupmember(member,alpha)))) .

--- new user (created with empty group memberlist)

rl  clq-new-user-req(member,group) =>
    clq-new-user-ack(member,group,context(idKeyShare,idPartialKey,eGroupMemberList)) .

--- join protocol

--- clq-proc-join

--- M_n stores the following list of length n:
---    alpha ^ N_1 * N_2 * ... * N_n-1 * N_n / N_i for i in [1 ... n]

crl fresh(var)
    clq-proc-join-req(controller,group,context,newmember) =>
    fresh(s var)
    clq-proc-join-ack(controller,group,context', token')
    if is-controller(context,controller) /\ 
       newkeyshare := random(var) /\
       groupmemberlist' := add-keyshare-except(groupmemberlist(context), controller, 
         (inv(keyshare(context)) * newkeyshare)) /\
       groupmemberlist'' := add(groupmemberlist', groupmember(newmember, 
         lookup(groupmemberlist(context),controller) ^ newkeyshare)) /\
       context' := update(context, newkeyshare, groupmemberlist'') /\
       token' := token(controller,group,new-member-message,groupmemberlist'') .

--- IMPORTANT DEVIATION FROM IMPLEMENTATION:
--- In the implementation add-keyshare seems to be used instead of add-keyshare-except, but why ? 

--- M_n (current controller) has generated new keyshare N'_n and sent to M_n+1 the following list of length n+1:
---    alpha ^ N_1 * n_2 * ... * N_n-1 * N'_n / N_i for i in [1 ... n], alpha^ N_1 * N_2 * ... * N_n-1 * N'_n

--- clq-join: new member M_n+1 

crl fresh(var)
    clq-join-req(newmember,group,token) =>
    fresh(s var)
    clq-join-ack(newmember,group,context', token')
    if group(token) == group /\ messagetype(token) == new-member-message /\
       groupmemberlist' := add-keyshare-except(groupmemberlist(token), newmember, random(var)) /\
       context' := context(random(var),idPartialKey,groupmemberlist') /\
       token' := token(newmember,group,key-update-message,groupmemberlist') .

--- M_n+1 (new controller) has generated new keyshare N_n+1 and broadcast the following list of length n+1:
---    alpha ^ N_1 * n_2 * ... * N_n-1 * N'_n * N_n+1 / N_i for i in [1 ... n], alpha^ N_1 * N_2 * ... * N_n-1 * N'_n
---  = alpha ^ N_1 * n_2 * ... * N_n-1 * N'_n * N_n+1 / N_i for i in [1 ... n+1]

--- clq-update-ctx

--- M_i (old or new member) receives the following list of length n+1:
---   alpha ^ N_1 * n_2 * ... * N_n-1 * N'_n * N_n+1 / N_i for i in [1 ... n+1]
--- which is of the form where each receiver of the token just needs to factor in its keyshare to obtain the group key

crl clq-update-ctx-req(member,group,context,token) =>
    clq-update-ctx-ack(member,group,context')
    if group(token) == group /\ messagetype(token) == key-update-message /\
       context' := update(context, lookup(groupmemberlist(token),member) ^ keyshare(context), groupmemberlist(token)) .

--- group key is computed by: 
---   alpha ^ N_1 * n_2 * ... * N_n-1 * N'_n * N_n+1 / N_i ^ N_i 
---  = alpha ^ N_1 * n_2 * ... * N_n-1 * N'_n * N_n+1

--- M_i stores the received list of length n+1:
---   alpha ^ N_1 * n_2 * ... * N_n-1 * N'_n * N_n+1 / N_i for i in [1 ... n+1]

--- leave protocol

--- assume M_n+1 ... M_n+k are leaving and M_n becomes new controller

--- M_n stores the following list of length n+k:
---    alpha ^ N_1 * N_2 * ... * N_n-1 * N_n * N_n+1 * ... * N_n+k / N_i for i in [1 ... n+k]

crl fresh(var)
    clq-leave-req(controller, group, context, memberlist) =>
    fresh(s var)
    clq-leave-ack-controller(controller, group, context'', token')
    if context' := remove(context, memberlist) /\
       is-controller(context',controller) /\
       newkeyshare := random(var) /\
       context'' := update(context', newkeyshare) /\
       groupmemberlist' := add-keyshare-except(groupmemberlist(context'), controller, inv(keyshare(context')) * newkeyshare) /\
       token' := token(controller,group,key-update-message,groupmemberlist') .

--- M_n removes leaving members and obtains the following list of length n:
---    alpha ^ N_1 * N_2 * ... * N_n-1 * N_n * N_n+1 * ... * N_n+k / N_i for i in [1 ... n]
---  = alpha ^ N_1 * N_2 * ... * N_n-1 * N_n * N_n+1 * ... * N_n+k / N_i for i in [1 ... n-1], alpha ^ N_1 * N_2 * ... * N_n-1 * N_n+1 * ... * N_n+k 

--- M_n (new controller) has generated new keyshare N'_n and broadcast the following list of length n:
---  = alpha ^ N_1 * N_2 * ... * N_n-1 * N'_n * N_n+1 * ... * N_n+k / N_i for i in [1 ... n-1], alpha ^ N_1 * N_2 * ... * N_n-1 * N_n+1 * ... * N_n+k 
--- which again is of the form where each receiver to the token just needs to factor in its keyshare to obtain the group key
--- note: the use of N and N' is very confusing (think how to formalize this more rigorously)

crl clq-leave-req(member, group, context, memberlist) =>
    clq-leave-ack-not-controller(member, group, context')
    if context' := remove(context, memberlist) /\
       contains(groupmemberlist(context'),member) /\
       not(is-controller(context', member)) .

crl clq-leave-req(member, group, context, memberlist) =>
    clq-leave-ack-not-member(member,group)
    if context' := remove(context, memberlist) /\
       not(contains(groupmemberlist(context'),member)) .

--- merge protocol

crl fresh(var)
    clq-update-key-first-req(controller, group, context, mergingagents) =>
    fresh(s var)
    clq-update-key-first-ack(controller, group, context', token)
    if is-controller(context, controller) /\ not(contains(members(context),mergingagents)) /\
       newkeyshare := random(var) /\
       groupmemberlist' := extend(groupmemberlist(context), mergingagents) /\
       groupmemberlist'' := overwrite-partialkey(groupmemberlist', next(members(groupmemberlist'), controller), 
         lookup(groupmemberlist',controller) ^ newkeyshare) /\
       context' := update(context, newkeyshare, groupmemberlist'') /\
       token := token(controller, group, mass-join-message, groupmemberlist'') .

crl fresh(var)
    clq-update-key-intermediate-req(newmember, group, context, token) =>
    fresh(s var)
    clq-update-key-intermediate-ack(newmember, group, context', token')
    if group(token) == group /\ messagetype(token) == mass-join-message /\  
       groupmemberlist := groupmemberlist(token) /\ not(is-controller(groupmemberlist,newmember)) /\ 
       newkeyshare := random(var) /\
       groupmemberlist' := overwrite-partialkey(groupmemberlist, next(members(groupmemberlist),newmember), 
         lookup(groupmemberlist,newmember) ^ newkeyshare) /\
       context' := update(context, newkeyshare, groupmemberlist') /\
       token' := token(newmember,group,mass-join-message,groupmemberlist') .

crl fresh(var)
    clq-update-key-last-req(newmember, group, context, token) =>
    fresh(s var)
    clq-update-key-last-ack(newmember, group, context', token')
    if group(token) == group /\ messagetype(token) == mass-join-message /\  
       groupmemberlist := groupmemberlist(token) /\ is-controller(groupmemberlist,newmember) /\ 
       context' := update(context, groupmemberlist) /\
       token' := token(newmember,group,merge-broadcast-message,groupmemberlist) .

crl clq-factor-out-req(member, group, context, token) =>
    clq-factor-out-ack(member, group, context', token')
    if group(token) == group /\ messagetype(token) == merge-broadcast-message /\
       groupmemberlist := groupmemberlist(token) /\ not(is-controller(groupmemberlist,member)) /\
       partialkey := lookup(groupmemberlist,last(members(groupmemberlist))) /\
       context' := update(context, overwrite-partialkey(groupmemberlist, member, partialkey ^ inv(keyshare(context)))) /\
       groupmemberlist' := sGroupMemberList(groupmember(member, partialkey ^ inv(keyshare(context)))) /\
       token' := token(member,group,merge-factor-out-message,groupmemberlist') .

crl clq-factor-out-req(member, group, context, token) =>
    clq-factor-out-ack(member, group, context)
       if group(token) == group /\ messagetype(token) == merge-broadcast-message /\
          groupmemberlist := groupmemberlist(token) /\ is-controller(groupmemberlist,member) .

crl fresh(var)
    clq-merge-req(member, group, context, sender, token, received) =>
    fresh(s var)
    clq-merge-ack(member, group, context', add(received,sender))
    if not(contains(received,sender)) /\ add(received,sender) =/= set(remove(members(context),last(members(context)))) /\
       group(token) == group /\ messagetype(token) == merge-factor-out-message /\
       newkeyshare := (if received == eAgentSet then random(var) else keyshare(context) fi) /\ 
       groupmemberlist' := overwrite-partialkey(groupmemberlist(context), sender, lookup(groupmemberlist(token),sender) ^ newkeyshare) /\
       context' := update(context, newkeyshare, groupmemberlist') .

crl fresh(var)
    clq-merge-req(member, group, context, sender, token, received) =>
    fresh(s var)
    clq-merge-ack(member, group, context', add(received,sender), token')
    if not(contains(received,sender)) /\ add(received,sender) == set(remove(members(context),last(members(context)))) /\
       group(token) == group /\ messagetype(token) == merge-factor-out-message /\
       newkeyshare := (if received == eAgentSet then random(var) else keyshare(context) fi) /\ 
       groupmemberlist' := overwrite-partialkey(groupmemberlist(context), sender, lookup(groupmemberlist(token),sender) ^ newkeyshare) /\
       context' := update(context, newkeyshare, groupmemberlist') /\
       token' := token(member,group,merge-key-update-message,groupmemberlist') .

crl clq-update-ctx-req(member, group, context, token) =>
    clq-update-ctx-ack(member, group, context')
    if group(token) == group /\ messagetype(token) == merge-key-update-message /\
       context' := update(context, lookup(groupmemberlist(token),member) ^ keyshare(context), groupmemberlist(token)) .

--- messages

op start : Agent Group -> State .
op start' : Agent Group AgentList -> State .

op join : Agent AgentList Group -> State .
op join : Agent AgentList AgentList Group -> State .

op leave : AgentList AgentList Group -> State .
op leave : AgentList AgentList AgentList Group -> State .

op merge : AgentList AgentList Group -> State .
op merge : AgentList AgentList AgentList Group -> State .

op  message : Agent AgentList Token -> State .

rl  message(agent, eAgentList, token) => eState .

crl message(agent, (agentlist agentlist'), token) =>
    message(agent, agentlist, token)
    message(agent, agentlist', token)
    if agentlist =/= eAgentList /\ agentlist' =/= eAgentList .

--- protocol states

op ready : Agent Group Context AgentList -> State .
op done : Agent Group Context AgentList -> State .
op done' : Agent Group Context AgentList -> State .
op done : Agent Group Context AgentList AgentSet -> State .
op done' : Agent Group Context AgentList AgentSet -> State .
op done'' : Agent Group Context AgentList AgentSet -> State .
op done''' : Agent Group Context AgentList -> State .

op join' : Agent AgentList AgentList Group -> State .
op merge' : AgentList AgentList AgentList Group -> State .

op leaving' : Agent Group Context AgentList AgentList -> State .
op joining' : Agent Group Context Agent AgentList -> State .
op merging' : Agent Group Context AgentList -> State .

op waiting-for-update : Agent Group Context AgentList -> State .
op waiting-for-update' : Agent Group Context AgentList -> State .

op waiting-for-merge-broadcast : Agent Group Context AgentList -> State .
op waiting-for-merge-broadcast' : Agent Group Context AgentList -> State .

op waiting-for-factor-out : Agent Group Context AgentList AgentSet -> State .
op waiting-for-factor-out' : Agent Group Context AgentList AgentSet -> State .

--- startup

rl  start(member,group) =>
    start'(member, group, sAgentList(member))
    clq-first-user-req(member, group) .
    
rl  start'(member, group, memberlist)
    clq-first-user-ack(member, group, context) =>
    ready(member, group, context, memberlist) .

--- join protocol

rl  join(agent, memberlist, group) =>
    join(agent, memberlist, memberlist, group) .

rl  join(agent, eAgentList, memberlist, group) => eState .

crl join(agent, (agentlist agentlist'), memberlist, group) =>
    join(agent, agentlist, memberlist, group)
    join(agent, agentlist', memberlist, group)
    if agentlist =/= eAgentList /\ agentlist' =/= eAgentList .

crl ready(controller, group, context, memberlist)
    join(joiningagent, sAgentList(controller), memberlist', group) =>
    clq-proc-join-req(controller, group, context, joiningagent)
    joining'(controller, group, context, joiningagent, memberlist')
    if is-controller(context, controller) /\
       memberlist' == add(memberlist, joiningagent) .

rl  joining'(controller, group, context, joiningagent, memberlist)
    clq-proc-join-ack(controller, group, context', token') =>
    message(controller, sAgentList(joiningagent), token')
    waiting-for-update(controller, group, context', memberlist) .

crl ready(controller, group, context, memberlist)
    join(joiningagent, sAgentList(controller), memberlist', group) =>
    waiting-for-update(controller, group, context, memberlist')
    if not(is-controller(context, controller)) .

crl join(newcontroller, sAgentList(newcontroller), memberlist, group)
    message(controller, sAgentList(newcontroller), token) =>
    clq-join-req(newcontroller, group, token) 
    join'(newcontroller, sAgentList(newcontroller), memberlist, group) 
    if group(token) == group /\ messagetype(token) == new-member-message .

rl  join'(newcontroller, sAgentList(newcontroller), memberlist, group)
    clq-join-ack(newcontroller, group, context, token) =>
    waiting-for-update(newcontroller, group, context, memberlist)
    message(newcontroller, memberlist, token) .

--- final update phase (used at the end of all protocols)

crl waiting-for-update(member, group, context, memberlist)
    message(agent, sAgentList(member), token) =>
    waiting-for-update'(member, group, context, memberlist)
    clq-update-ctx-req(member, group, context, token) 
    if group(token) == group /\ 
       ((messagetype(token) == key-update-message) or
        (messagetype(token) == merge-key-update-message)) .

rl  waiting-for-update'(member, group, context, memberlist)
    clq-update-ctx-ack(member, group, context') =>
    done(member, group, context', memberlist) .

--- synchronization phase (instance of standard pattern)

op  done-req : Agent Group AgentSet -> State .
op  done-req : Agent Group AgentSet AgentSet -> State .
op  done-rep : AgentSet Group Agent -> State .

rl  done(member, group, context, memberlist) =>
    done'(member, group, context, memberlist, set(memberlist))
    done-req(member, group, set(memberlist), set(memberlist)) .

crl done-req(member, group, (members members'), memberset) =>
    done-req(member, group, members, memberset)
    done-req(member, group, members', memberset)
    if members =/= eAgentSet and members' =/= eAgentSet .

rl  done'(member, group, context, memberlist, eAgentSet) =>
    eState . 
crl done'(member, group, context, memberlist, (members members')) =>
    done'(member, group, context, memberlist, members)
    done'(member, group, context, memberlist, members')
    if members =/= eAgentSet and members' =/= eAgentSet .

crl done'(member, group, context, memberlist, sAgentSet(member'))
    done-req(member', group, sAgentSet(member), memberset) =>
    done''(member, group, context, memberlist, sAgentSet(member'))
    done-rep(sAgentSet(member), group, member')
    if memberset == set(memberlist) .

rl  done-rep(members, group, member)
    done-rep(members', group, member) =>
    done-rep(members members', group, member) .

rl  done''(member, group, context, memberlist, members)
    done''(member, group, context, memberlist, members') =>
    done''(member, group, context, memberlist, (members members')) .

crl done''(member, group, context, memberlist, memberset)
    done-rep(memberset, group, member) =>
    done'''(member, group, context, memberlist) 
    if memberset == set(memberlist) .

rl  done'''(member, group, context, memberlist) =>
    ready(member, group, context, memberlist) .
 

--- leave protocol

rl  leave(leavingagents, memberlist, group) =>
    leave(leavingagents, memberlist, memberlist, group) . 

rl  leave(leavingagents, eAgentList, memberlist, group) => eState .

crl leave(leavingagents, (agentlist agentlist'), memberlist, group) =>
    leave(leavingagents, agentlist, memberlist, group)
    leave(leavingagents, agentlist', memberlist, group)
    if agentlist =/= eAgentList /\ agentlist' =/= eAgentList .

rl  ready(member, group, context, memberlist)
    leave(leavingagents, sAgentList(member), memberlist, group) =>
    leaving'(member, group, context, leavingagents, remove(memberlist,leavingagents))
    clq-leave-req(member, group, context, leavingagents) .

rl  leaving'(controller, group, context, leavingagents, memberlist) 
    clq-leave-ack-controller(controller, group, context', token) =>
    waiting-for-update(controller, group, context', memberlist) 
    message(controller, memberlist, token) .

rl  leaving'(member, group, context, leavingagents, memberlist) 
    clq-leave-ack-not-controller(member, group, context') =>
    waiting-for-update(member, group, context', memberlist) .

rl  leaving'(member, group, context, leavingagents, memberlist)
    clq-leave-ack-not-member(agent, group) =>
    eState .

--- merge protocol

rl  merge(mergingagents, memberlist, group) =>
    merge(mergingagents, memberlist, memberlist, group) . 

rl  merge(mergingagents, eAgentList, memberlist, group) => eState .

crl merge(mergingagents, (agentlist agentlist'), memberlist, group) =>
    merge(mergingagents, agentlist, memberlist, group)
    merge(mergingagents, agentlist', memberlist, group)
    if agentlist =/= eAgentList /\ agentlist' =/= eAgentList .

crl ready(member, group, context, memberlist)
    merge(mergingagents, sAgentList(member), memberlist', group) =>
    waiting-for-merge-broadcast(member, group, context, memberlist')
    if not(is-controller(context, member)) /\ not(contains(mergingagents,member)) /\
       memberlist' == add(memberlist, mergingagents) .

crl ready(controller, group, context, memberlist)
    merge(mergingagents, sAgentList(controller), memberlist', group) =>
    merging'(controller, group, context, memberlist')
    clq-update-key-first-req(controller, group, context, mergingagents)
    if is-controller(context, controller) /\
       memberlist' == add(memberlist, mergingagents) .

rl  merging'(controller, group, context, memberlist)
    clq-update-key-first-ack(controller, group, context', token') =>
    waiting-for-merge-broadcast(controller, group, context', memberlist)
    message(controller, sAgentList(next(memberlist,controller)), token') .

crl merge(mergingagents, sAgentList(newmember), memberlist, group) =>
    clq-new-user-req(newmember, group)
    merge'(mergingagents, sAgentList(newmember), memberlist, group)
    if contains(mergingagents, newmember) .

rl  merge'(mergingagents, sAgentList(newmember), memberlist, group) 
    clq-new-user-ack(newmember, group, context) =>
    ready(newmember, group, context, memberlist) .

crl ready(newmember, group, context, memberlist) 
    message(agent, sAgentList(newmember), token) =>
    clq-update-key-intermediate-req(newmember, group, context, token) 
    merging'(newmember, group, context, memberlist) 
    if group(token) == group /\ messagetype(token) == mass-join-message /\ 
       newmember =/= last(memberlist) .

rl  merging'(member, group, context, memberlist)
    clq-update-key-intermediate-ack(member, group, context', token') =>
    waiting-for-merge-broadcast(member, group, context', memberlist)
    message(member, sAgentList(next(memberlist,member)), token') .

crl ready(newmember, group, context, memberlist) 
    message(agent, sAgentList(newmember), token) =>
    clq-update-key-last-req(newmember, group, context, token) 
    merging'(newmember, group, context, memberlist) 
    if group(token) == group /\ messagetype(token) == mass-join-message /\ 
       newmember == last(memberlist) .

rl  merging'(controller, group, context, memberlist)
    clq-update-key-last-ack(controller, group, context', token') =>
    waiting-for-merge-broadcast(controller, group, context', memberlist)
    message(controller, memberlist, token') .

crl waiting-for-merge-broadcast(member, group, context, memberlist) 
    message(agent, sAgentList(member), token) =>
    clq-factor-out-req(member, group, context, token)
    waiting-for-merge-broadcast'(member, group, context, memberlist) 
    if group(token) == group /\ messagetype(token) == merge-broadcast-message .

rl  waiting-for-merge-broadcast'(member, group, context, memberlist)
    clq-factor-out-ack(member, group, context',token) =>
    waiting-for-update(member, group, context', memberlist) 
    message(member, sAgentList(last(memberlist)), token) .

rl  waiting-for-merge-broadcast'(member, group, context, memberlist)
    clq-factor-out-ack(member, group, context') =>
    waiting-for-factor-out(member, group, context', memberlist, eAgentSet) .

crl waiting-for-factor-out(member, group, context, memberlist, received) 
    message(agent, sAgentList(member), token) =>
    waiting-for-factor-out'(member, group, context, memberlist,received) 
    clq-merge-req(member, group, context, sender(token), token, received)
    if group(token) == group /\ messagetype(token) == merge-factor-out-message .

rl  waiting-for-factor-out'(member, group, context, memberlist,received) 
    clq-merge-ack(member, group, context', received') =>
    waiting-for-factor-out(member, group, context', memberlist, received') .    

rl  waiting-for-factor-out'(member, group, context, memberlist,received) 
    clq-merge-ack(member, group, context', received', token) =>
    waiting-for-update(member, group, context', memberlist)
    message(member, memberlist, token) .

endm