*** level independent

load ../ALL/all-lookup.m

*** level specific
load ../L1/sp1.m     *** SSP2 == SSP1 CSP2 == CSP1
load sptk2.m         *** CSPTK2  SSPTK2
***(
)

mod TEST2-LOOKUP is
  inc TEST-LOOKUP .
  inc STM .
  inc CSP1 .
  inc SSP1 .
  inc CSPTK2 .
  inc SSPTK2 .
  
*** 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 .



  eq sptkobs =
     ( < (JS . sstm) : STM | pkey(sPk), skey(sSk), policy(sP) >
       < (JS . ssptk) : SSPTK2 | stms(JS . sstm), lookup(JL . lup),idle > )
  .

  eq cptkobs =
     ( < (JC . cstm) : STM | pkey(cPk), skey(cSk), policy(cP) >
       < (JC . csptk) : CSPTK2 | stms(JC . cstm), lookup(JL . lup), 
                                 checksn(true), 
***                                 checksn(false), 
                                 clientId("sam"), ts(sPk),
                                 idle > )
  .
  
  eq acptkobs = 
    ( < (JL . cstm) : STM | pkey(aPk), skey(aSk), policy(aP) >
      < (JL . ssptk) : SSPTK2 | stms(JL . cstm), lookup(JL . lup), idle > 
      < (JL . csptk) : CSPTK2 | stms(JL . cstm), lookup(JL . lup), 
                                 checksn(false), 
                                 clientId(fakeId), ts(sPk),
                                 idle > 
       msg(JL . ssptk, JL . fred, spRegisterReq("Attack", JL . AttackSvc))
     ) 
  .

endm

*** note need to vary checksn
***(
rew  eecf aljcf sjcf cjcf .

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

)




