***load sptk1.m  *** SPTKs 
*** secure proxy toolkit 
*** server side registers services:
*** creates and installs serverside secure proxy
*** creates clientside secure proxy descr that knows the clientside proxy
*** and registers it



fmod SSPTK1-CLASS is
  inc SSPTK-IFACE .
  inc SPTK-CLASS .
  inc CSP1-CLASS .  *** must create description of CSP1
  inc SSP1-CLASS .  *** must create an instance of SSP1
  op SSPTK1 : -> Cid .
endfm

mod SSPTK1 is
  inc SSPTK1-CLASS .

  rl[ssptk.regreq]:
  < O:Oid : SSPTK1 | lookup(L:Oid), idle >
  msg(O:Oid, S:Oid, spRegisterReq(sn:String, sid:Oid))
   => 
  < O:Oid : SSPTK1 | lookup(L:Oid),
                     waitfor(myJVM, S:Oid, spRegisterReq(sn:String, sid:Oid)) >
  msg(myJVM, O:Oid, newIdReq)
.

 rl[ssptk.sapId]:
  < O:Oid : SSPTK1 | lookup(L:Oid),
                     waitfor(myJVM, S:Oid, spRegisterReq(sn:String, sid:Oid)) >
  msg(O:Oid, myJVM, newIdReply(N:Oid))
  => 
  < O:Oid : SSPTK1 | lookup(L:Oid),
                     waitfor(L:Oid, S:Oid, spRegisterReq(sn:String, sid:Oid)) >
  < N:Oid : SSP1 | svc(sid:Oid), sname(sn:String),  idle >
  msg(L:Oid, O:Oid, registerReq(sn:String, proxyD(CSP1, svc(N:Oid))))
 .

 rl[ssptk.regreply]:
  < O:Oid : SSPTK1 | lookup(L:Oid),
                     waitfor(L:Oid, S:Oid, spRegisterReq(sn:String, sid:Oid)) >
  msg(O:Oid, L:Oid, r:MsgBody)
  =>
  < O:Oid : SSPTK1 | lookup(L:Oid),  idle >
  msg(S:Oid, O:Oid, r:MsgBody) .
endm


