*** SPTK with levels of protections and attack
*** Level 2 client proxy (code and data) are signed

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

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

mod TEST2-ETHER is
  inc TEST-ETHER .
  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), clientId("sam"), ts(sPk),
***                                 checksn(false), clientId("sam"), ts(sPk),
                                 idle > )
  .


  eq aptkobs = 
     < (JA . cstm) : STM | pkey(aPk), skey(aSk), policy(aP) >
     < (JA .  csptk) : CSPTK2 | stms(JA . cstm), lookup(JL . lup),
                                clientId(fakeId), checksn(false), ts(sPk), 
                                idle > .



endm

***(

 rew eecf sjcf ljcf cjcf  .
 rew eacf sjcf ljcf cjcf  .

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



