***load ssp3.m
*** SecureSesssion proxies
******Generic Service

**** client and server secure session proxies
fmod SSSP-IFACE is
  inc SVC-IFACE .
  inc SP-IFACE .
  inc STM-IFACE .
endfm

fmod SSSP-CLASS is
  inc SSSP-IFACE .
  inc SP-CLASS .
  op SSSP : -> Cid .
  op perms : Permissions -> Attribute .
***  op svc : Oid -> Attribute .

endfm

mod SSSP is
  inc SSSP-CLASS .
  op checkPerms : Data Permissions -> Bool .

rl[sssp.svcreq]:
  < O:Oid : SSSP | svc(S:Oid), sname(sn:String), perms(p:Permissions),idle >
  smsg(O:Oid, C:Oid,  svcReq(d:Data))
  =>
  (if (checkPerms(d:Data, p:Permissions))
   then
    ( < O:Oid : SSSP | svc(S:Oid), sname(sn:String), perms(p:Permissions),
                      waitfor(S:Oid, C:Oid, svcReq(d:Data)) >
      msg(S:Oid, O:Oid, svcReq(d:Data, getId(p:Permissions))) )
   else
  ( < O:Oid : SSSP | svc(S:Oid), sname(sn:String), perms(p:Permissions), idle >
      smsg(C:Oid, O:Oid, svcReply(badData)) )
   fi)
  .

rl[sssp.reply]:
  < O:Oid : SSSP | svc(S:Oid), sname(sn:String), perms(p:Permissions),
                   waitfor(S:Oid, C:Oid, svcReq(dreq:Data)) >
  msg(O:Oid, S:Oid, svcReply(dreply:Data))
  =>
  < O:Oid : SSSP | svc(S:Oid), sname(sn:String), perms(p:Permissions), idle > 
  smsg(C:Oid, O:Oid, svcReply(dreply:Data))
 .
endm

fmod CSSP-IFACE is
  inc SP-IFACE .
  inc SVC-IFACE .
endfm

fmod CSSP-CLASS is
  inc CSSP-IFACE .
  inc SP-CLASS .
  op CSSP : -> Cid .
***  op svc : Oid -> Attribute .
endfm

mod CSSP is
  inc CSSP-CLASS .

  rl[cssp.svcreq]:
  < O:Oid : CSSP | svc(S:Oid), idle >
  msg(O:Oid, A:Oid, svcReq(d:Data))
  =>
  < O:Oid : CSSP | svc(S:Oid), waitfor(S:Oid, A:Oid, svcReq(d:Data)) >
  smsg(S:Oid, O:Oid, svcReq(d:Data))
 .
  rl[cssp.svcreply]:
  < O:Oid : CSSP | svc(S:Oid), waitfor(S:Oid, A:Oid, svcReq(dreq:Data)) >
  smsg(O:Oid, S:Oid, svcReply(dreply:DataX))
  =>
  < O:Oid : CSSP | svc(S:Oid), idle > 
  msg(A:Oid, O:Oid, svcReply(dreply:DataX))
 .
endm
