*** SPTKs
***load sptk2.m
*** secure signed proxy toolkit 
*** server side registers services:
*** creates and installs serverside secure proxy 
*** creates and signs clientside secure proxy descr (that knows the serverside)
*** and registers it  uses the level 1 proxies



fmod SPTK2-CLASS is
  inc SPTK-CLASS .
  inc STM-IFACE .
  inc CSP1-CLASS .  *** for creating description and installing
  op stms : Oid -> Attribute .
endfm

fmod SSPTK2-CLASS is
  inc SSPTK-IFACE .
  inc SPTK2-CLASS .
  inc SSP1-CLASS .  *** must create an instance of SSP1 
  op SSPTK2 : -> Cid .
endfm

mod SSPTK2 is
  inc SSPTK2-CLASS .

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

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

 rl[ssptk.signreply]:
  < O:Oid : SSPTK2 | stms(M:Oid),  lookup(L:Oid),
                    waitfor(M:Oid, S:Oid, spRegisterReq(sn:String, sid:Oid)) >
  msg(O:Oid, M:Oid, signReply(signedPD:Data))
  =>
  < O:Oid : SSPTK2 | stms(M:Oid),  lookup(L:Oid), 
                    waitfor(L:Oid, S:Oid, spRegisterReq(sn:String, sid:Oid)) >
  msg(L:Oid, O:Oid, registerReq(sn:String,signedPD:Data))
 .

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


fmod CSPTK2-CLASS is
  inc CSPTK-IFACE .
  inc SPTK2-CLASS .

  op checksn : Bool -> Attribute .      *** checking attribute?
  op ts : Key -> Attribute .
  op CSPTK2 : -> Cid .
endfm


mod CSPTK2 is
  inc CSPTK2-CLASS .

 rl[csptk.findServiceReq]:
  < O:Oid : CSPTK2 | stms(M:Oid), lookup(L:Oid),
                     clientId(cn:String), checksn(b:Bool), ts(sk:Key),
                     idle >
  msg(O:Oid, A:Oid, findServiceReq(sn:String)) 
  =>
  < O:Oid : CSPTK2 | stms(M:Oid), lookup(L:Oid),   
                     clientId(cn:String), checksn(b:Bool), ts(sk:Key),
                waitfor(L:Oid, A:Oid, findServiceReq(sn:String)) >
  msg(L:Oid, O:Oid, lookupReq(sn:String)) 
 .

 rl[csptk.lookupFail]:
  < O:Oid : CSPTK2 | stms(M:Oid), lookup(L:Oid),   
                     clientId(cn:String), checksn(b:Bool), ts(sk:Key),
                waitfor(L:Oid, A:Oid, findServiceReq(sn:String)) >
  msg(O:Oid, L:Oid, lookupFail(sn:String) )
  =>
  < O:Oid : CSPTK2 | stms(M:Oid), lookup(L:Oid),
                     clientId(cn:String), checksn(b:Bool), ts(sk:Key),
                     idle >
  msg(A:Oid, O:Oid, findServiceFailed(sn:String) )
 .

 rl[csptk.lookupOk]:  *** check name, verify sig, 
  < O:Oid : CSPTK2 | stms(M:Oid), lookup(L:Oid),   
                     clientId(cn:String), checksn(b:Bool), ts(sk:Key),
                waitfor(L:Oid, A:Oid, findServiceReq(sn:String)) >
  msg(O:Oid, L:Oid, lookupOk(sn:String, signedPD:Data))
  =>
  < O:Oid : CSPTK2 | stms(M:Oid), lookup(L:Oid),  
                     clientId(cn:String), checksn(b:Bool), ts(sk:Key),
                 waitfor(M:Oid, A:Oid, findServiceReq(sn:String)) >
  msg(M:Oid, O:Oid, verifySigReq(signedPD:Data,sk:Key) )
 .

 rl[csptk.verifyOk]:
  < O:Oid : CSPTK2 | stms(M:Oid), lookup(L:Oid),   
                     clientId(cn:String), checksn(b:Bool), ts(sk:Key),
                 waitfor(M:Oid, A:Oid, findServiceReq(sn:String)) >
    msg(O:Oid, M:Oid, verifySigOk(pd:Data))
  =>
  < O:Oid : CSPTK2 | stms(M:Oid), lookup(L:Oid),   
                     pxd(pd:Data),
                     clientId(cn:String), checksn(b:Bool), ts(sk:Key),
                   waitfor(myJVM,A:Oid, findServiceReq(sn:String)) >
    msg(myJVM, O:Oid, newIdReq)
 .

 rl[csptk.verifyFail]:
   < O:Oid : CSPTK2 | stms(M:Oid), lookup(L:Oid),   
                      clientId(cn:String), checksn(b:Bool), ts(sk:Key),
                waitfor(M:Oid, A:Oid, findServiceReq(sn:String)) >
    msg(O:Oid, M:Oid, verifySigFail)
  =>
  < O:Oid : CSPTK2 | stms(M:Oid), lookup(L:Oid),
                     clientId(cn:String), checksn(b:Bool), ts(sk:Key),
                     idle > 
    msg(A:Oid, O:Oid, findServiceFailed(sn:String) )
 .

 rl[csptk.newidreply]:
    < O:Oid : CSPTK2 | stms(M:Oid), lookup(L:Oid),   
                pxd(proxyD(cl:Cid, (sname(mysn:String), atts:AttributeSet))),
                  clientId(cn:String), checksn(b:Bool), ts(sk:Key),
                  waitfor(myJVM, A:Oid, findServiceReq(sn:String)) >
    msg(O:Oid, myJVM, newIdReply(N:Oid))
  =>
    < O:Oid : CSPTK2 | stms(M:Oid), lookup(L:Oid),  
                       clientId(cn:String), checksn(b:Bool), ts(sk:Key),
                       idle >
    (if ((sn:String == mysn:String) or not(b:Bool))
     then
       < N:Oid : cl:Cid | sname(mysn:String), clientId(cn:String),
                          atts:AttributeSet,  idle >
       msg(A:Oid, O:Oid, findServiceOk(sn:String, N:Oid)) 
     else
       msg(A:Oid, O:Oid, findServiceFailed(sn:String))
    fi )
 .

endm
