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

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

mod TEST3-LOOKUP is
  inc TEST-LOOKUP .
  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 aCred : -> Cred .
  eq getKey(myCred) = cPk .
  eq getKey(aCred) = 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("GBPquote",  aCred, sP)) = false .
  eq getId(clientPerm("GBPquote", aCred, sP))  = fakeId .
  eq getId(clientPerm("USquote", aCred, 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 acptkobs = 
    ( < (JL . cstm) : STM | pkey(aPk), skey(aSk), policy(aP) >
      < (JL . ssptk) : SSPTK3 | stms(JL . cstm), lookup(JL . lup), idle > 
      < (JL . csptk) : CSPTK3 | stms(JL . cstm), lookup(JL . lup), 
                                cred(aCred), ts(sPk),
                                 idle >
      msg(JL . ssptk, JL . fred, spRegisterReq("Attack", JL . AttackSvc))
    ) 
  .


endm

*** set print format on .
***(
rew  eecf aljcf sjcf cjcf .

rew  eecf aljcf sjcf .
rew  eecf aljcf sjcf cjcf1 .
rew  eecf aljcf sjcf cjcf2 .
rew  eecf aljcf0 sjcf cjcf1 .

)







