--- Formal Specification of the Group Diffie-Hellman Protocol (GDH.2) 
---  as Part of the Cliques Toolkit (Version 1.0)
---
--- Authors: Mark-Oliver Stehr, Sebastian Gutierrez-Nolasco (UCI)
--- Date: July, 2004
---
--- High-level Notes:
--- - 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
---
--- Further Notes:
--- - 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 can work. 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 .
protecting AGENT .
protecting GROUP .
including STATE .

var i : Nat .
var group : Group .
var agent agent' : Agent .
var joiningagent : Agent .
var controller newcontroller : Agent .
var member member' : Agent .
var newmember : Agent .
var agentlist agentlist' : AgentList .
var memberlist memberlist' : AgentList .
var leavingagents mergingagents : AgentList .
var received received' : AgentSet .
var memberset : AgentSet .
var members members' : AgentSet .


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

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


--- 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 .


--- group of key contributions
sort KeyShare .	

--- 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 .


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


--- generator of PartialKey group
op alpha : -> PartialKey . 
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
--- Diffie-Hellman parameters
sort Params .
op params Nat Nat Nat : -> Params . 


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


--- 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  rm : GroupMemberList GroupMember -> GroupMemberList .
eq  rm(eGroupMemberList,groupmember) = eGroupMemberList .
ceq rm((sGroupMemberList(groupmember) groupmemberlist),groupmember') = rm(groupmemberlist,groupmember')
    if (groupmember' == groupmember) .
ceq rm((sGroupMemberList(groupmember) groupmemberlist),groupmember') = (sGroupMemberList(groupmember) rm(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 controller : GroupMemberList ~> Agent .
eq controller(groupmemberlist) = last(members(groupmemberlist)) .

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

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

op rm : GroupMemberList AgentList -> GroupMemberList .
eq rm(groupmemberlist, eAgentList) = groupmemberlist .
eq rm(groupmemberlist, (sAgentList(agent') agentlist')) = 
   rm(rm(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
---   KeyId		--- Agreed (unique) KeyId
---   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 .


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


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

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 controller : Context ~> Agent .
eq controller(context) = controller(groupmemberlist(context)) .

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 rm : Context Agent -> Context .
eq rm(context(keyshare,groupsecret,groupmemberlist), agent) =
      context(keyshare,groupsecret,rm(groupmemberlist,agent)) .

op rm : Context AgentList -> Context .
eq rm(context(keyshare,groupsecret,groupmemberlist), agentlist) =
      context(keyshare,groupsecret,rm(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.
---
--- called by current controller
op clq-proc-join-req 
    : 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.
---
--- called by new member
op clq-join-req 
    : 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
---
--- called by every group member
op clq-update-ctx-req  
    : 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.
---
--- called by first member of a group
op clq-first-user-req 
    : 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 rm 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.
---
--- called by every group member
op clq-leave-req 
    : 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.
---
--- called by controller
op clq-refresh-key-req  
    : 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).

--- called by every group member (except last one)
op clq-factor-out-req 
    : 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.
---
--- called by last new member
op clq-merge-req 
    : 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 .

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

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' := rm(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 rms 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' := rm(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' := rm(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 clq-update-key-last-req(newmember, group, context, token)  
    =>
    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) =/= agentset(rm(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) == agentset(rm(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)) .

endm