fmod SAPI is

--- Secure Spread layer API

protecting SMESSAGE .
including STATE .

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

op ssp-connect-req        --- client requests connection to 
                          --- secure spread server
    : Agent               --- client
   -> State .

op ssp-connect-ack        --- server acknowledges established connection
    : Agent               --- client
   -> State .

op ssp-connect-err        --- server rejects request
    : Agent               --- client
      ConnectError        --- error status
   -> State .
      
-----------------------

op ssp-disconnect-req     --- client requests to disconnect from 
                          --- secure spread server
    : Agent               --- client
   -> State .

op ssp-disconnect-ack     --- server acknowledges disconnect
    : Agent               --- client
   -> State .

op ssp-disconnect-err     --- server rejects request
    : Agent               --- client
      DisconnectError     --- error status
   -> State .

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

op ssp-join-req           --- client requests to join a group
    : Agent               --- client
      Group               --- group to join
   -> State .

op ssp-join-ack           --- server acknowledges group join
    : Agent               --- client
   -> State .

op ssp-join-err           --- server rejects request
    : Agent               --- client
      JoinError           --- error status 
   -> State .

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

op ssp-leave-req          --- client requests to leave a group
    : Agent               --- client
      Group               --- group to leave
   -> State .

op ssp-leave-ack          --- server acknowledges group leave
    : Agent               --- client
   -> State .

op ssp-leave-err          --- server rejects request
    : Agent               --- client
      LeaveError          --- error status
   -> State .

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

op ssp-multicast-req      --- client requests multicast to a group
    : Agent               --- client
      Mode                --- message type
      Group               --- destination
      SData	          --- contents
    -> State .

op ssp-multicast-ack      --- server acknowledges multicast
    : Agent               --- client
   -> State .

op ssp-multicast-err      --- server rejects multicast
    : Agent               --- client
      MulticastError      --- error status
   -> State .

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

op ssp-receive-req        --- client requests next message from server
    : Agent               --- client = intended receiver
   -> State .

op ssp-receive-ack        --- received message
    : Agent               --- client = receiver
      SMessage
   -> State .

op ssp-receive-err        --- receive failed
    : Agent               --- client = intended receiver
      ReceiveError        --- error status
   -> State . 

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

op ssp-flushok-req        --- client sends flushok
    : Agent               --- client
      Group               --- group to flush
   -> State . 

op ssp-flushok-ack        --- server acknowledges flushok
    : Agent               --- client
   -> State . 

op ssp-flushok-err        --- server rejects flushok
    : Agent               --- client
      FlushError          --- error status
   -> State .
  
----------------------------------------------------------
--- the following are omitted in the present specification
----------------------------------------------------------

op ssp-signed-multicast-req     --- client requests multicast to a group
    : Agent                     --- client
      Mode                      --- message type
      Group                     --- destination group
      Group                     --- signing group
      SData	                --- contents
    -> State .

op ssp-signed-multicast-ack     --- server acknowledges multicast
    : Agent                     --- client
   -> State .

op ssp-signed-multicast-err     --- server rejects multicast
    : Agent                     --- client
      MulticastError            --- error status
   -> State .
   
-----------------------

sort KeyError .
subsort KeyError < Error .

op ssp-getkey-req        --- client requests group key
    : Agent              --- client
      Group              --- group of which key is requested
   -> State .

op ssp-getkey-ack        --- received key 
    : Agent              --- client
      PartialKey         --- shared group key
   -> State .

op ssp-getkey-err        --- get key failed 
    : Agent              --- client
      KeyError           --- error status
   -> State .
   
endfm