fmod SMESSAGE is protecting BOOL . protecting NAT . protecting STRING . protecting FLUSHSPREAD . protecting CLIQUES . var client agent : Agent . var group group' : Group . var agentset agentset' : AgentSet . var token : Token . var view : View . var transset transset' : AgentSet . var fdata : FData . var error : Error . var key : PartialKey . --- KeyId sort KeyId . op keyid : Nat -> KeyId . var keyid keyid' : KeyId . --- key agreement type sort KAType . op blocking : -> KAType . op non-blocking : -> KAType . var katype : KAType . op isblocking : KAType -> Bool . eq isblocking(blocking) = true . eq isblocking(non-blocking) = false . op isnonblocking : KAType -> Bool . eq isnonblocking(blocking) = false . eq isnonblocking(non-blocking) = true . --- laziness mode sort Laziness . op eager : -> Laziness . op sending-time : -> Laziness . op changing-time : -> Laziness . op combined-sct : -> Laziness . var laziness : Laziness . op islazy : Laziness -> Bool . eq islazy(sending-time) = true . eq islazy(changing-time) = true . eq islazy(combined-sct) = true . eq islazy(eager) = false . op islazyst : Laziness -> Bool . eq islazyst(sending-time) = true . eq islazyst(changing-time) = false . eq islazyst(combined-sct) = true . eq islazyst(eager) = false . op islazyct : Laziness -> Bool . eq islazyct(sending-time) = false . eq islazyct(changing-time) = true . eq islazyct(combined-sct) = false . eq islazyct(eager) = false . op islazysct : Laziness -> Bool . eq islazysct(sending-time) = false . eq islazysct(changing-time) = false . eq islazysct(combined-sct) = true . eq islazysct(eager) = false . op iseager : Laziness -> Bool . eq iseager(sending-time) = false . eq iseager(changing-time) = false . eq iseager(combined-sct) = false . eq iseager(eager) = true . --- freshness mode sort Freshness . op freshkey : -> Freshness . var freshness : Freshness . op isfreshkey : Freshness -> Bool . eq isfreshkey(freshkey) = true . --- custom mode sort Custom . op req-sending-view : -> Custom . var custom : Custom . op isviewrequested : Custom -> Bool . eq isviewrequested(req-sending-view) = true . --- secure spread messages sort SMessage . var smessage smessage' : SMessage . --- contents of secure spread a messages sort SData . op sdata : String -> SData . op nondecryptable : FData -> SData . op delayed : FData -> SData . op custom : FData -> SData . var sdata : SData . var flushtype : FlushType . --- secure spread messages subsort SMessage < FData . --- some secure layer messages are flush layer data --- messages visible to the upper layer op sdatamsg --- regular message : Agent --- sender Group --- all receivers SData --- contents View --- sending view -> SMessage . op sfreqmsg --- secure flush request message : Agent --- sender Group --- affected group -> SMessage . op sfreqmsg --- secure flush request message : Agent --- sender Group --- affected group FlushType --- force flush request -> SMessage . op stransmsg --- secure transitional view message : Group --- affected group -> SMessage . op sjoinmsg --- regular secure view message caused by join : Agent --- joining agent Group --- affected group View --- new view -> SMessage . op sleavemsg --- regular secure view message caused by leave : Agent --- joining agent Group --- affected group View --- new view -> SMessage . op sdisconnectmsg --- regular secure view message caused by disconnect : Agent --- disconnecting agent Group --- affected group View --- new view -> SMessage . op sconfmsg --- regular secure view message caused by network : Group --- affected group View --- new view AgentSet --- transitional set of agents -> SMessage . --- (i.e. agents that came with client into the new view) op sselfleavemsg --- selfleavemsg message : Agent --- leaving agent Group --- affected group -> SMessage . --- internal messages (not visible to the upper layer) op sdatamsg --- internal data message : KeyId --- keyId of the encryption key PartialKey --- encryption key SData --- contents -> SMessage . op stokenmsg --- internal cliques message : Token --- contents -> SMessage . op stokenmsg --- internal cliques message : Token --- contents KeyId --- new keyId for the new key -> SMessage . ----------------------- op issdata : SMessage ~> Bool . eq issdata(sdatamsg(client,group,sdata,view)) = true . eq issdata(stokenmsg(token)) = false . eq issdata(stokenmsg(token,keyid)) = false . eq issdata(sfreqmsg(client,group)) = false . eq issdata(sfreqmsg(client,group,flushtype)) = false . eq issdata(sjoinmsg(client,group,view)) = false . eq issdata(sleavemsg(client,group,view)) = false . eq issdata(stransmsg(group)) = false . eq issdata(sconfmsg(group,view,transset)) = false . eq issdata(sselfleavemsg(client,group)) = false . eq issdata(sdisconnectmsg(client,group,view)) = false . op issfreq : SMessage ~> Bool . eq issfreq(sdatamsg(client,group,sdata,view)) = false . eq issfreq(sfreqmsg(client,group)) = true . eq issfreq(sfreqmsg(client,group,flushtype)) = false . ---true . eq issfreq(sjoinmsg(client,group,view)) = false . eq issfreq(sleavemsg(client,group,view)) = false . eq issfreq(stransmsg(group)) = false . eq issfreq(sconfmsg(group,view,transset)) = false . eq issfreq(sselfleavemsg(client,group)) = false . eq issfreq(sdisconnectmsg(client,group,view)) = false . op issffreq : SMessage ~> Bool . eq issffreq(sdatamsg(client,group,sdata,view)) = false . eq issffreq(sfreqmsg(client,group)) = false . eq issffreq(sfreqmsg(client,group,flushtype)) = true . eq issffreq(sjoinmsg(client,group,view)) = false . eq issffreq(sleavemsg(client,group,view)) = false . eq issffreq(stransmsg(group)) = false . eq issffreq(sconfmsg(group,view,transset)) = false . eq issffreq(sselfleavemsg(client,group)) = false . eq issffreq(sdisconnectmsg(client,group,view)) = false . op issjoin : SMessage ~> Bool . eq issjoin(sdatamsg(client,group,sdata,view)) = false . eq issjoin(sfreqmsg(client,group)) = false . eq issjoin(sfreqmsg(client,group,flushtype)) = false . eq issjoin(sjoinmsg(client,group,view)) = true . eq issjoin(sleavemsg(client,group,view)) = false . eq issjoin(stransmsg(group)) = false . eq issjoin(sconfmsg(group,view,transset)) = false . eq issjoin(sselfleavemsg(client,group)) = false . eq issjoin(sdisconnectmsg(client,group,view)) = false . op issleave : SMessage ~> Bool . eq issleave(sdatamsg(client,group,sdata,view)) = false . eq issleave(sfreqmsg(client,group)) = false . eq issleave(sfreqmsg(client,group,flushtype)) = false . eq issleave(sjoinmsg(client,group,view)) = false . eq issleave(sleavemsg(client,group,view)) = true . eq issleave(stransmsg(group)) = false . eq issleave(sconfmsg(group,view,transset)) = false . eq issleave(sselfleavemsg(client,group)) = false . eq issleave(sdisconnectmsg(client,group,view)) = false . op issselfleave : SMessage ~> Bool . eq issselfleave(sdatamsg(client,group,sdata,view)) = false . eq issselfleave(sfreqmsg(client,group)) = false . eq issselfleave(sfreqmsg(client,group,flushtype)) = false . eq issselfleave(sjoinmsg(client,group,view)) = false . eq issselfleave(sleavemsg(client,group,view)) = false . eq issselfleave(stransmsg(group)) = false . eq issselfleave(sconfmsg(group,view,transset)) = false . eq issselfleave(sselfleavemsg(client,group)) = true . eq issselfleave(sdisconnectmsg(client,group,view)) = false . op isstrans : SMessage ~> Bool . eq isstrans(sdatamsg(client,group,sdata,view)) = false . eq isstrans(sfreqmsg(client,group)) = false . eq isstrans(sfreqmsg(client,group,flushtype)) = false . eq isstrans(sjoinmsg(client,group,view)) = false . eq isstrans(sleavemsg(client,group,view)) = false . eq isstrans(stransmsg(group)) = true . eq isstrans(sconfmsg(group,view,transset)) = false . eq isstrans(sselfleavemsg(client,group)) = false . eq isstrans(sdisconnectmsg(client,group,view)) = false . op issconf : SMessage ~> Bool . eq issconf(sdatamsg(client,group,sdata,view)) = false . eq issconf(sfreqmsg(client,group)) = false . eq issconf(sfreqmsg(client,group,flushtype)) = false . eq issconf(sjoinmsg(client,group,view)) = false . eq issconf(sleavemsg(client,group,view)) = false . eq issconf(stransmsg(group)) = false . eq issconf(sconfmsg(group,view,transset)) = true . eq issconf(sselfleavemsg(client,group)) = false . eq issconf(sdisconnectmsg(client,group,view)) = false . op issdisconnect : SMessage ~> Bool . eq issdisconnect(sdatamsg(client,group,sdata,view)) = false . eq issdisconnect(sfreqmsg(client,group)) = false . eq issdisconnect(sfreqmsg(client,group,flushtype)) = false . eq issdisconnect(sjoinmsg(client,group,view)) = false . eq issdisconnect(sleavemsg(client,group,view)) = false . eq issdisconnect(stransmsg(group)) = false . eq issdisconnect(sconfmsg(group,view,transset)) = false . eq issdisconnect(sselfleavemsg(client,group)) = false . eq issdisconnect(sdisconnectmsg(client,group,view)) = true . op view : SMessage ~> View . eq view(sdatamsg(client,group,sdata,view)) = view . op group : SMessage ~> Group . eq group(sdatamsg(client,group,sdata,view)) = group . eq group(sfreqmsg(client,group)) = group . eq group(sfreqmsg(client,group,flushtype)) = group . eq group(sjoinmsg(client,group,view)) = group . eq group(sleavemsg(client,group,view)) = group . eq group(stransmsg(group)) = group . eq group(sconfmsg(group,view,transset)) = group . eq group(sselfleavemsg(client,group)) = group . eq group(sdisconnectmsg(client,group,view)) = group . op flushtype : SMessage ~> FlushType . eq flushtype(sfreqmsg(client,group,flushtype)) = flushtype . op update-transset : SMessage AgentSet ~> SMessage . eq update-transset(sdatamsg(client,group,sdata,view),transset') = sdatamsg(client,group,sdata,view) . eq update-transset(stokenmsg(token),transset') = stokenmsg(token) . eq update-transset(sfreqmsg(client,group),transset') = sfreqmsg(client,group) . eq update-transset(sfreqmsg(client,group,flushtype),transset') = sfreqmsg(client,group,flushtype) . eq update-transset(sjoinmsg(client,group,view),transset') = sjoinmsg(client,group,view) . eq update-transset(sleavemsg(client,group,view),transset') = sleavemsg(client,group,view) . eq update-transset(stransmsg(group),transset') = stransmsg(group) . eq update-transset(sconfmsg(group,view,transset),transset') = sconfmsg(group,view,transset') . eq update-transset(sselfleavemsg(client,group),transset') = sselfleavemsg(client,group) . eq update-transset(sdisconnectmsg(client,group,view),transset') = sdisconnectmsg(client,group,view) . ---- two kinds of internal messages op isidata : SMessage ~> Bool . eq isidata(sdatamsg(keyid,key,sdata)) = true . eq isidata(stokenmsg(token)) = false . eq isidata(stokenmsg(token,keyid)) = false . op isitoken : SMessage ~> Bool . eq isitoken(sdatamsg(keyid,key,sdata)) = false . eq isitoken(stokenmsg(token)) = true . eq isitoken(stokenmsg(token,keyid)) = true . op keyid : SMessage ~> KeyId . eq keyid(sdatamsg(keyid,key,sdata)) = keyid . eq keyid(stokenmsg(token,keyid)) = keyid . op token : SMessage ~> Token . eq token(stokenmsg(token)) = token . eq token(stokenmsg(token,keyid)) = token . op data : SMessage ~> SData . eq data(sdatamsg(client,group,sdata,view)) = sdata . ----------------------- sort SMessageList . op eSMessageList : -> SMessageList . op sSMessageList : SMessage -> SMessageList . op __ : SMessageList SMessageList -> SMessageList [assoc id: eSMessageList] . var smessagelist smessagelist' : SMessageList . sort SMessageSet . op sSMessageSet : SMessage -> SMessageSet . op eSMessageSet : -> SMessageSet . op __ : SMessageSet SMessageSet -> SMessageSet [assoc comm id: eSMessageSet] . var smessageset smessageset' : SMessageSet . op contains : SMessageSet SMessage -> Bool . eq contains(eSMessageSet, smessage') = false . eq contains((sSMessageSet(smessage) smessageset), smessage') = (smessage' == smessage) or contains(smessageset, smessage') . op add : SMessageSet SMessage -> SMessageSet . eq add(smessageset,smessage) = (smessageset sSMessageSet(smessage)) . op add' : SMessageSet SMessage -> SMessageSet . ceq add'(smessageset,smessage) = smessageset if contains(smessageset, smessage) . ceq add'(smessageset,smessage) = (smessageset sSMessageSet(smessage)) if not(contains(smessageset, smessage)) . op rm : SMessageSet SMessage -> SMessageSet . eq rm(eSMessageSet,smessage) = eSMessageSet . ceq rm((sSMessageSet(smessage) smessageset),smessage') = rm(smessageset,smessage') if (smessage' == smessage) . ceq rm((sSMessageSet(smessage) smessageset),smessage') = (sSMessageSet(smessage) rm(smessageset,smessage')) if (smessage' =/= smessage) . op rm : SMessageSet SMessageSet -> SMessageSet . eq rm(smessageset, eSMessageSet) = smessageset . eq rm(smessageset, sSMessageSet(smessage) smessageset') = rm(rm(smessageset,smessage),smessageset') . endfm