*** load ap.m
*** Authenication proxies
**** abstract authentication proxy

fmod AP-IFACE is
  inc STM-IFACE .
  inc JVM-IFACE . 
  op authenticateReq : String Cred -> MsgBody .
  op authenticateReply : Data -> MsgBody .
  op authenticateReply : Oid -> MsgBody .
endfm

fmod AP-CLASS is
  inc AP-IFACE .
  inc CSSP-CLASS .
  op stms : Oid -> Attribute .
endfm

*** ServersideAuthenticationProxy Class
fmod SAP-IFACE is
  inc AP-IFACE .
endfm

fmod SAP-CLASS is
  inc AP-CLASS .
  inc SSSP-CLASS .
  op SAP : -> Cid .  *** svc and perms attributes from SSSP-CLASS
endfm

mod SAP is
  inc SAP-CLASS .
  inc PROXY-DESCRIPTION .

 rl[sap.authreq]:
  < O:Oid : SAP | stms(M:Oid), svc(S:Oid), sname(sn:String), idle >
  smsg(O:Oid, C:Oid, authenticateReq(sn:String, ccred:Cred))
  => 
  < O:Oid : SAP | stms(M:Oid), svc(S:Oid), sname(sn:String),
                  waitfor(M:Oid,C:Oid,authenticateReq(sn:String, ccred:Cred)) >
  msg(M:Oid, O:Oid, checkClientReq(sn:String,ccred:Cred))
 .

 rl[sap.permsreply]:
  < O:Oid : SAP | stms(M:Oid), svc(S:Oid), sname(sn:String),
                  waitfor(M:Oid,C:Oid,authenticateReq(sn:String, ccred:Cred)) >
  msg(O:Oid, M:Oid, checkClientReply(pm:Permissions))
                *** clientPerm(sn:String,ccred:Cred,p:Policy)
  =>
  < O:Oid : SAP | stms(M:Oid), svc(S:Oid), sname(sn:String),
                  perms(pm:Permissions),
                  waitfor(myJVM,C:Oid,authenticateReq(sn:String, ccred:Cred)) >
   msg(myJVM, O:Oid, newIdReq)
 .

 rl[sap.newidreply]:
  < O:Oid : SAP | stms(M:Oid), svc(S:Oid), sname(sn:String),
                  perms(pm:Permissions),
                  waitfor(myJVM,C:Oid,authenticateReq(sn:String, ccred:Cred)) >
   msg(O:Oid, myJVM, newIdReply(N:Oid))
  =>
  < O:Oid : SAP | stms(M:Oid), svc(S:Oid),  sname(sn:String), 
                  perms(pm:Permissions),
                  waitfor(M:Oid,C:Oid,authenticateReq(sn:String, ccred:Cred)) >
  < N:Oid : SSSP | svc(S:Oid), sname(sn:String), perms(pm:Permissions), idle > 
   msg(M:Oid, O:Oid, encryptReq(proxyD(CSSP, svc(N:Oid)), ccred:Cred))
 .

 rl[sap.authreply]:
  < O:Oid : SAP | stms(M:Oid), svc(S:Oid), sname(sn:String), 
                  perms(pm:Permissions),
                  waitfor(M:Oid,C:Oid,authenticateReq(sn:String, ccred:Cred)) >
   msg(O:Oid, M:Oid, encryptReply(encrPxD:Data))
  =>
  < O:Oid : SAP | stms(M:Oid), svc(S:Oid), sname(sn:String), idle >
  smsg(C:Oid, O:Oid, authenticateReply(encrPxD:Data))
 .
endm


**** client side authentication proxy
fmod CAP-IFACE is
  inc AP-IFACE .
endfm

fmod CAP-CLASS is
  inc AP-CLASS .
  inc CAP-IFACE .
  op CAP : -> Cid .
  op pxd : Data -> Attribute .
endfm

mod CAP is
  inc CAP-CLASS .
  inc PROXY-DESCRIPTION .

 rl[cap.authreq]:
  < O:Oid : CAP | stms(M:Oid), svc(S:Oid), idle >
  msg(O:Oid, C:Oid, authenticateReq(sn:String, ccred:Cred))
  => 
  < O:Oid : CAP | stms(M:Oid), svc(S:Oid),
               waitfor(S:Oid, C:Oid,authenticateReq(sn:String, ccred:Cred)) >
  smsg(S:Oid, O:Oid, authenticateReq(sn:String,ccred:Cred))
 .

 rl[cap.authrepl]: 
  < O:Oid : CAP | stms(M:Oid), svc(S:Oid), 
               waitfor(S:Oid, C:Oid,authenticateReq(sn:String, ccred:Cred)) >
  smsg(O:Oid, S:Oid, authenticateReply(encrPD:Data))
  => 
  < O:Oid : CAP | stms(M:Oid), svc(S:Oid),
               waitfor(M:Oid, C:Oid,authenticateReq(sn:String, ccred:Cred)) >
  msg(M:Oid, O:Oid, decryptReq(encrPD:Data))
 .

 rl[cap.decryptreply]:
  < O:Oid : CAP | stms(M:Oid), svc(S:Oid),
               waitfor(M:Oid, C:Oid,authenticateReq(sn:String, ccred:Cred)) >
  msg(O:Oid, M:Oid, decryptReply(proxyD(CSSP, svc(SP:Oid))))
  =>
  < O:Oid : CAP | stms(M:Oid), svc(S:Oid), pxd(proxyD(CSSP, svc(SP:Oid))),
               waitfor(myJVM, C:Oid,authenticateReq(sn:String, ccred:Cred)) >
  msg(myJVM, O:Oid, newIdReq)
 .

 rl[cap.newidreply]:
  < O:Oid : CAP | stms(M:Oid), svc(S:Oid), pxd(proxyD(CSSP, svc(SP:Oid))),
                 waitfor(myJVM,C:Oid,authenticateReq(sn:String, ccred:Cred)) >
  msg(O:Oid, myJVM, newIdReply(N:Oid))
  =>
  < N:Oid : CSSP | svc(SP:Oid), idle >
  < O:Oid : CAP | stms(M:Oid), svc(S:Oid), idle >
  msg(C:Oid, O:Oid, authenticateReply(N:Oid)) 
 .

endm
