--- Formal Specification of 
--- the Secure Spread Basic Robust Key Agreement Algorithm on top of 
--- the Spread Group Communication System (using Flush Spread) and
--- the Cliques Toolkit
---
--- Authors: Grit Denker, (SRI), Mark-Oliver Stehr (UIUC), Carolyn Talcott (SRI)
--- Date: March 26, 2004
---
--- References: 
---
---   Secure Group Communication Using Robust Contributory Key Agreement.
---      Y. Amir, Y. Kim, C. Nita-Rotaru, J. Schultz, J. Stanton, G. Tsudik
---      IEEE Transactions on Parallel and Distributed Systems archive, 
---      pp. 468 - 480, 15(5), IEEE Press, 2004.
---
---   Secure Spread Souce Code. Version 2.1.0. Available at www.spread.org.
---
--- Notes:
---
--- Our formalization deviates from the paper in a few points:
--- - In contrast to the paper we handle events in no state
---   (diagram/decription in the paper not clear about join)
--- - Use of last in PT state for ctx did not make sense
---   because the context doesnt contain the new members yet.
--- - KL state needs to store which factor out tokens 
---   have been received so far (in order to use the cliqes API).
--- - We ignore our own merge broadcast (we dont need to update our own info).
--- - Some assignments (e.g. in case 2 of PT state) are really 
---   cliques procedure calls (according to cliques API).
--- - Encryption/decryption is made explicit.

--- The actual implementation also provides signed multicast and
--- and getkey function, which we omitted in the current spec.

mod SECURESPREAD is

protecting BOOL .
protecting NAT .
protecting STRING .
protecting FLUSHSPREAD .
protecting CLIQUES .
protecting SMESSAGE .
protecting SAPI .
protecting GROUPVAR .

------------------------

var client agent : Agent .
var group group' : Group .
var agentset agentset' : AgentSet .
var context context' : Context .
var token : Token .
var viewset viewset' : ViewSet .
var view : View .
var fmessage : FMessage .
var fmessagelist : FMessageList .
var transset transset' : AgentSet .
var fdata : FData .
var error : Error .
var smessage smessage' : SMessage .
var sdata : SData .
var smessagelist smessagelist' : SMessageList .
var groupcontextset groupcontextset' : GroupContextSet .

-----------------------

var key : PartialKey .
 
op enc : PartialKey SData ~> FData .
eq enc(key,sdata) = sdatamsg(key,sdata) .

op dec : PartialKey FData ~> SData .
eq dec(key,sdatamsg(key,sdata)) = sdata .

-------------------------
---- there are two kinds of internal messages (encapsulated as flush level data)

op isidata : FMessage -> Bool .
eq isidata(fmessage) = isfdata(fmessage) and isidata(data(fmessage)) .

op isitoken : FMessage -> Bool .
eq isitoken(fmessage) = isfdata(fmessage) and isitoken(data(fmessage)) .

-------------------------
--- translation between flush layer messages and secure layer messages

op conv : FMessage ~> SMessage .
eq conv(freqmsg(agent,group)) = sfreqmsg(agent,group) .
eq conv(ftransmsg(group)) = stransmsg(group) .
eq conv(fjoinmsg(agent,group,view)) = sjoinmsg(agent,group,view) .
eq conv(fleavemsg(agent,group,view)) = sleavemsg(agent,group,view) .
eq conv(fdisconnectmsg(agent,group,view)) = sdisconnectmsg(agent,group,view) .
eq conv(fconfmsg(group,view,transset)) = sconfmsg(group,view,transset) .
eq conv(fselfleavemsg(agent,group)) = sselfleavemsg(agent,group) .

op conv : PartialKey FMessage ~> SMessage .
eq conv(key,fdatamsg(client,group,fdata,view)) = sdatamsg(client,group,dec(key,fdata),view) .

-----------------------
--- internal data structures

op siview : Agent ViewSet -> State . 
   --- the views the agent has installed
   
op sstate : Agent GroupSet GroupSet GroupSet GroupSet GroupSet GroupSet -> State . 
   --- client's state for all groups
   --- S, CM, PT, FT, FO, KL

var secure secure' cm cm' pt pt' ft ft' fo fo' kl kl' : GroupSet .
   
--- global variables (values for each group)

op snotfirsttrans : Agent GroupSet -> State .
op svstrans : Agent GroupSet -> State .
op snotfirstcm : Agent GroupSet -> State .
op swaitforsfok : Agent GroupSet  -> State .
op sklgotfreq : Agent GroupSet -> State .
op svsset : Agent GroupAgentSetSet -> State .
op scontext : Agent GroupContextSet -> State .
op snewmembmsg : Agent GroupSMessageSet -> State .
op snewcontroller : Agent GroupSet -> State .
op sforeceived : Agent GroupAgentSetSet -> State .

var waitforsfok waitforsfok' : GroupSet .
var klgotfreq klgotfreq' : GroupSet .
var notfirsttrans notfirsttrans' : GroupSet .
var vstrans vstrans' : GroupSet .
var notfirstcm notfirstcm' : GroupSet .
var vsset vsset' : GroupAgentSetSet .
var foreceived foreceived' : GroupAgentSetSet .
var newmembmsgset  newmembmsgset' : GroupSMessageSet .
var newcontroller newcontroller' : GroupSet .

--- messages to be delivered to application

op sbuffer : Agent SMessageList -> State . 

-----------------------
--- ssp-connect
-----------------------

op ssp-connect-req' : Agent -> State .

rl  ssp-connect-req(client) =>
    ssp-connect-req'(client)
    f-connect-req(client) .

rl  ssp-connect-req'(client)
    f-connect-ack(client) =>
    siview(client,eViewSet)
    sstate(client,eGroupSet,eGroupSet,eGroupSet,eGroupSet,eGroupSet,eGroupSet)
    swaitforsfok(client,eGroupSet)
    sklgotfreq(client,eGroupSet)
    snotfirsttrans(client,eGroupSet)
    svstrans(client,eGroupSet)
    snotfirstcm(client,eGroupSet)
    svsset(client,eGroupAgentSetSet)
    snewcontroller(client,eGroupSet)
    scontext(client,eGroupContextSet)
    snewmembmsg(client,eGroupSMessageSet)
    sforeceived(client,eGroupAgentSetSet)
    sbuffer(client,eSMessageList)
    ssp-connect-ack(client) .

rl  ssp-connect-req'(client)
    f-connect-err(client,error) =>
    ssp-connect-err(client,error) .

-----------------------
--- sp-disconnect
-----------------------

op ssp-disconnect-req' : Agent -> State .

rl  ssp-disconnect-req(client) =>
    ssp-disconnect-req'(client)
    f-disconnect-req(client) .

rl  ssp-disconnect-req'(client)
    siview(client,viewset)
    sstate(client,secure,cm,pt,ft,fo,kl)
    swaitforsfok(client,waitforsfok)
    sklgotfreq(client,klgotfreq)
    snotfirsttrans(client,notfirsttrans)
    svstrans(client,vstrans)
    snotfirstcm(client,notfirstcm)
    svsset(client,vsset)
    snewcontroller(client,newcontroller)
    scontext(client,groupcontextset)
    snewmembmsg(client,newmembmsgset)
    sforeceived(client,foreceived)
    sbuffer(client,smessagelist)
    f-disconnect-ack(client) =>
    ssp-disconnect-ack(client) .

rl  ssp-disconnect-req'(client)
    f-disconnect-err(client,error) =>
    ssp-disconnect-err(client,error) .

-----------------------
--- ssp-join
-----------------------

op ssp-join-req' : Agent Group -> State .

rl  ssp-join-req(client,group) =>
    ssp-join-req'(client,group)
    f-join-req(client,group) .
    
rl  ssp-join-req'(client,group)
    f-join-ack(client) =>
    ssp-join-ack(client) .

rl  ssp-join-req'(client,group)
    f-join-err(client,error) =>
    ssp-join-err(client,error) .

-----------------------
--- ssp-leave
-----------------------

op ssp-leave-req' : Agent Group -> State .

rl  ssp-leave-req(client,group) =>
    ssp-leave-req'(client,group)
    f-leave-req(client,group) .

rl  ssp-leave-req'(client,group)
    f-leave-ack(client) =>
    ssp-leave-ack(client) .

rl  ssp-leave-req'(client,group)
    f-leave-err(client,error) =>
    ssp-leave-err(client,error) .

    --- ??? see ssp code
    --- if err= connection_closed or illegal session, code calls
    --- ssp-disconnect-req(client)
    --- instead of ssp-leave-err(...)
    --- MOS: dont understand this comment
 
-----------------------
--- ssp-multicast
-----------------------

var mode : Mode .

op ssp-multicast-req' : Agent Mode Group SData -> State .

--- if client is in secure state, then user msg is broadcast

crl sstate(client,secure,cm,pt,ft,fo,kl)
    scontext(client,groupcontextset)    
    ssp-multicast-req(client,mode,group,sdata) =>
    sstate(client,secure,cm,pt,ft,fo,kl)
    scontext(client,groupcontextset)    
    ssp-multicast-req'(client,mode,group,sdata)
    f-multicast-req(client,mode,group,fdata)
    if contains(secure,group) /\ 
       key := groupsecret(get(groupcontextset,group)) /\
       fdata := enc(key,sdata) .

    --- ??? can agent receive user message when in no state for group? 
    --- MOS: shouldn't happen

--- if client is in CM,PT,FT,FO,KL state, then user msg produces error

crl sstate(client,secure,cm,pt,ft,fo,kl)
    ssp-multicast-req(client,mode,group,sdata) =>
    sstate(client,secure,cm,pt,ft,fo,kl)
    ssp-multicast-err(client,IllegalState)
    if contains(cm,group) or contains(pt,group) or 
       contains(ft,group) or contains(fo,group) or 
       contains(kl,group) .
    
rl  ssp-multicast-req'(client,mode,group,sdata)
    f-multicast-ack(client) =>
    ssp-multicast-ack(client) .

rl  ssp-multicast-req'(client,mode,group,sdata)
    f-multicast-err(client,error) =>
    ssp-multicast-err(client,error) .

-----------------------
--- ssp-receive
-----------------------

op ssp-receive-req' : Agent -> State .

--- if there is anything to deliver, do it right away

rl  ssp-receive-req(client) 
    sbuffer(client, sSMessageList(smessage) smessagelist) =>
    sbuffer(client, smessagelist)
    ssp-receive-ack(client,smessage) .

--- otherwise check if transitions are enabled in state machine 

rl  ssp-receive-req(client) 
    sbuffer(client, eSMessageList) =>
    ssp-receive-req'(client)
    sbuffer(client, eSMessageList)
    f-receive-req(client) .

rl ssp-receive-req'(client)
   f-receive-err(client,error) =>
   ssp-receive-err(client,error) .
    
-------------------------------------------------------------------  
--- 
--- NO STATE BEHAVIOR 
---
-------------------------------------------------------------------           
--- NO STATE - receive secure_flush_ok from app -> see ssp-flushok-req
 
--- NO STATE - receive freq msg
--- if client is in no state for the group mentioned in freq msg
--- deliver freq msgs to app, set waitforsfok flag

crl ssp-receive-req'(client) 
    sstate(client,secure,cm,pt,ft,fo,kl)
    swaitforsfok(client,waitforsfok)
    sbuffer(client,smessagelist)
    f-receive-ack(client,fmessage) =>
    sstate(client,secure,cm,pt,ft,fo,kl)
    swaitforsfok(client,waitforsfok')
    sbuffer(client,smessagelist sSMessageList(conv(fmessage)))
    ssp-receive-req(client) 
    if isfreq(fmessage) /\ group := group(fmessage) /\
       not(contains(cm pt ft fo kl, group)) /\  
       not(contains(waitforsfok,group)) /\
       waitforsfok' := add(waitforsfok, group) .
   
-------------------------------------------------------------------  
--- 
--- SECURE STATE BEHAVIOR 
---
-------------------------------------------------------------------

--- SECURE STATE - receive user msg ->  see ssp-multicast-req
--- SECURE STATE - receive secure flush ok from app -> see ssp-flushok-req
   
--- SECURE STATE - receive fdata msg   
--- if client is in secure or cm state for the group mentioned in fdata msg
--- pass fdata msg in right view to app 
--- in all other states, fdata msg is not possible (due to paper)

crl siview(client,viewset)
    sstate(client,secure,cm,pt,ft,fo,kl)
    scontext(client,groupcontextset)    
    ssp-receive-req'(client)
    sbuffer(client,smessagelist)
    f-receive-ack(client,fmessage) =>
    siview(client,viewset)
    sstate(client,secure,cm,pt,ft,fo,kl)
    scontext(client,groupcontextset)
    sbuffer(client,smessagelist sSMessageList(smessage))
    ssp-receive-req(client)
    if isidata(fmessage) /\ group := group(fmessage) /\
       contains((secure cm),group) /\
       get(viewset,group) == view(fmessage) /\ --- should hold because of sending view delivery
       key := groupsecret(get(groupcontextset,group)) /\
       smessage := conv(key,fmessage) .

    --- ??? what to do with fdata msg in wrong view? can that happen? MOS: shouln't happen
    --- ??? what if agent is not in secure state for group of fdata msg? 
    ---     can that happen? MOS: shouldn't happen
     
--- SECURE STATE - receive freq msg
--- if client is in secure state for the group mentioned in freq msg
--- deliver freq msgs to app, set waitforsfok flag

crl ssp-receive-req'(client) 
    sstate(client,secure,cm,pt,ft,fo,kl)
    swaitforsfok(client,waitforsfok)
    sbuffer(client,smessagelist)
    f-receive-ack(client,fmessage) =>
    sstate(client,secure,cm,pt,ft,fo,kl)
    sbuffer(client,smessagelist sSMessageList(conv(fmessage)))
    swaitforsfok(client,waitforsfok')
    ssp-receive-req(client)
    if isfreq(fmessage) /\  group := group(fmessage) /\
       contains(secure,group) /\
       waitforsfok' := add(waitforsfok,group) .

--- SECURE STATE - ftrans msg   
--- if client is in secure state for the group mentioned in ftrans msg
--- deliver ftrans msgs to app, set flags

crl ssp-receive-req'(client) 
    sstate(client,secure,cm,pt,ft,fo,kl)
    snotfirsttrans(client,notfirsttrans)
    svstrans(client,vstrans)
    sbuffer(client,smessagelist)
    f-receive-ack(client,fmessage) =>
    sstate(client,secure,cm,pt,ft,fo,kl)
    snotfirsttrans(client,notfirsttrans')
    svstrans(client,vstrans')
    sbuffer(client,smessagelist sSMessageList(conv(fmessage)))
    ssp-receive-req(client) 
    if isftrans(fmessage) /\ group := group(fmessage) /\
       contains(secure,group) /\
       vstrans' := add(vstrans,group) /\
       notfirsttrans' := add(notfirsttrans,group) .

--- if client is in SECURE state for the group mentioned in fselfleave msg
--- delete view for affected group, deliver fselfleave msg to app
--- in all other states, fselfleave msg not possible 

crl siview(client,viewset)
    sstate(client,secure,cm,pt,ft,fo,kl)
    ssp-receive-req'(client)
    sbuffer(client,smessagelist)
    f-receive-ack(client,fmessage) =>
    siview(client,viewset')
    sstate(client,secure',cm,pt,ft,fo,kl)
    sbuffer(client,smessagelist sSMessageList(conv(fmessage)))
    ssp-receive-req(client) 
    if isfselfleave(fmessage) /\ group := group(fmessage) /\
       contains(secure,group) /\
       secure' := rm(secure, group) /\
       viewset' := rm(viewset,group) .
                  

-------------------------------------------------------------------  
--- 
--- BEHAVIOR SHARED BETWEEN DIFFERENT STATES
---
------------------------------------------------------------------- 

op ssp-wait-for-flushok : Agent Group -> State .

--- PT,FT,FO - receive freq msg
--- if client is in this state for the group mentioned in freq msg
--- send flushok to flushlayer, change state to cm

crl ssp-receive-req'(client) 
    sstate(client,secure,cm,pt,ft,fo,kl)
    f-receive-ack(client,fmessage) =>
    sstate(client,secure,cm,pt,ft,fo,kl)
    ssp-wait-for-flushok(client, group)
    f-flushok-req(client,group) 
    if isfreq(fmessage) /\ group := group(fmessage) /\
       contains((pt ft fo),group) .  

crl ssp-wait-for-flushok(client,group)
    sstate(client,secure,cm,pt,ft,fo,kl)
    f-flushok-ack(client) =>
    sstate(client,secure,cm',pt',ft',fo,kl)
    ssp-receive-req(client)
    if pt' := rm(pt,group) /\
       ft' := rm(ft,group) /\
       fo' := rm(fo,group) /\
       cm' := add(cm,group) .  

--- PT,FT,FO,CM,KL - receive trans message

crl ssp-receive-req'(client) 
    sstate(client,secure,cm,pt,ft,fo,kl)
    snotfirsttrans(client, notfirsttrans)
    svstrans(client, vstrans)
    f-receive-ack(client,fmessage) =>
    sstate(client,secure,cm,pt,ft,fo,kl)
    snotfirsttrans(client, notfirsttrans)
    svstrans(client, vstrans')
    ssp-receive-req(client)
    if isftrans(fmessage) /\ group := group(fmessage) /\
       contains((pt ft fo cm kl),group) /\
       contains(notfirsttrans, group) /\
       vstrans' := add(vstrans, group) .  

crl ssp-receive-req'(client) 
    sstate(client,secure,cm,pt,ft,fo,kl)
    snotfirsttrans(client, notfirsttrans)
    svstrans(client, vstrans)
    sbuffer(client,smessagelist)
    f-receive-ack(client,fmessage) =>
    sstate(client,secure,cm,pt,ft,fo,kl)
    snotfirsttrans(client, notfirsttrans')
    svstrans(client, vstrans')
    sbuffer(client,smessagelist sSMessageList(conv(fmessage)))
    ssp-receive-req(client)
    if isftrans(fmessage) /\ group := group(fmessage) /\
       contains((pt ft fo cm kl),group) /\
       not(contains(notfirsttrans, group)) /\
       vstrans' := add(vstrans, group) /\
       notfirsttrans' := add(notfirsttrans, group) .  

-------------------------------------------------------------------  
--- 
--- PARTIAL TOKEN STATE BEHAVIOR 
---
------------------------------------------------------------------- 

--- PT intermediate states

op ssp-pt-wait-for-update-key-intermediate : Agent Group -> State .
op ssp-pt-wait-for-update-key-last : Agent Group -> State .
op ssp-pt-wait-for-final-token-multicast : Agent Group -> State .
op ssp-pt-wait-for-partial-token-unicast : Agent Group -> State .

--- PT - receive partial token

--- i am not the new controller

crl ssp-receive-req'(client)
    sstate(client,secure,cm,pt,ft,fo,kl)
    scontext(client,groupcontextset)
    snewcontroller(client,newcontroller)
    f-receive-ack(client,fmessage) =>
    ssp-pt-wait-for-update-key-intermediate(client,group)
    sstate(client,secure,cm,pt,ft,fo,kl)
    scontext(client,groupcontextset)
    snewcontroller(client,newcontroller)
    clq-update-key-intermediate-req(client,group,context,token)
    if isitoken(fmessage) /\ token := token(data(fmessage)) /\ messagetype(token) == mass-join-message /\  
       group := group(token) /\ contains(pt,group) /\
       context := get(groupcontextset, group) /\
       not(contains(newcontroller, group)) .

crl ssp-pt-wait-for-update-key-intermediate(client,group)
    scontext(client,groupcontextset)
    clq-update-key-intermediate-ack(client,group,context,token) =>
    ssp-pt-wait-for-partial-token-unicast(client,group)
    scontext(client,groupcontextset')
    f-multicast-req(client,fifo,privategroup(next(members(groupmemberlist(context)),client)),stokenmsg(token))
    if groupcontextset' := update(groupcontextset, group, context) .

crl ssp-pt-wait-for-partial-token-unicast(client,group)
    sstate(client,secure,cm,pt,ft,fo,kl)
    f-multicast-ack(client) =>
    sstate(client,secure,cm,pt',ft',fo,kl)
    ssp-receive-req(client)
    if pt' := rm(pt,group) /\
       ft' := add(ft,group) .  

--- i am the new controller

crl ssp-receive-req'(client)
    sstate(client,secure,cm,pt,ft,fo,kl)
    scontext(client,groupcontextset)
    snewcontroller(client,newcontroller)
    f-receive-ack(client,fmessage) =>
    ssp-pt-wait-for-update-key-last(client,group)
    sstate(client,secure,cm,pt,ft,fo,kl)
    scontext(client,groupcontextset)
    snewcontroller(client,newcontroller)
    clq-update-key-last-req(client,group,context,token)
    if isitoken(fmessage) /\ token := token(data(fmessage)) /\ messagetype(token) == mass-join-message /\  
       group := group(token) /\ contains(pt,group) /\
       context := get(groupcontextset, group) /\
       contains(newcontroller, group) .

crl ssp-pt-wait-for-update-key-last(client,group)
    scontext(client,groupcontextset)
    clq-update-key-last-ack(client,group,context,token) =>
    ssp-pt-wait-for-final-token-multicast(client,group)
    scontext(client,groupcontextset')
    f-multicast-req(client,fifo,group,stokenmsg(token))
    if groupcontextset' := update(groupcontextset, group, context) .  

crl ssp-pt-wait-for-final-token-multicast(client,group)
    sstate(client,secure,cm,pt,ft,fo,kl)
    f-multicast-ack(client) =>
    sstate(client,secure,cm,pt',ft,fo',kl)
    ssp-receive-req(client)
    if pt' := rm(pt,group) /\
       fo' := add(fo,group) .  

-------------------------------------------------------------------  
--- 
--- FINAL TOKEN STATE BEHAVIOR 
---
------------------------------------------------------------------- 

--- FT intermediate states

op ssp-ft-wait-for-factor-out : Agent Group -> State .
op ssp-ft-wait-for-factor-out-unicast : Agent Group -> State .

--- FT - receive final token

crl ssp-receive-req'(client) 
    sstate(client,secure,cm,pt,ft,fo,kl)
    scontext(client,groupcontextset)
    f-receive-ack(client,fmessage) =>
    ssp-ft-wait-for-factor-out(client,group)
    sstate(client,secure,cm,pt,ft,fo,kl)
    scontext(client,groupcontextset)
    clq-factor-out-req(client,group,context,token)
    if isitoken(fmessage) /\ token := token(data(fmessage)) /\ messagetype(token) == merge-broadcast-message /\
       group := group(token) /\ contains(ft,group) /\
       context := get(groupcontextset, group) . 

crl ssp-ft-wait-for-factor-out(client,group)
    scontext(client,groupcontextset)
    clq-factor-out-ack(client,group,context,token) =>
    ssp-ft-wait-for-factor-out-unicast(client,group)
    scontext(client,groupcontextset)
    f-multicast-req(client,fifo,privategroup(controller(context)),stokenmsg(token))
    if groupcontextset' := update(groupcontextset, group, context) .

crl ssp-ft-wait-for-factor-out-unicast(client,group)
    sstate(client,secure,cm,pt,ft,fo,kl)
    sklgotfreq(client,klgotfreq)
    f-multicast-ack(client) =>
    ssp-receive-req(client)
    sstate(client,secure,cm,pt,ft',fo,kl')
    sklgotfreq(client,klgotfreq')
    if ft' := rm(ft,group) /\
       kl' := add(kl,group) /\
       klgotfreq' := rm(klgotfreq,group) .

-------------------------------------------------------------------  
--- 
--- FACTOR OUT STATE BEHAVIOR 
---
-------------------------------------------------------------------      

--- FO intermediate states

op ssp-fo-wait-for-merge : Agent Group -> State .
op ssp-fo-wait-for-keylist-multicast : Agent Group -> State .

--- FO - receive factor out token

var received : AgentSet .

crl ssp-receive-req'(client) 
    sstate(client,secure,cm,pt,ft,fo,kl)
    scontext(client,groupcontextset)
    sforeceived(client,foreceived)
    f-receive-ack(client,fmessage) =>
    ssp-fo-wait-for-merge(client,group)
    sstate(client,secure,cm,pt,ft,fo,kl)
    scontext(client,groupcontextset)
    sforeceived(client,foreceived)
    clq-merge-req(client,group,context,sender(fmessage),token,received)
    if isitoken(fmessage) /\ token := token(data(fmessage)) /\ messagetype(token) == merge-factor-out-message /\
       group := group(token) /\ contains(fo,group) /\
       context := get(groupcontextset, group) /\
       received := get(foreceived, group) . 

crl ssp-fo-wait-for-merge(client,group)
    scontext(client,groupcontextset)
    sforeceived(client,foreceived)
    clq-merge-ack(client,group,context,received) =>
    scontext(client,groupcontextset')
    sforeceived(client,foreceived')
    ssp-receive-req(client)
    if groupcontextset' := update(groupcontextset, group, context) /\
       foreceived' := update(foreceived, group, received) .

crl ssp-fo-wait-for-merge(client,group)
    scontext(client,groupcontextset)
    sforeceived(client,foreceived)
    clq-merge-ack(client,group,context,received,token) =>
    scontext(client,groupcontextset')
    sforeceived(client,foreceived')
    ssp-fo-wait-for-keylist-multicast(client,group)
    f-multicast-req(client,agreed,group,stokenmsg(token)) 
    if groupcontextset' := update(groupcontextset, group, context) /\
       foreceived' := update(foreceived, group, received) .

crl ssp-fo-wait-for-keylist-multicast(client,group)
    sstate(client,secure,cm,pt,ft,fo,kl)
    sklgotfreq(client,klgotfreq)
    f-multicast-ack(client) =>
    ssp-receive-req(client)
    sstate(client,secure,cm,pt,ft,fo',kl')
    sklgotfreq(client,klgotfreq')
    if fo' := rm(fo,group) /\
       kl' := add(kl,group) /\
       klgotfreq' := rm(klgotfreq,group) .

--- ignore own merge-broadcast-message

crl ssp-receive-req'(client) 
    sstate(client,secure,cm,pt,ft,fo,kl)
    f-receive-ack(client,fmessage) =>
    sstate(client,secure,cm,pt,ft,fo,kl)
    ssp-receive-req(client) 
    if isitoken(fmessage) /\ token := token(data(fmessage)) /\ 
       messagetype(token) == merge-broadcast-message /\ sender(token) == client /\
       group := group(token) /\ contains(fo,group) . 

-------------------------------------------------------------------  
--- 
--- KEY LIST STATE BEHAVIOR 
---
-------------------------------------------------------------------                 

--- KL intermediate states

op ssp-kl-wait-for-flushok : Agent Group -> State .
op ssp-kl-wait-for-update-ctx : Agent Group -> State .
op ssp-kl-check-for-flushok : Agent Group -> State .
op ssp-kl-wait-for-flushok' : Agent Group -> State .

--- KL - receive freq msg
--- if client is in kl state for the group mentioned in freq msg
--- and svtrans is true, then send flushok to flushlayer, change state to cm

crl ssp-receive-req'(client)
    sstate(client,secure,cm,pt,ft,fo,kl)
    svstrans(client,vstrans)
    sklgotfreq(client, klgotfreq)
    f-receive-ack(client,fmessage) =>
    sstate(client,secure,cm,pt,ft,fo,kl)
    svstrans(client,vstrans)
    sklgotfreq(client, klgotfreq')
    ssp-receive-req(client)
    if isfreq(fmessage) /\ group := group(fmessage) /\
       contains(kl,group(fmessage)) /\
       not(contains(vstrans,group)) /\
       klgotfreq' := add(klgotfreq, group).   

crl ssp-receive-req'(client) 
    sstate(client,secure,cm,pt,ft,fo,kl)
    svstrans(client,vstrans)
    f-receive-ack(client,fmessage) =>
    ssp-wait-for-flushok(client,group)
    sstate(client,secure,cm,pt,ft,fo,kl)
    svstrans(client,vstrans)
    f-flushok-req(client,group) 
    if isfreq(fmessage) /\ group := group(fmessage) /\
       contains(kl,group(fmessage)) /\
       contains(vstrans,group) .   

crl ssp-wait-for-flushok(client,group)
    sstate(client,secure,cm,pt,ft,fo,kl)
    f-flushok-ack(client) =>
    sstate(client,secure,cm',pt,ft,fo,kl')
    ssp-receive-req(client)
    if kl' := rm(pt,group) /\
       cm' := add(cm,group) .   
               
--- KL - receive freq msg
--- if client is in kl state for the group mentioned in freq msg
--- but svtrans is not true, then only set sklgotfreq to true 

crl ssp-receive-req'(client) 
    sstate(client,secure,cm,pt,ft,fo,kl)
    svstrans(client,vstrans)
    sklgotfreq(client,klgotfreq)
    f-receive-ack(client,fmessage) =>
    sstate(client,secure,cm,pt,ft,fo,kl)
    svstrans(client,vstrans)
    sklgotfreq(client,klgotfreq')
    if isfreq(fmessage) /\ group := group(fmessage) /\
       contains(kl,group) /\
       not(contains(vstrans,group)) /\
       klgotfreq' := add(klgotfreq,group) .  

--- KL - receive key list

crl ssp-receive-req'(client) 
    sstate(client,secure,cm,pt,ft,fo,kl)
    svstrans(client,vstrans)
    f-receive-ack(client,fmessage) =>
    sstate(client,secure,cm,pt,ft,fo,kl)
    svstrans(client,vstrans)
    ssp-receive-req(client)
    if isitoken(fmessage) /\ token := token(data(fmessage)) /\ messagetype(token) == merge-key-update-message /\
       group := group(token) /\ contains(kl,group) /\ contains(vstrans,group) . 

crl ssp-receive-req'(client) 
    sstate(client,secure,cm,pt,ft,fo,kl)
    svstrans(client,vstrans)
    scontext(client,groupcontextset)
    f-receive-ack(client,fmessage) =>
    ssp-kl-wait-for-update-ctx(client,group)
    sstate(client,secure,cm,pt,ft,fo,kl)
    svstrans(client,vstrans)
    scontext(client,groupcontextset)
    clq-update-ctx-req(client,group,context,token)
    if isitoken(fmessage) /\ token := token(data(fmessage)) /\ messagetype(token) == merge-key-update-message /\
       group := group(token) /\ contains(kl,group) /\ not(contains(vstrans,group)) /\
       context := get(groupcontextset, group) . 

crl ssp-kl-wait-for-update-ctx(client,group)
    sstate(client,secure,cm,pt,ft,fo,kl)
    svsset(client,vsset)
    snotfirsttrans(client,notfirsttrans)
    snotfirstcm(client,notfirstcm)
    scontext(client,groupcontextset)
    snewmembmsg(client,newmembmsgset)
    sbuffer(client,smessagelist)
    clq-update-ctx-ack(client,group,context) =>
    sstate(client,secure',cm,pt,ft,fo,kl')
    svsset(client,vsset)
    sbuffer(client,smessagelist sSMessageList(smessage))
    ssp-kl-check-for-flushok(client,group)
    scontext(client,groupcontextset')
    snotfirsttrans(client,notfirsttrans')
    snotfirstcm(client,notfirstcm')
    snewmembmsg(client,newmembmsgset)
    if groupcontextset' := update(groupcontextset, group, context) /\
       notfirsttrans' := rm(notfirsttrans, group) /\
       notfirstcm' := rm(notfirstcm, group) /\
       smessage := update-transset(get(newmembmsgset,group), get(vsset, group)) /\
       kl' := rm(kl,group) /\
       secure' := add(secure,group) .

crl ssp-kl-check-for-flushok(client,group)
    sklgotfreq(client,klgotfreq)
    swaitforsfok(client,waitforsfok)
    sbuffer(client,smessagelist) =>
    sklgotfreq(client,klgotfreq)
    swaitforsfok(client,waitforsfok')
    sbuffer(client,smessagelist sSMessageList(smessage))
    ssp-receive-req(client)
    if contains(klgotfreq, group) /\
       waitforsfok' := add(waitforsfok, group) /\
       smessage := sfreqmsg(client,group) .

crl ssp-kl-check-for-flushok(client,group)
    sklgotfreq(client,klgotfreq) =>
    sklgotfreq(client,klgotfreq)
    ssp-receive-req(client)
    if not(contains(klgotfreq, group)) .

--- KL receive trans message

crl ssp-receive-req'(client) 
    sstate(client,secure,cm,pt,ft,fo,kl)
    snotfirsttrans(client, notfirsttrans)
    svstrans(client, vstrans)
    sklgotfreq(client,klgotfreq) 
    sbuffer(client,smessagelist)
    f-receive-ack(client,fmessage) =>
    sstate(client,secure,cm,pt,ft,fo,kl)
    snotfirsttrans(client, notfirsttrans')
    svstrans(client, vstrans')
    sklgotfreq(client,klgotfreq)
    sbuffer(client,smessagelist sSMessageList(conv(fmessage)))
    ssp-receive-req(client)
    if isftrans(fmessage) /\ group := group(fmessage) /\
       contains(kl,group) /\
       not(contains(notfirsttrans, group)) /\
       not(contains(klgotfreq, group)) /\
       vstrans' := add(vstrans, group) /\
       notfirsttrans' := add(notfirsttrans, group) .  

crl ssp-receive-req'(client) 
    sstate(client,secure,cm,pt,ft,fo,kl)
    snotfirsttrans(client, notfirsttrans)
    svstrans(client, vstrans)
    sklgotfreq(client,klgotfreq) 
    sbuffer(client,smessagelist)
    f-receive-ack(client,fmessage) =>
    sstate(client,secure,cm',pt,ft,fo,kl')
    snotfirsttrans(client, notfirsttrans')
    svstrans(client, vstrans')
    sklgotfreq(client,klgotfreq)
    sbuffer(client,smessagelist sSMessageList(conv(fmessage)))
    ssp-flushok-req(client,group)
    ssp-kl-wait-for-flushok'(client,group)
    if isftrans(fmessage) /\ group := group(fmessage) /\
       contains(kl,group) /\
       not(contains(notfirsttrans, group)) /\
       contains(klgotfreq, group) /\
       vstrans' := add(vstrans, group) /\
       notfirsttrans' := add(notfirsttrans, group) /\
       kl' := rm(kl, group) /\
       cm' := add(cm, group) .  

rl  ssp-kl-wait-for-flushok'(client,group) 
    f-flushok-ack(client) =>
    ssp-receive-req(client) .

-------------------------------------------------------------------  
--- 
--- CASCADING MEMBERSHIP STATE BEHAVIOR 
---
-------------------------------------------------------------------                          

--- CM intermediate states

op ssp-cm-cases : Agent Group FMessage -> State .
op ssp-cm-alone-wait-for-first-user : Agent Group FMessage -> State .
op ssp-cm-not-alone-wait-for-new-user : Agent Group FMessage -> State .
op ssp-cm-not-alone-wait-for-first-user : Agent Group FMessage AgentList -> State .
op ssp-cm-not-alone-wait-for-update-key-first : Agent Group FMessage AgentList -> State .
op ssp-cm-not-alone-wait-for-unicast : Agent Group FMessage AgentList -> State .

--- CM - receive freq msg

--- if client is in CM state for the group mentioned in membership msg
--- DO THE HARD WORK

var leaveset : AgentSet .

crl siview(client,viewset)
    sstate(client,secure,cm,pt,ft,fo,kl)
    snotfirstcm(client,notfirstcm)
    svstrans(client,vstrans)
    svsset(client,vsset)
    snewmembmsg(client,newmembmsgset)
    sforeceived(client,foreceived)
    ssp-receive-req'(client)
    f-receive-ack(client,fmessage) =>
    siview(client,viewset')
    sstate(client,secure,cm,pt,ft,fo,kl)
    snotfirstcm(client,notfirstcm')
    svstrans(client,vstrans')
    svsset(client,vsset')
    snewmembmsg(client,newmembmsgset')
    sforeceived(client,foreceived')
    ssp-cm-cases(client,group,fmessage)
    if isviewmsg(fmessage) /\ group := group(fmessage) /\
       contains(cm, group) /\
       viewset' := (update(viewset,group,view(fmessage))) /\
       notfirstcm' := add(notfirstcm,group) /\
       newmembmsgset' := update(newmembmsgset,group,conv(fmessage)) /\
       leaveset := if(contains(viewset,group)) then
                     rm(agentset(members(view(fmessage))),agentset(members(get(viewset,group))))
                   else eAgentSet fi /\
       vsset' := update(vsset, group, 
                    rm(if contains(notfirstcm,group) then get(vsset,group) 
                       else agentset(members(view(fmessage))) fi, leaveset)) /\ 
       foreceived' := update(foreceived, group, eAgentSet) /\
       vstrans' := rm(vstrans,group) .


--- I am alone

crl ssp-cm-cases(client,group,fmessage) =>
    ssp-cm-alone-wait-for-first-user(client,group,fmessage)
    clq-first-user-req(client,group)
    if agentset(members(view(fmessage))) == sAgentSet(client) . --- I am alone

crl ssp-cm-alone-wait-for-first-user(client,group,fmessage) 
    sstate(client,secure,cm,pt,ft,fo,kl)
    scontext(client,groupcontextset)
    snewcontroller(client,newcontroller)
    snewmembmsg(client,newmembmsgset)
    sbuffer(client,smessagelist)
    clq-first-user-ack(client,group,context) =>
    sstate(client,secure',cm',pt,ft,fo,kl) 
    sbuffer(client,smessagelist sSMessageList(smessage))
    scontext(client,groupcontextset')
    snewcontroller(client,newcontroller')
    snewmembmsg(client,newmembmsgset)
    ssp-receive-req(client)
    if groupcontextset' := update(groupcontextset, group, context) /\
       newcontroller' := add(newcontroller, group) /\
       smessage := update-transset(get(newmembmsgset, group),sAgentSet(client)) /\
       cm' := rm(cm, group) /\ 
       secure' := add(secure, group) .

--- I am not alone and I am not choosen

crl ssp-cm-cases(client,group,fmessage) 
    snewcontroller(client,newcontroller) =>
    ssp-cm-not-alone-wait-for-new-user(client,group,fmessage)
    snewcontroller(client,newcontroller')
    clq-new-user-req(client,group)
    if card(agentset(members(view(fmessage)))) > 1 /\ --- I am not alone
       client =/= first(members(view(fmessage))) /\ --- I am not choosen 
       newcontroller' := if client == last(members(view(fmessage))) 
                         then add(newcontroller, group) else rm(newcontroller, group) fi .

crl ssp-cm-not-alone-wait-for-new-user(client,group,fmessage) 
    sstate(client,secure,cm,pt,ft,fo,kl)
    scontext(client,groupcontextset)
    clq-new-user-ack(client,group,context) =>
    sstate(client,secure,cm',pt',ft,fo,kl) 
    scontext(client,groupcontextset')
    ssp-receive-req(client)
    if groupcontextset' := update(groupcontextset, group, context) /\
       cm' := rm(cm, group) /\ 
       pt' := add(pt, group) . 
       
--- I am not alone and I am choosen

var mergingagents : AgentList .

crl ssp-cm-cases(client,group,fmessage) 
    snewcontroller(client,newcontroller) =>
    ssp-cm-not-alone-wait-for-first-user(client,group,fmessage,mergingagents)
    snewcontroller(client,newcontroller')
    clq-first-user-req(client,group)
    if card(agentset(members(view(fmessage)))) > 1 /\ --- I am not alone
       client == first(members(view(fmessage))) /\ --- I am not choosen 
       mergingagents := rm(members(view(fmessage)),client) /\
       newcontroller' := rm(newcontroller, group) .

crl ssp-cm-not-alone-wait-for-first-user(client,group,fmessage,mergingagents) 
    scontext(client,groupcontextset)
    clq-first-user-ack(client,group,context) =>
    ssp-cm-not-alone-wait-for-update-key-first(client,group,fmessage,mergingagents) 
    scontext(client,groupcontextset')
    clq-update-key-first-req(client,group,context,mergingagents)
    if groupcontextset' := update(groupcontextset, group, context) .

crl ssp-cm-not-alone-wait-for-update-key-first(client,group,fmessage,mergingagents) 
    scontext(client,groupcontextset)
    clq-update-key-first-ack(client,group,context,token) =>
    ssp-cm-not-alone-wait-for-unicast(client,group,fmessage,mergingagents) 
    scontext(client,groupcontextset')
    f-multicast-req(client,fifo,privategroup(next(members(groupmemberlist(context)),client)),stokenmsg(token))
    if groupcontextset' := update(groupcontextset, group, context) .

crl ssp-cm-not-alone-wait-for-unicast(client,group,fmessage,mergingagents) 
    sstate(client,secure,cm,pt,ft,fo,kl)
    f-multicast-ack(client) =>
    sstate(client,secure,cm',pt,ft',fo,kl) 
    ssp-receive-req(client)
    if cm' := rm(cm, group) /\ 
       ft' := add(ft, group) . 

--- ignore partial token, final token, fact out token, and keylist messages

crl ssp-receive-req'(client) 
    sstate(client,secure,cm,pt,ft,fo,kl)
    f-receive-ack(client,fmessage) =>
    sstate(client,secure,cm,pt,ft,fo,kl)
    ssp-receive-req(client) 
    if isitoken(fmessage) /\ token := token(data(fmessage)) /\ 
       group := group(token) /\ contains(cm,group) . 


-----------------------
--- ssp-flushok
-----------------------

op  ssp-flushok-req' : Agent Group -> State .

--- SECURE STATE - receive ssp-flushok-req msg    
--- if client is in secure state for the group mentioned in msg
--- and waifforsflok flag is set
--- then pass msg to app and change to CM state

crl sstate(client,secure,cm,pt,ft,fo,kl)
    swaitforsfok(client,waitforsfok)
    ssp-flushok-req(client,group) =>
    sstate(client,secure',cm',pt,ft,fo,kl)
    swaitforsfok(client,waitforsfok')
    f-flushok-req(client,group)
    ssp-flushok-req'(client,group) 
    if contains(secure,group) /\
       contains(waitforsfok,group) /\
       secure' := rm(secure,group) /\
       cm' := add(cm,group) /\
       waitforsfok' := rm(waitforsfok,group) .
   
--- NO STATE - receive ssp-flushok-req msg      
--- if client is in no state currently for the group mentioned in msg
--- then pass msg for application and change to CM state

crl sstate(client,secure,cm,pt,ft,fo,kl)
    swaitforsfok(client,waitforsfok) 
    ssp-flushok-req(client,group) =>
    sstate(client,secure,cm',pt,ft,fo,kl)
    swaitforsfok(client,waitforsfok') 
    f-flushok-req(client,group)
    ssp-flushok-req'(client,group) 
    if not(contains(secure cm pt ft fo kl,group)) /\
       contains(waitforsfok,group) /\
       cm' := add(cm,group) /\
       waitforsfok' := rm(waitforsfok,group) .

--- ANY STATE - receive ssp-flushok-req msg    
--- if client is in any state for the group mentioned in msg
--- but waitforsfok flag not set 
--- then error     

crl swaitforsfok(client,waitforsfok)
    ssp-flushok-req(client,group) =>
    swaitforsfok(client,waitforsfok)
    ssp-receive-err(client,IllegalState) 
    if not(contains(waitforsfok,group)).

--- if client is in CM,PT,FT,FO,KL state, then flushok produces error

crl sstate(client,secure,cm,pt,ft,fo,kl)
    ssp-flushok-req(client,group) =>
    sstate(client,secure,cm,pt,ft,fo,kl)
    ssp-flushok-err(client,IllegalState)
    if contains(cm,group) or contains(pt,group) or 
       contains(ft,group) or contains(fo,group) or 
       contains(kl,group) .
 
rl  ssp-flushok-req'(client,group) 
    f-flushok-ack(client) => 
    ssp-flushok-ack(client) .

rl  ssp-flushok-req'(client,group)
    f-flushok-err(client,error) => 
    ssp-flushok-err(client,error) . 

endm