***load sp.m
*** Secure Proxy Toolkit  SPTKs level 3
*** server side registers services:
***   creates and signs clientside authentication proxy descr
***   registers it,  and creates and installs serverside authentication proxy 


fmod SPTK3-CLASS is
  inc SPTK-CLASS .
  inc STM-IFACE .
  inc CAP-CLASS . *** must create instance and description of CAP
  op svcName : String -> Attribute .  *** used to pass name for checking
endfm


fmod SSPTK3-CLASS is
  inc SSPTK-IFACE .
  inc SPTK3-CLASS .
  inc SAP-CLASS . *** must create an instance of SAP 
  op SSPTK3 : -> Cid .
endfm

mod SSPTK3 is
  inc SSPTK3-CLASS .

  rl[ssptk.regreq]:
  < O:Oid : SSPTK3 | stms(M:Oid), lookup(L:Oid), idle >
  msg(O:Oid, S:Oid, spRegisterReq(sn:String, sid:Oid))
  => 
  < O:Oid : SSPTK3 | 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 : SSPTK3 | stms(M:Oid),  lookup(L:Oid),
                    waitfor(myJVM, S:Oid, spRegisterReq(sn:String, sid:Oid)) >
  msg(O:Oid, myJVM, newIdReply(N:Oid))
  => 
  < O:Oid : SSPTK3 | stms(M:Oid),  lookup(L:Oid),
                    waitfor(M:Oid, S:Oid, spRegisterReq(sn:String, sid:Oid)) >
  < N:Oid : SAP | svc(sid:Oid), stms(M:Oid), sname(sn:String), idle >
  msg(M:Oid, O:Oid, signReq(proxyD(CAP, (sname(sn:String), svc(N:Oid)))))
  .

  rl[ssptk.signreply]:
  < O:Oid : SSPTK3 | 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 : SSPTK3 | 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 : SSPTK3 | 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 : SSPTK3 | stms(M:Oid),  lookup(L:Oid),  idle >
  msg(S:Oid, O:Oid, r:MsgBody)
  .

endm


fmod CSPTK3-CLASS is
  inc CSPTK-IFACE .
  inc SPTK3-CLASS .
  op cred : Cred -> Attribute .
  op ts : Key -> Attribute .
  op CSPTK3 : -> Cid .
endfm


mod CSPTK3 is
  inc CSPTK3-CLASS .

  rl[csptk.findServiceReq]:
  < O:Oid : CSPTK3 | stms(M:Oid), lookup(L:Oid), cred(c:Cred), ts(sk:Key),
                    idle >
  msg(O:Oid, A:Oid, findServiceReq(sn:String)) 
  =>
  < O:Oid : CSPTK3 | stms(M:Oid), lookup(L:Oid), cred(c:Cred),  ts(sk:Key),  
                    waitfor(L:Oid, A:Oid, findServiceReq(sn:String)) >
  msg(L:Oid, O:Oid, lookupReq(sn:String)) 
  .

  rl[csptk.lookupFail]:
  < O:Oid : CSPTK3 | stms(M:Oid), lookup(L:Oid), cred(c:Cred), ts(sk:Key),  
                    waitfor(L:Oid, A:Oid, findServiceReq(sn:String)) >
  msg(O:Oid, L:Oid, lookupFail(sn:String) )
  =>
  < O:Oid : CSPTK3 | stms(M:Oid), lookup(L:Oid), cred(c:Cred), ts(sk:Key),
                    idle >
  msg(A:Oid, O:Oid, findServiceFailed(sn:String) )
  .

  rl[csptk.lookupOk]:  *** check name, verify sig, 
  < O:Oid : CSPTK3 | stms(M:Oid), lookup(L:Oid), cred(c:Cred), ts(sk:Key), 
                    waitfor(L:Oid, A:Oid, findServiceReq(sn:String)) >
  msg(O:Oid, L:Oid, lookupOk(sn:String, signedPD:Data))
  =>
  < O:Oid : CSPTK3 | stms(M:Oid), lookup(L:Oid), cred(c:Cred), 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 : CSPTK3 | stms(M:Oid), lookup(L:Oid), cred(c:Cred), ts(sk:Key),  
                    waitfor(M:Oid, A:Oid, findServiceReq(sn:String)) >
  msg(O:Oid, M:Oid, verifySigOk(pd:Data))
  =>
  < O:Oid : CSPTK3 | stms(M:Oid), lookup(L:Oid), cred(c:Cred), ts(sk:Key),  
                    pxd(pd:Data),
                    waitfor(myJVM,A:Oid, findServiceReq(sn:String)) >
  msg(myJVM, O:Oid, newIdReq)
  .

  rl[csptk.verifyFail]:
  < O:Oid : CSPTK3 | stms(M:Oid), lookup(L:Oid), cred(c:Cred), ts(sk:Key),  
                    waitfor(M:Oid, A:Oid, findServiceReq(sn:String)) >
  msg(O:Oid, M:Oid, verifySigFail)
  =>
  < O:Oid : CSPTK3 | stms(M:Oid), lookup(L:Oid), cred(c:Cred), ts(sk:Key),
                    idle > 
  msg(A:Oid, O:Oid, findServiceFailed(sn:String) )
  .

  rl[csptk.newidreply]:
  < O:Oid : CSPTK3 | stms(M:Oid), lookup(L:Oid), cred(c:Cred), ts(sk:Key),  
                    pxd(proxyD(cl:Cid, 
                       (sname(mysn:String), atts:AttributeSet))), 
                    waitfor(myJVM, A:Oid, findServiceReq(sn:String)) >
  msg(O:Oid, myJVM, newIdReply(N:Oid))
  =>
  (if (mysn:String == sn:String)
  then
    < O:Oid : CSPTK3 | stms(M:Oid), lookup(L:Oid), cred(c:Cred), ts(sk:Key), 
                    waitfor(N:Oid, A:Oid, findServiceReq(sn:String)) >
    < N:Oid : cl:Cid | atts:AttributeSet, stms(M:Oid), idle >
    msg(N:Oid, O:Oid, authenticateReq(sn:String, c:Cred) )
  else
    < O:Oid : CSPTK3 | stms(M:Oid), lookup(L:Oid), cred(c:Cred), ts(sk:Key),
                      idle >
    msg(A:Oid, O:Oid, findServiceFailed(sn:String))
  fi) 
  .

  rl[csptk.authreply]:
  < O:Oid : CSPTK3 | stms(M:Oid), lookup(L:Oid), cred(c:Cred), ts(sk:Key), 
                    waitfor(N:Oid, A:Oid, findServiceReq(sn:String)) >
  msg(O:Oid, N:Oid, authenticateReply(S:Oid)) 
  =>
  < O:Oid : CSPTK3 | stms(M:Oid), lookup(L:Oid), cred(c:Cred), ts(sk:Key),
                    idle >
  msg(A:Oid, O:Oid, findServiceOk(sn:String, S:Oid)) 
  .

endm
