--- 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), --- Sebastian Gutierrez-Nolasco (UCI) --- Date: September, 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. --- - We model some errors (connection_closed or illegal session, code calls) --- as ssp-disconnect-req(client) instead of ssp-leave-err(...) --- The actual implementation also provides signed multicast and --- and getkey function, which we omitted in the current spec. --- Modifications (Generalizations to Secure Spread): Seguti --- --- - Every agent keeps a list of keys and associated keyids (assockeylist) --- - Every outgoing message is encrypted and tagged with a unique keyid --- - The most recent keyid is used to get the associated key. --- Thus, messages can be encrypted and sent when rekey is --- in progress (Non-blocking rekey) --- --- - When an agent receives an encrypted message, extract the keyid and --- look for the proper key to decrypt it --- - VS Case --- - current keyid = message keyid --- - EVS Case --- - current keyid >= message keyid --- - Agent can receive a message tagged with an unknown --- keyid (message was sent before agent joined the --- group) -> old message --- - To preserve backward secrecy and EVS semantics at the --- secure layer, old (encrypted) messages are marked --- nondecryptable and delivered to the application --- --- - Message Types --- - non-decryptable --- - Message received but the key associated with the --- message's keyid was not found --- - delayed --- - Message received and decrypted with a vary old key --- - requested-sending-view --- - Message is encrypted using key associated with requested view --- - fresh-secure --- - Message triggers a rekey if current key is not fresh --- --- - Secure Delivery Modes --- - Non-Secure (NS) --- - Clear text data message --- - sndclear flag --- - Secure (S) --- - Encrypted message delivered, but may be nondecryptable --- - Extra Secure (ES) --- - Encrypted message delivered and guaranteed to be decryptable --- * Ultra Secure (US) --- - Encrypted message is delivered only if everybody else --- received and can be decrypted with recent key --- - Forceka flag --- --- - Group Types --- - vs-group --- - VS groups use secure spread with VS semantics (flush) --- - evs-group --- - EVS groups use generalization of secure spread with --- EVS semantics (no flush) --- --- --- --- NOTES: --- - Keyid concept was taken from the following paper: "Scaling Secure --- Communication Systems: Beyond Peer-to-Peer", Y. Amir, C. Nita-Rotaru, --- J. Stanton, G. Tsudik, in Proceedings of DISCEX3 Washington DC, 2003. --- --- - A keyid does not uniquely identify a key. i.e. several keyids --- may reference the same key --- --- mod SECURESPREAD is protecting BOOL . protecting NAT . protecting STRING . protecting FLUSHSPREAD . protecting CLIQUES . protecting SMESSAGE . protecting SAPI . protecting GROUPVAR . protecting ASSOCKEY . protecting ASSOCMEMBSET . 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 rnum : Nat . var keyid keyid' currkeyid currkeyid' : KeyId . var key partialkey partialkey' : PartialKey . var assockey assockey' : AssocKey . var assockeylist assockeylist' : AssocKeyList . var groupassockeylist groupassockeylist' : GroupAssocKeyList . var groupassockeylistset groupassockeylistset' : GroupAssocKeyListSet . var assocmembsetlist assocmembsetlist' : AssocMembSetList . var groupassocmembsetlist groupassocmembsetlist' : GroupAssocMembSetList . var groupassocmembsetlistset groupassocmembsetlistset' : GroupAssocMembSetListSet . var flushtype : FlushType . op enc : KeyId PartialKey SData ~> FData . eq enc(keyid,key,sdata) = sdatamsg(keyid,key,sdata) . op dec : PartialKey FData ~> SData . eq dec(key,sdatamsg(keyid,key,sdata)) = sdata . --- 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(freqmsg(agent,group,flushtype)) = sfreqmsg(agent,group,flushtype) . 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 --- the views the agent has installed op siview : Agent ViewSet -> State . --- client's state for all groups (S, CM, PT, FT, FO, KL) op sstate : Agent GroupSet GroupSet GroupSet GroupSet GroupSet GroupSet -> State . 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 snewmembmsg : Agent GroupSMessageSet -> State . op snewcontroller : Agent GroupSet -> State . op sforeceived : Agent GroupAgentSetSet -> State . op freshkeyid : Nat -> State . op scontext : Agent KeyId GroupContextSet -> State . op sgrptype : Agent GroupSet GroupSet -> State . op slaziness : Agent GroupSet GroupSet GroupSet -> State . op sgroupkeylist : Agent GroupAssocKeyListSet -> State . op sgroupmembsetlist : Agent GroupAssocMembSetListSet -> State . op sfreshness : Agent GroupSet -> State . op sforceka : Agent GroupSet -> State . op skatype : Agent GroupSet GroupSet -> State . op skainprogress : Agent GroupSet -> State . op sshadowmessage : Agent FMessageList -> State . var vsgrp evsgrp : GroupSet . var lazyst lazyct eager : GroupSet . var blocking non-blocking : GroupSet . var freshkey freshkey' : GroupSet . var forceka forceka' : GroupSet . var kainprogress kainprogress' : GroupSet . var shadowmessage : FMessageList . var grouptype : GroupType . var laziness : Laziness . var katype : KAType . 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,keyid(0),eGroupContextSet) snewmembmsg(client,eGroupSMessageSet) sforeceived(client,eGroupAgentSetSet) sbuffer(client,eSMessageList) sgroupkeylist(client,eGroupAssocKeyListSet) sgrptype(client,eGroupSet,eGroupSet) sgroupmembsetlist(client,eGroupAssocMembSetListSet) slaziness(client,eGroupSet,eGroupSet,eGroupSet) sfreshness(client,eGroupSet) sforceka(client,eGroupSet) skainprogress(client,eGroupSet) sshadowmessage(client,eFMessageList) skatype(client,eGroupSet,eGroupSet) 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,currkeyid,groupcontextset) snewmembmsg(client,newmembmsgset) sforeceived(client,foreceived) sbuffer(client,smessagelist) sgroupkeylist(client,groupassockeylistset) sgrptype(client,vsgrp,evsgrp) sgroupmembsetlist(client,groupassocmembsetlistset) slaziness(client,lazyst,lazyct,eager) sfreshness(client,freshkey) sforceka(client,forceka) skainprogress(client,kainprogress) sshadowmessage(client,shadowmessage) skatype(client,blocking,non-blocking) 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 GroupType Laziness KAType -> State . --- lazyct crl ssp-join-req(client,group,grouptype,laziness,katype) sgrptype(client,vsgrp,evsgrp) slaziness(client,lazyst,lazyct,eager) skatype(client,blocking,non-blocking) sforceka(client,forceka) => ssp-join-req'(client,group,grouptype,laziness,katype) sgrptype(client,add'(vsgrp,group),evsgrp) slaziness(client,lazyst,add'(lazyct,group),eager) skatype(client,blocking,add'(non-blocking,group)) sforceka(client,forceka') f-join-req(client,group,grouptype) if isvs(grouptype) /\ islazyct(laziness) /\ forceka' := add(forceka,group) . crl ssp-join-req(client,group,grouptype,laziness,katype) sgrptype(client,vsgrp,evsgrp) slaziness(client,lazyst,lazyct,eager) skatype(client,blocking,non-blocking) sforceka(client,forceka) => ssp-join-req'(client,group,grouptype, laziness,katype) sgrptype(client,vsgrp,add'(evsgrp,group)) slaziness(client,lazyst,add'(lazyct,group),eager) skatype(client,blocking,add'(non-blocking,group)) sforceka(client,forceka') f-join-req(client,group,grouptype) if isevs(grouptype) /\ islazyct(laziness) /\ forceka' := add(forceka,group) . --- lazyst crl ssp-join-req(client,group,grouptype,laziness,katype) sgrptype(client,vsgrp,evsgrp) slaziness(client,lazyst,lazyct,eager) skatype(client,blocking,non-blocking) => ssp-join-req'(client,group,grouptype,laziness,katype) sgrptype(client,add'(vsgrp,group),evsgrp) slaziness(client,add'(lazyst,group),lazyct,eager) skatype(client,blocking,add'(non-blocking,group)) f-join-req(client,group,grouptype) if isvs(grouptype) /\ islazyst(laziness) . crl ssp-join-req(client,group,grouptype,laziness,katype) sgrptype(client,vsgrp,evsgrp) slaziness(client,lazyst,lazyct,eager) skatype(client,blocking,non-blocking) => ssp-join-req'(client,group,grouptype,laziness,katype) sgrptype(client,vsgrp,add'(evsgrp,group)) slaziness(client,add'(lazyst,group),lazyct,eager) skatype(client,blocking,add'(non-blocking,group)) f-join-req(client,group,grouptype) if isevs(grouptype) /\ islazyst(laziness) . --- eager crl ssp-join-req(client,group,grouptype,laziness,katype) sgrptype(client,vsgrp,evsgrp) slaziness(client,lazyst,lazyct,eager) skatype(client,blocking,non-blocking) sforceka(client,forceka) => ssp-join-req'(client,group,grouptype,laziness,katype) sgrptype(client,add'(vsgrp,group),evsgrp) slaziness(client,lazyst,lazyct,add'(eager,group)) skatype(client,blocking,add'(non-blocking,group)) sforceka(client,forceka') f-join-req(client,group,grouptype) if isvs(grouptype) /\ iseager(laziness) /\ forceka' := add(forceka,group) . crl ssp-join-req(client,group,grouptype,laziness,katype) sgrptype(client,vsgrp,evsgrp) slaziness(client,lazyst,lazyct,eager) skatype(client,blocking,non-blocking) sforceka(client,forceka) => ssp-join-req'(client,group,grouptype,laziness,katype) sgrptype(client,add'(vsgrp,group),evsgrp) slaziness(client,lazyst,lazyct,add'(eager,group)) skatype(client,add'(blocking,group),non-blocking) sforceka(client,forceka') f-join-req(client,group,grouptype) if isvs(grouptype) /\ iseager(laziness) /\ isblocking(katype) /\ forceka' := add(forceka,group) . crl ssp-join-req(client,group,grouptype,laziness,katype) sgrptype(client,vsgrp,evsgrp) slaziness(client,lazyst,lazyct,eager) skatype(client,blocking,non-blocking) sforceka(client,forceka) => ssp-join-req'(client,group,grouptype, laziness,katype) sgrptype(client,vsgrp,add'(evsgrp,group)) slaziness(client,lazyst,lazyct,add'(eager,group)) skatype(client,blocking,add'(non-blocking,group)) sforceka(client,forceka') f-join-req(client,group,grouptype) if isevs(grouptype) /\ iseager(laziness) /\ forceka' := add(forceka,group) . rl ssp-join-req'(client,group,grouptype,laziness,katype) f-join-ack(client) => ssp-join-ack(client) . rl ssp-join-req'(client,group,grouptype,laziness,katype) f-join-err(client,error) => ssp-join-err(client,error) . ----------------------- --- ssp-leave ----------------------- op ssp-leave-req' : Agent Group -> State . crl ssp-leave-req(client,group) sgrptype(client,vsgrp,evsgrp) => ssp-leave-req'(client,group) sgrptype(client,rm(vsgrp,group),evsgrp) f-leave-req(client,group) if contains(vsgrp,group) . crl ssp-leave-req(client,group) sgrptype(client,vsgrp,evsgrp) => ssp-leave-req'(client,group) sgrptype(client,vsgrp,rm(evsgrp,group)) f-leave-req(client,group) if contains(evsgrp,group) . rl ssp-leave-req'(client,group) sfreshness(client,freshkey) f-leave-ack(client) => sfreshness(client,rm(freshkey,group)) ssp-leave-ack(client) . rl ssp-leave-req'(client,group) f-leave-err(client,error) => ssp-leave-err(client,error) . ----------------------- --- ssp-multicast ----------------------- op ssp-multicast-req' : Agent Mode Group SData -> State . op ssp-multicast-req'' : Agent Mode Group SData -> State . op ssp-multicast-req-check-rekey : Agent Mode Group SData -> State . op ssp-multicast-req-trigger-rekey : Agent Mode Group SData -> State . op ssp-multicast-req-wait-for-rekey : Agent Mode Group SData -> State . var viewkeyid : KeyId . var mode : Mode . --- Ultra-secure -> user msg is encrypted using the key associated with --- the most current keyid and broadcast afterwards crl sstate(client,secure,cm,pt,ft,fo,kl) scontext(client,currkeyid,groupcontextset) ssp-multicast-req(client,mode,group,sdata) sgroupkeylist(client,groupassockeylistset) slaziness(client,lazyst,lazyct,eager) => sstate(client,secure,cm,pt,ft,fo,kl) scontext(client,currkeyid,groupcontextset) ssp-multicast-req'(client,mode,group,sdata) sgroupkeylist(client,groupassockeylistset) slaziness(client,lazyst,lazyct,eager) f-multicast-req(client,mode,group,fdata) if key := partialkey(lookup((get(groupassockeylistset,group)), currkeyid)) /\ fdata := enc(currkeyid,key,sdata) /\ not(contains(lazyst,group)) . --- Blocking ultra-secure -> data transmitted only in secure state crl sstate(client,secure,cm,pt,ft,fo,kl) scontext(client,currkeyid,groupcontextset) ssp-multicast-req(client,mode,group,sdata) sgroupkeylist(client,groupassockeylistset) slaziness(client,lazyst,lazyct,eager) skatype(client,blocking,non-blocking) => sstate(client,secure,cm,pt,ft,fo,kl) scontext(client,currkeyid,groupcontextset) ssp-multicast-req'(client,mode,group,sdata) sgroupkeylist(client,groupassockeylistset) slaziness(client,lazyst,lazyct,eager) skatype(client,blocking,non-blocking) f-multicast-req(client,mode,group,fdata) if key := partialkey(lookup((get(groupassockeylistset,group)), currkeyid)) /\ fdata := enc(currkeyid,key,sdata) /\ contains(secure,group) /\ contains(blocking,group) /\ not(contains(lazyst,group)) . --- Sending-view -> user msg is encrypted using the key associated with the --- requested sending view and broadcast afterwards crl sstate(client,secure,cm,pt,ft,fo,kl) scontext(client,currkeyid,groupcontextset) ssp-multicast-req(client,mode,group,sdata,req-sending-view) sgroupkeylist(client,groupassockeylistset) sgroupmembsetlist(client,groupassocmembsetlistset) slaziness(client,lazyst,lazyct,eager) siview(client,viewset) => sstate(client,secure,cm,pt,ft,fo,kl) scontext(client,currkeyid,groupcontextset) ssp-multicast-req'(client,mode,group,sdata) sgroupkeylist(client,groupassockeylistset) sgroupmembsetlist(client,groupassocmembsetlistset) slaziness(client,lazyst,lazyct,eager) siview(client,viewset) f-multicast-req(client,mode,group,fdata) if viewkeyid := keyid(lookup((get(groupassocmembsetlistset, group)), agentset(members(get(viewset,group))))) /\ key := partialkey(lookup((get(groupassockeylistset,group)), viewkeyid)) /\ fdata := enc(currkeyid,key,sdata) /\ not(contains(lazyst,group)) . --- Fresh-secure -> user msg is encrypted using a recently generated key --- and broadcast afterwards --- --- Note: if no message has been sent in the current view (!freshkey), a new key --- will be generated; oterwise key and its keyid exist --- if (sending-time) /\ (freshkey), encrypt and broadcast message crl sstate(client,secure,cm,pt,ft,fo,kl) scontext(client,currkeyid,groupcontextset) ssp-multicast-req(client,mode,group,sdata) sgroupkeylist(client,groupassockeylistset) sgroupmembsetlist(client,groupassocmembsetlistset) slaziness(client,lazyst,lazyct,eager) sfreshness(client,freshkey) siview(client,viewset) => sstate(client,secure,cm,pt,ft,fo,kl) scontext(client,currkeyid,groupcontextset) ssp-multicast-req'(client,mode,group,sdata) sgroupkeylist(client,groupassockeylistset) sgroupmembsetlist(client,groupassocmembsetlistset) slaziness(client,lazyst,lazyct,eager) sfreshness(client,freshkey) siview(client,viewset) f-multicast-req(client,mode,group,fdata) if contains(lazyst,group) /\ contains(freshkey,group) /\ contains(secure,group) /\ contains(get(groupassockeylistset,group), currkeyid) /\ key := partialkey(lookup((get(groupassockeylistset,group)), currkeyid)) /\ fdata := enc(currkeyid,key,sdata) . --- if (sending-time) /\ not(freshkey), check-rekey crl sstate(client,secure,cm,pt,ft,fo,kl) scontext(client,currkeyid,groupcontextset) ssp-multicast-req(client,mode,group,sdata) slaziness(client,lazyst,lazyct,eager) sfreshness(client,freshkey) => sstate(client,secure,cm,pt,ft,fo,kl) scontext(client,currkeyid,groupcontextset) slaziness(client,lazyst,lazyct,eager) sfreshness(client,freshkey) ssp-multicast-req-check-rekey(client,mode,group,sdata) if contains(lazyst,group) /\ not(contains(freshkey,group)) . --- check-rekey: if (kainprogress), buffer message and return ack crl sstate(client,secure,cm,pt,ft,fo,kl) scontext(client,currkeyid,groupcontextset) ssp-multicast-req-check-rekey(client,mode,group,sdata) slaziness(client,lazyst,lazyct,eager) skainprogress(client,kainprogress) => sstate(client,secure,cm,pt,ft,fo,kl) scontext(client,currkeyid,groupcontextset) slaziness(client,lazyst,lazyct,eager) skainprogress(client,kainprogress) ssp-multicast-req-wait-for-rekey(client,mode,group,sdata) --- buffer msg ssp-multicast-ack(client) --- return ack if contains(lazyst,group) /\ contains(kainprogress,group) . --- check-rekey: if not(rainprogress), set kainprogress and trigger rekey crl sstate(client,secure,cm,pt,ft,fo,kl) scontext(client,currkeyid,groupcontextset) ssp-multicast-req-check-rekey(client,mode,group,sdata) slaziness(client,lazyst,lazyct,eager) skainprogress(client,kainprogress) => sstate(client,secure,cm,pt,ft,fo,kl) scontext(client,currkeyid,groupcontextset) slaziness(client,lazyst,lazyct,eager) skainprogress(client,kainprogress) ssp-multicast-req-trigger-rekey(client,mode,group,sdata) if contains(lazyst,group) /\ not(contains(kainprogress,group)) . crl sstate(client,secure,cm,pt,ft,fo,kl) scontext(client,currkeyid,groupcontextset) ssp-multicast-req-trigger-rekey(client,mode,group,sdata) slaziness(client,lazyst,lazyct,eager) skainprogress(client,kainprogress) => sstate(client,secure,cm,pt,ft,fo,kl) scontext(client,currkeyid,groupcontextset) slaziness(client,lazyst,lazyct,eager) skainprogress(client,add'(kainprogress,group)) ssp-multicast-req-wait-for-rekey(client,mode,group,sdata) --- buffer msg ssp-multicast-ack(client) --- return ack f-flushreq-now(client,group) --- trigger rekey if contains(lazyst,group) . --- rekey finished when freshkey is set in KL, reset kainprogress and proceed crl sstate(client,secure,cm,pt,ft,fo,kl) scontext(client,currkeyid,groupcontextset) ssp-multicast-req-wait-for-rekey(client,mode,group,sdata) f-flushok-ack(client) sgroupkeylist(client,groupassockeylistset) sgroupmembsetlist(client,groupassocmembsetlistset) slaziness(client,lazyst,lazyct,eager) sfreshness(client,freshkey) siview(client,viewset) => sstate(client,secure,cm,pt,ft,fo,kl) scontext(client,currkeyid,groupcontextset) sgroupkeylist(client,groupassockeylistset) sgroupmembsetlist(client,groupassocmembsetlistset) slaziness(client,lazyst,lazyct,eager) sfreshness(client,freshkey) siview(client,viewset) ssp-multicast-req''(client,mode,group,sdata) f-multicast-req(client,mode,group,fdata) if contains(lazyst,group) /\ contains(freshkey,group) /\ key := partialkey(lookup((get(groupassockeylistset,group)), currkeyid)) /\ fdata := enc(currkeyid,key,sdata) . rl ssp-multicast-req''(client,mode,group,sdata) f-multicast-ack(client) => eState . 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 ssp-flushok-req from app -> see ssp-flushok --- NO STATE - receive freq msg -> deliver freq msg 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) sgroupkeylist(client,groupassockeylistset) sgroupmembsetlist(client,groupassocmembsetlistset) => sstate(client,secure,cm,pt,ft,fo,kl) swaitforsfok(client,waitforsfok') sbuffer(client,smessagelist sSMessageList(conv(fmessage))) ssp-receive-req(client) sgroupkeylist(client, groupassockeylistset') sgroupmembsetlist(client,groupassocmembsetlistset') if isfreq(fmessage) /\ group := group(fmessage) /\ not(contains(cm pt ft fo kl, group)) /\ not(contains(waitforsfok,group)) /\ waitforsfok' := add(waitforsfok,group) /\ groupassockeylistset' := add'(groupassockeylistset, group, eAssocKeyList) /\ groupassocmembsetlistset' := add'(groupassocmembsetlistset, group, eAssocMembSetList) . ------------------------------------------------------------------- --- RECEIVE DATA ANYTIME, ANY STATE ------------------------------------------------------------------- --- Decryptable message: Client has the pair (keyid,key), message --- is decrypted and delivered to the app crl siview(client,viewset) sstate(client,secure,cm,pt,ft,fo,kl) scontext(client,currkeyid,groupcontextset) ssp-receive-req'(client) sbuffer(client,smessagelist) f-receive-ack(client,fmessage) sgroupkeylist(client,groupassockeylistset) => siview(client,viewset) sstate(client,secure,cm,pt,ft,fo,kl) scontext(client,currkeyid,groupcontextset) sbuffer(client,smessagelist sSMessageList(smessage)) ssp-receive-req(client) sgroupkeylist(client,groupassockeylistset) if isidata(fmessage) /\ group := group(fmessage) /\ keyid' := keyid(data(fmessage)) /\ contains((get(groupassockeylistset, group)), keyid') /\ key := partialkey(lookup((get(groupassockeylistset, group)), keyid')) /\ smessage := conv(key,fmessage) . --- Non-decryptable message: Client does not have the key associated --- to the message keyid. The non-decrypted --- message is delivered to the app crl siview(client,viewset) sstate(client,secure,cm,pt,ft,fo,kl) scontext(client,currkeyid,groupcontextset) ssp-receive-req'(client) sbuffer(client,smessagelist) f-receive-ack(client,fmessage) sgroupkeylist(client,groupassockeylistset) => siview(client,viewset) sstate(client,secure,cm,pt,ft,fo,kl) scontext(client,currkeyid,groupcontextset) sbuffer(client,smessagelist sSMessageList(smessage)) ssp-receive-req(client) sgroupkeylist(client,groupassockeylistset) if isidata(fmessage) /\ group := group(fmessage) /\ keyid' := keyid(data(fmessage)) /\ not(contains((get(groupassockeylistset, group)), keyid')) /\ smessage := sdatamsg(client,group, nondecryptable(data(fmessage)),get(viewset,group)) . --- Delayed message: Client has the pair (keyid,key), but view is --- very old. Message is decrypted, tagged as delayed --- and delivered to the app crl siview(client,viewset) sstate(client,secure,cm,pt,ft,fo,kl) scontext(client,currkeyid,groupcontextset) ssp-receive-req'(client) sbuffer(client,smessagelist) f-receive-ack(client,fmessage) sgroupkeylist(client,groupassockeylistset) => siview(client,viewset) sstate(client,secure,cm,pt,ft,fo,kl) scontext(client,currkeyid,groupcontextset) sbuffer(client,smessagelist sSMessageList(smessage)) ssp-receive-req(client) sgroupkeylist(client,groupassockeylistset) if isidata(fmessage) /\ group := group(fmessage) /\ keyid' := keyid(data(fmessage)) /\ contains((get(groupassockeylistset, group)), keyid') /\ key := partialkey(lookup((get(groupassockeylistset, group)), keyid')) /\ index(get(viewset,group)) >= (s s s s s s s (index(view(fmessage)))) /\ smessage := sdatamsg(client,group, delayed(conv(key,fmessage)),get(viewset,group)) . ------------------------------------------------------------------- --- SECURE STATE BEHAVIOR ------------------------------------------------------------------- --- SECURE - receive ssp-flushok-req from app -> see ssp-flushok --- SECURE - receive user msg -> see ssp-multicast --- SECURE - receive fdata msg -> see receive data anytime --- SECURE - receive 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 - 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) . --- SECURE - fselfleave msg -> delete view for affected group, --- deliver fselfleave msg to app --- --- Note: in all other states, fselfleave is 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 ------------------------------------------------------------------- --- PT,FT,FO,KL,CM - receive user msg -> see ssp-multicast --- PT,FT,FO,KL,CM - receive fdata msg -> see receive data anytime op ssp-wait-for-flushok : Agent Group -> State . --- PT,FT,FO - receive freq msg -> send f-flushok-req 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 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) 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 ------------------------------------------------------------------- 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,currkeyid,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,currkeyid,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,currkeyid,groupcontextset) clq-update-key-intermediate-ack(client,group,context,token) => ssp-pt-wait-for-partial-token-unicast(client,group) scontext(client,currkeyid,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) . --- PT - receive partial token -> I am the new controller crl ssp-receive-req'(client) sstate(client,secure,cm,pt,ft,fo,kl) scontext(client,currkeyid,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,currkeyid,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,currkeyid,groupcontextset) clq-update-key-last-ack(client,group,context,token) => ssp-pt-wait-for-final-token-multicast(client,group) scontext(client,currkeyid,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 ------------------------------------------------------------------- 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,currkeyid,groupcontextset) f-receive-ack(client,fmessage) => ssp-ft-wait-for-factor-out(client,group) sstate(client,secure,cm,pt,ft,fo,kl) scontext(client,currkeyid,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,currkeyid,groupcontextset) clq-factor-out-ack(client,group,context,token) => ssp-ft-wait-for-factor-out-unicast(client,group) scontext(client,currkeyid,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 ------------------------------------------------------------------- op ssp-fo-wait-for-merge : Agent Group -> State . op ssp-fo-wait-for-keylist-multicast : Agent Group -> State . var received : AgentSet . --- FO - receive factor out token crl ssp-receive-req'(client) sstate(client,secure,cm,pt,ft,fo,kl) scontext(client,currkeyid,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,currkeyid,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,currkeyid,groupcontextset) sforeceived(client,foreceived) clq-merge-ack(client,group,context,received) => scontext(client,currkeyid,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,currkeyid,groupcontextset) sforeceived(client,foreceived) clq-merge-ack(client,group,context,received,token) freshkeyid(rnum) => freshkeyid(s rnum) scontext(client,currkeyid,groupcontextset') sforeceived(client,foreceived') ssp-fo-wait-for-keylist-multicast(client,group) f-multicast-req(client,agreed,group,stokenmsg(token,keyid(rnum))) 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) . --- FO - 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 ------------------------------------------------------------------- op ssp-kl-wait-for-flushok : Agent Group -> State . op ssp-kl-wait-for-update-ctx : Agent Group KeyId -> State . op ssp-kl-check-for-flushok : Agent Group -> State . op ssp-kl-wait-for-flushok' : Agent Group -> State . --- KL - receive freq msg -> if (vstrans), send f-flushok-req to flushlayer, --- and 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 not(vstrans), set sklgotfreq 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,currkeyid,groupcontextset) f-receive-ack(client,fmessage) => ssp-kl-wait-for-update-ctx(client,group,keyid) sstate(client,secure,cm,pt,ft,fo,kl) svstrans(client,vstrans) scontext(client,currkeyid,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)) /\ keyid := keyid(data(fmessage)) /\ context := get(groupcontextset, group) . --- KL (VS semantics) -> pass conf to app crl ssp-kl-wait-for-update-ctx(client,group,keyid) sstate(client,secure,cm,pt,ft,fo,kl) sgrptype(client,vsgrp,evsgrp) svsset(client,vsset) snotfirsttrans(client,notfirsttrans) snotfirstcm(client,notfirstcm) scontext(client,currkeyid,groupcontextset) snewmembmsg(client,newmembmsgset) sbuffer(client,smessagelist) clq-update-ctx-ack(client,group,context) sgroupkeylist(client,groupassockeylistset) sgroupmembsetlist(client,groupassocmembsetlistset) slaziness(agent,lazyst,lazyct,eager) sfreshness(client,freshkey) skainprogress(client,kainprogress) => sstate(client,secure',cm,pt,ft,fo,kl') sgrptype(client,vsgrp,evsgrp) svsset(client,vsset) sbuffer(client,smessagelist sSMessageList(smessage)) ssp-kl-check-for-flushok(client,group) scontext(client,currkeyid',groupcontextset') snotfirsttrans(client,notfirsttrans') snotfirstcm(client,notfirstcm') snewmembmsg(client,newmembmsgset) sgroupkeylist(client,groupassockeylistset') sgroupmembsetlist(client,groupassocmembsetlistset') slaziness(agent,lazyst,lazyct,eager) sfreshness(client,add'(freshkey,group)) skainprogress(client,rm(kainprogress,group)) 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) /\ key := groupsecret(context) /\ currkeyid' := keyid /\ assockeylist := get(groupassockeylistset, group) /\ assockeylist' := add'(assockeylist, (assockey(key, keyid))) /\ groupassockeylistset' := update(groupassockeylistset,group,assockeylist') /\ assocmembsetlist := get(groupassocmembsetlistset, group) /\ assocmembsetlist' := add'(assocmembsetlist, (assocmembset(agentset(members(context)), currkeyid'))) /\ groupassocmembsetlistset' := update(groupassocmembsetlistset,group,assocmembsetlist') /\ secure' := add(secure,group) /\ contains(vsgrp,group) . --- KL (EVS semantics) crl ssp-kl-wait-for-update-ctx(client,group,keyid) sstate(client,secure,cm,pt,ft,fo,kl) sgrptype(client,vsgrp,evsgrp) svsset(client,vsset) snotfirsttrans(client,notfirsttrans) snotfirstcm(client,notfirstcm) scontext(client,currkeyid,groupcontextset) snewmembmsg(client,newmembmsgset) clq-update-ctx-ack(client,group,context) sgroupkeylist(client,groupassockeylistset) sgroupmembsetlist(client,groupassocmembsetlistset) slaziness(agent,lazyst,lazyct,eager) sfreshness(client,freshkey) skainprogress(client,kainprogress) => sstate(client,secure',cm,pt,ft,fo,kl') sgrptype(client,vsgrp,evsgrp) svsset(client,vsset) ssp-kl-check-for-flushok(client,group) scontext(client,currkeyid',groupcontextset') snotfirsttrans(client,notfirsttrans') snotfirstcm(client,notfirstcm') snewmembmsg(client,newmembmsgset) sgroupkeylist(client,groupassockeylistset') sgroupmembsetlist(client,groupassocmembsetlistset') slaziness(agent,lazyst,lazyct,eager) sfreshness(client,add'(freshkey,group)) skainprogress(client,rm(kainprogress,group)) if groupcontextset' := update(groupcontextset, group, context) /\ notfirsttrans' := rm(notfirsttrans, group) /\ notfirstcm' := rm(notfirstcm, group) /\ kl' := rm(kl,group) /\ key := groupsecret(context) /\ currkeyid' := keyid /\ assockeylist := get(groupassockeylistset, group) /\ assockeylist' := add'(assockeylist, (assockey(key, keyid))) /\ groupassockeylistset' := update(groupassockeylistset,group,assockeylist') /\ assocmembsetlist := get(groupassocmembsetlistset, group) /\ assocmembsetlist' := add'(assocmembsetlist, (assocmembset(agentset(members(context)), currkeyid'))) /\ groupassocmembsetlistset' := update(groupassocmembsetlistset,group,assocmembsetlist') /\ secure' := add(secure,group) /\ not(contains(vsgrp,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 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) 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 ------------------------------------------------------------------- op ssp-cm-check-members : Agent Group FMessage -> State . op ssp-cm-check-forceka : Agent Group FMessage -> State . op ssp-cm-avoid-rekey : Agent Group FMessage -> State . op ssp-cm-cases : Agent Group FMessage -> State . op ssp-cm-eager : 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 . var leaveset : AgentSet . --- CM (all) - receive freq msg -> DO THE HARD WORK 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-check-forceka(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) . ----------------- --- Sending-time: if not(forceka), reset freshness flag and avoid rekey ----------------- crl ssp-cm-check-forceka(client,group,fmessage) sforceka(client,forceka) sfreshness(client,freshkey) sshadowmessage(client,shadowmessage) => sforceka(client,forceka) sfreshness(client,rm(freshkey,group)) sshadowmessage(client,rm(shadowmessage,shadowmessage)) ssp-cm-avoid-rekey(client,group,fmessage) if not(contains(forceka,group)) . --- CM (sending-time) -> avoid rekey /\ I'm alone crl ssp-cm-avoid-rekey(client,group,fmessage) sstate(client,secure,cm,pt,ft,fo,kl) scontext(client,currkeyid,groupcontextset) snewmembmsg(client,newmembmsgset) sshadowmessage(client,shadowmessage) sbuffer(client,smessagelist) => sstate(client,secure',cm',pt,ft,fo,kl) scontext(client,currkeyid,groupcontextset) snewmembmsg(client,newmembmsgset) sshadowmessage(client,add'(shadowmessage,fmessage)) sbuffer(client,smessagelist sSMessageList(smessage)) ssp-receive-req(client) if agentset(members(view(fmessage))) == sAgentSet(client) /\ smessage := update-transset(get(newmembmsgset, group), sAgentSet(client)) /\ cm' := rm(cm, group) /\ secure' := add(secure, group) . --- CM (sending-time) -> avoid rekey /\ I'm not alone crl ssp-cm-avoid-rekey(client,group,fmessage) sstate(client,secure,cm,pt,ft,fo,kl) scontext(client,currkeyid,groupcontextset) snewmembmsg(client,newmembmsgset) svsset(client,vsset) snotfirstcm(client,notfirstcm) sshadowmessage(client,shadowmessage) sbuffer(client,smessagelist) => sstate(client,secure',cm',pt,ft,fo,kl) scontext(client,currkeyid,groupcontextset) snewmembmsg(client,newmembmsgset) svsset(client,vsset) snotfirstcm(client,notfirstcm') sshadowmessage(client,add'(shadowmessage,fmessage)) sbuffer(client,smessagelist sSMessageList(smessage)) ssp-receive-req(client) if card(agentset(members(view(fmessage)))) > 1 /\ notfirstcm' := rm(notfirstcm, group) /\ smessage := update-transset(get(newmembmsgset,group), get(vsset, group)) /\ cm' := rm(cm, group) /\ secure' := add(secure, group) . ----------------- --- Sending-time: if (forceka), rekey ----------------- op ssp-cm-forceka : Agent Group FMessage -> State . var fmessage' : FMessage . crl ssp-cm-check-forceka(client,group,fmessage) sforceka(client,forceka) slaziness(client,lazyst,lazyct,eager) sshadowmessage(client,shadowmessage) => sforceka(client,forceka) slaziness(client,lazyst,lazyct,eager) sshadowmessage(client,shadowmessage) ssp-cm-forceka(client,group,fmessage) if contains(forceka,group) /\ contains(lazyst,group) . crl ssp-cm-forceka(client,group,fmessage) slaziness(client,lazyst,lazyct,eager) sforceka(client,forceka) sfreshness(client,freshkey) sshadowmessage(client,shadowmessage) => slaziness(client,lazyst,lazyct,eager) sforceka(client,rm(forceka,group)) sfreshness(client,rm(freshkey,group)) sshadowmessage(client,shadowmessage) ssp-cm-check-members(client,group,fmessage) if contains(lazyst,group) . ------------------ --- Changing-time: if (forceka), rekey ------------------ crl ssp-cm-check-forceka(client,group,fmessage) sforceka(client,forceka) slaziness(client,lazyst,lazyct,eager) => sforceka(client,forceka) slaziness(client,lazyst,lazyct,eager) ssp-cm-check-members(client,group,fmessage) if contains(forceka,group) /\ contains(lazyct,group) . crl ssp-cm-check-forceka(client,group,fmessage) sforceka(client,forceka) slaziness(client,lazyst,lazyct,eager) => sforceka(client,forceka) slaziness(client,lazyst,lazyct,eager) ssp-cm-cases(client,group,fmessage) if contains(forceka,group) /\ not(contains(lazyct,group)) . --- CM (changing-time) -> same members /\ I'm alone crl ssp-cm-check-members(client,group,fmessage) sstate(client,secure,cm,pt,ft,fo,kl) scontext(client,currkeyid,groupcontextset) snewmembmsg(client,newmembmsgset) sbuffer(client,smessagelist) sgroupkeylist(client,groupassockeylistset) sgroupmembsetlist(client,groupassocmembsetlistset) sfreshness(client,freshkey) skainprogress(client,kainprogress) freshkeyid(rnum) => sstate(client,secure',cm',pt,ft,fo,kl) scontext(client,currkeyid',groupcontextset) snewmembmsg(client,newmembmsgset) sbuffer(client,smessagelist sSMessageList(smessage)) sgroupkeylist(client,groupassockeylistset') sgroupmembsetlist(client,groupassocmembsetlistset') sfreshness(client,add'(freshkey,group)) skainprogress(client,rm(kainprogress,group)) freshkeyid(s rnum) ssp-receive-req(client) if contains((get(groupassocmembsetlistset, group)), agentset(members(view(fmessage)))) /\ agentset(members(view(fmessage))) == sAgentSet(client) /\ keyid' := keyid(lookup((get(groupassocmembsetlistset, group)), agentset(members(view(fmessage))))) /\ key := partialkey(lookup((get(groupassockeylistset,group)), keyid')) /\ currkeyid' := keyid(rnum) /\ assockeylist := get(groupassockeylistset, group) /\ assockeylist' := add'(assockeylist, (assockey(key, currkeyid'))) /\ groupassockeylistset' := update(groupassockeylistset,group,assockeylist') /\ assocmembsetlist := get(groupassocmembsetlistset, group) /\ assocmembsetlist' := add'(assocmembsetlist, (assocmembset(agentset(members(view(fmessage))), currkeyid'))) /\ groupassocmembsetlistset' := update(groupassocmembsetlistset,group,assocmembsetlist') /\ smessage := update-transset(get(newmembmsgset, group), sAgentSet(client)) /\ cm' := rm(cm, group) /\ secure' := add(secure, group) . --- CM (changing-time)- > same members /\ I'm not alone crl ssp-cm-check-members(client,group,fmessage) sstate(client,secure,cm,pt,ft,fo,kl) scontext(client,currkeyid,groupcontextset) snewmembmsg(client,newmembmsgset) svsset(client,vsset) snotfirstcm(client,notfirstcm) sbuffer(client,smessagelist) sgroupkeylist(client,groupassockeylistset) sgroupmembsetlist(client,groupassocmembsetlistset) sfreshness(client,freshkey) skainprogress(client,kainprogress) => sstate(client,secure',cm',pt,ft,fo,kl) scontext(client,currkeyid',groupcontextset) snewmembmsg(client,newmembmsgset) svsset(client,vsset) snotfirstcm(client,notfirstcm') sbuffer(client,smessagelist sSMessageList(smessage)) sgroupkeylist(client,groupassockeylistset') sgroupmembsetlist(client,groupassocmembsetlistset') sfreshness(client,add'(freshkey,group)) skainprogress(client,rm(kainprogress,group)) ssp-receive-req(client) if contains((get(groupassocmembsetlistset, group)), agentset(members(view(fmessage)))) /\ card(agentset(members(view(fmessage)))) > 1 /\ keyid' := keyid(lookup((get(groupassocmembsetlistset, group)), agentset(members(view(fmessage))))) /\ currkeyid' := keyid' /\ key := partialkey(lookup((get(groupassockeylistset,group)), keyid')) /\ assockeylist := get(groupassockeylistset, group) /\ assockeylist' := add'(assockeylist, (assockey(key, currkeyid'))) /\ groupassockeylistset' := update(groupassockeylistset,group,assockeylist') /\ assocmembsetlist := get(groupassocmembsetlistset, group) /\ assocmembsetlist' := add'(assocmembsetlist, (assocmembset(agentset(members(view(fmessage))), currkeyid'))) /\ groupassocmembsetlistset' := update(groupassocmembsetlistset,group,assocmembsetlist') /\ notfirstcm' := rm(notfirstcm, group) /\ smessage := update-transset(get(newmembmsgset,group), get(vsset, group)) /\ cm' := rm(cm, group) /\ secure' := add(secure, group) . --- CM (changing-time) -> no recurrent members => trigger eager rekey crl ssp-cm-check-members(client,group,fmessage) sgroupmembsetlist(client,groupassocmembsetlistset) => ssp-cm-cases(client,group,fmessage) sgroupmembsetlist(client,groupassocmembsetlistset) if not(contains((get(groupassocmembsetlistset, group)), agentset(members(view(fmessage))))) . ----------- --- Eager: Always rekey ----------- --- CM (eager) -> rekey /\ 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,currkeyid,groupcontextset) snewcontroller(client,newcontroller) snewmembmsg(client,newmembmsgset) sbuffer(client,smessagelist) clq-first-user-ack(client,group,context) freshkeyid(rnum) sgroupkeylist(client,groupassockeylistset) sgroupmembsetlist(client,groupassocmembsetlistset) sfreshness(client,freshkey) => sstate(client,secure',cm',pt,ft,fo,kl) sbuffer(client,smessagelist sSMessageList(smessage)) scontext(client,currkeyid',groupcontextset') snewcontroller(client,newcontroller') snewmembmsg(client,newmembmsgset) ssp-receive-req(client) freshkeyid(s rnum) sgroupkeylist(client,groupassockeylistset') sgroupmembsetlist(client,groupassocmembsetlistset') sfreshness(client,add'(freshkey,group)) if groupcontextset' := update(groupcontextset, group, context) /\ newcontroller' := add(newcontroller, group) /\ smessage := update-transset(get(newmembmsgset, group),sAgentSet(client)) /\ cm' := rm(cm, group) /\ key := groupsecret(context) /\ currkeyid' := keyid(rnum) /\ assockeylist := get(groupassockeylistset, group) /\ assockeylist' := add'(assockeylist, (assockey(key, currkeyid'))) /\ groupassockeylistset' := update(groupassockeylistset,group,assockeylist') /\ assocmembsetlist := get(groupassocmembsetlistset, group) /\ assocmembsetlist' := add'(assocmembsetlist, (assocmembset(agentset(members(context)), currkeyid'))) /\ groupassocmembsetlistset' := update(groupassocmembsetlistset,group,assocmembsetlist') /\ secure' := add(secure, group) . --- CM (eager) -> rekey /\ 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 . --- CM (VS-eager) -> conf will be passed in KL state crl ssp-cm-not-alone-wait-for-new-user(client,group,fmessage) sstate(client,secure,cm,pt,ft,fo,kl) sgrptype(client,vsgrp,evsgrp) scontext(client,currkeyid,groupcontextset) clq-new-user-ack(client,group,context) => sstate(client,secure,cm',pt',ft,fo,kl) sgrptype(client,vsgrp,evsgrp) scontext(client,currkeyid,groupcontextset') ssp-receive-req(client) if groupcontextset' := update(groupcontextset, group, context) /\ cm' := rm(cm, group) /\ pt' := add(pt, group) /\ contains(vsgrp,group) . --- CM (EVS-eager) -> pass conf to appl crl ssp-cm-not-alone-wait-for-new-user(client,group,fmessage) sstate(client,secure,cm,pt,ft,fo,kl) sgrptype(client,vsgrp,evsgrp) snewmembmsg(client,newmembmsgset) svsset(client,vsset) scontext(client,currkeyid,groupcontextset) clq-new-user-ack(client,group,context) sbuffer(client,smessagelist) => sstate(client,secure,cm',pt',ft,fo,kl) sgrptype(client,vsgrp,evsgrp) snewmembmsg(client,newmembmsgset) svsset(client,vsset) scontext(client,currkeyid,groupcontextset') sbuffer(client,smessagelist sSMessageList(smessage)) ssp-receive-req(client) if groupcontextset' := update(groupcontextset, group, context) /\ smessage := update-transset(get(newmembmsgset,group), get(vsset, group)) /\ cm' := rm(cm, group) /\ pt' := add(pt, group) /\ not(contains(vsgrp,group)) . --- CM (eager) -> rekey /\ 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 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,currkeyid,groupcontextset) clq-first-user-ack(client,group,context) => ssp-cm-not-alone-wait-for-update-key-first(client,group,fmessage,mergingagents) scontext(client,currkeyid,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,currkeyid,groupcontextset) clq-update-key-first-ack(client,group,context,token) => ssp-cm-not-alone-wait-for-unicast(client,group,fmessage,mergingagents) scontext(client,currkeyid,groupcontextset') f-multicast-req(client,fifo,privategroup(next(members( groupmemberlist(context)),client)),stokenmsg(token)) if groupcontextset' := update(groupcontextset, group, context) . --- CM (VS-eager) -> conf will be passed in KL state crl ssp-cm-not-alone-wait-for-unicast(client,group,fmessage,mergingagents) sstate(client,secure,cm,pt,ft,fo,kl) sgrptype(client,vsgrp,evsgrp) f-multicast-ack(client) => sstate(client,secure,cm',pt,ft',fo,kl) sgrptype(client,vsgrp,evsgrp) ssp-receive-req(client) if cm' := rm(cm, group) /\ ft' := add(ft, group) /\ contains(vsgrp,group) . --- CM (EVS-eager) -> pass conf to appl crl ssp-cm-not-alone-wait-for-unicast(client,group,fmessage,mergingagents) sstate(client,secure,cm,pt,ft,fo,kl) sgrptype(client,vsgrp,evsgrp) snewmembmsg(client,newmembmsgset) svsset(client,vsset) sbuffer(client,smessagelist) f-multicast-ack(client) => sstate(client,secure,cm',pt,ft',fo,kl) sgrptype(client,vsgrp,evsgrp) snewmembmsg(client,newmembmsgset) svsset(client,vsset) sbuffer(client,smessagelist sSMessageList(smessage)) ssp-receive-req(client) if smessage := update-transset(get(newmembmsgset,group), get(vsset, group)) /\ cm' := rm(cm, group) /\ ft' := add(ft, group) /\ not(contains(vsgrp,group)) . --- CM (all) - ignore pt,ft,fo, kl msgs 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 . --- NO STATE - receive ssp-flushok-req msg -> if (waitforsfok),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 not(contains(secure cm pt ft fo kl,group)) /\ contains(waitforsfok,group) /\ cm' := add(cm,group) /\ waitforsfok' := rm(waitforsfok,group) . --- SECURE - receive ssp-flushok-req msg -> if (waitforsfok), 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) . --- ANY STATE - receive ssp-flushok-req msg -> if not(waitforsfok), 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, 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