sptk3.m    *** client server ptks for level3 
SPTK3-CLASS inc SPTK-CLASS STM-IFACE CAP-CLASS .  *** shared by client-server
  op svcName : String -> Attribute .  *** used to pass name for checking

SSPTK3-CLASS inc SSPTK-IFACE SPTK3-CLASS SAP-CLASS .
  op SSPTK3 : -> Cid .
SSPTK3 inc SSPTK3-CLASS .

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

************************************************************
ap3.m                         *** authentiation proxies
AP-IFACE inc STM-IFACE JVM-IFACE               *** shared server and client
  op authenticateReq : String Cred -> MsgBody .
  op authenticateReply : Data -> MsgBody .
  op authenticateReply : Oid -> MsgBody .
endfm

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

SAP-IFACE inc AP-IFACE .   *** ServersideAuthenticationProxy Class

SAP-CLASS inc AP-CLASS SSSP-CLASS .
  op SAP : -> Cid .  
SAP inc SAP-CLASS PROXY-DESCRIPTION .

************************************************************
ssp3.m   **** client and server secure session proxies
SSSP-IFACE inc SVC-IFACE SP-IFACE STM-IFACE .
SSSP-CLASS inc SSSP-IFACE SP-CLASS .
  op perms : Permissions -> Attribute .
  op SSSP : -> Cid .
SSSP inc SSSP-CLASS .

CSSP-IFACE inc SP-IFACE SVC-IFACE .
CSSP-CLASS inc CSSP-IFACE inc SP-CLASS .
  op CSSP : -> Cid .
CSSP inc CSSP-CLASS .

************************************************************
*** level 3 test configurations 
***       defines sptkobs cptkopbs aptkobs
***       defines STM key and permissions functions on test data

test3-ether.txt      *** ether attack model
TEST3-ETHER  inc TEST-ETHER  STM CSSP SSSP CAP SAP CSPTK3 SSPTK3 .

test3-lookup.txt      *** lookup attack model
TEST3-LOOKUP inc TEST-LOOKUP  STM CSSP SSSP CAP SAP CSPTK3 SSPTK3 .

************************************************************
*** samples of rewriting test configurations
runs3-ether.txt
runs3-lookup.txt

************************************************************
*** search results for the test-suite search patterns (in ALL/test-<attack>.m)
search3-ether.txt
search3-lookup.txt