*** level independent
load ../ALL/all-ether.m

*** level specific
load ssp3.m            *** SSSP  CSSP
load ap3.m             *** SAP   CAP
load sptk3.m           *** SSPTK CSPTK  


mod TEST3-ETHER is
  inc TEST-ETHER .
  inc STM .
  inc CSSP .
  inc SSSP .
  inc CAP .
  inc SAP .
  inc CSPTK3 .
  inc SSPTK3 .
  
*** STM setup
  ops cPk sPk aPk : -> Key  .
  ops cSk sSk aSk : -> Key .
  ops cP sP aP    : -> Policy .

  eq keyInv(sSk) = sPk .
  eq keyInv(sPk) = sSk .
  eq keyInv(cSk) = cPk .
  eq keyInv(cPk) = cSk .
  eq keyInv(aSk) = aPk .
  eq keyInv(aPk) = aSk .

  ops myCred fakeCred : -> Cred .
  eq getKey(myCred) = cPk .
  eq getKey(fakeCred) = aPk .
  eq checkPerms(mycall, clientPerm("USquote",  myCred, sP)) = true .
  eq checkPerms(mycall, clientPerm("GBPquote",  myCred, sP)) = true .
  eq checkPerms(badcall, clientPerm("USquote",  myCred, sP)) = false .
  eq checkPerms(badcall, clientPerm("GBPquote",  myCred, sP)) = false .
  eq getId(clientPerm("GBPquote", myCred, sP))  = "sam" .
  eq getId(clientPerm("USquote", myCred, sP))  = "sam" .

  eq checkPerms(fakeCall, clientPerm("USquote",  fakeCred, sP)) = false .
  eq checkPerms(fakeCall, clientPerm("GBPquote",  fakeCred, sP)) = false .
  eq getId(clientPerm("GBPquote", fakeCred, sP))  = fakeId .
  eq getId(clientPerm("USquote",  fakeCred, sP))  = fakeId .

  eq sptkobs =
     ( < (JS . sstm) : STM | pkey(sPk), skey(sSk), policy(sP) >
       < (JS . ssptk) : SSPTK3 | stms(JS . sstm), lookup(JL . lup),idle > ) .
  
  eq cptkobs =
     ( < (JC . cstm) : STM | pkey(cPk), skey(cSk), policy(cP) >
       < (JC . csptk) : CSPTK3 | stms(JC . cstm), lookup(JL . lup), 
                                 cred(myCred), ts(sPk),
                                 idle > )  .


  eq aptkobs = 
   (  < (JA . cstm) : STM | pkey(aPk), skey(aSk), policy(aP) >
     < (JA .  csptk) : CSPTK3 | stms(JA . cstm), lookup(JL . lup),
                                cred(fakeCred), ts(sPk), 
                                idle > ) .

endm

*** set print format on .
***( 
rew eecf sjcf ljcf cjcf  .
rew eacf sjcf ljcf cjcf  .

rew eecf sjcf ljcf cjcf ajcf .
rew eacf sjcf ljcf cjcf ajcf .
)


