sptk1.m          *** serverside ptk for level1  (clientside is same as level0)
SSPTK1-CLASS inc SSPTK-IFACE SPTK-CLASS
                 CSP1-CLASS SSP1-CLASS .  *** create instances
  op SSPTK1 : -> Cid .
SSPTK1  inc SSPTK1-CLASS .

************************************************************
sp1.m           *** client- and server-side level1 proxies
                *** differs from level0 in using smsg for remote messaging

SSP1-CLASS inc SP-CLASS .
  op SSP1  : -> Cid .
SSP1  inc SSP1-CLASS .

CSP1-CLASS inc SP-CLASS .
  op CSP1 : -> Cid .
CSP1 inc CSP1-CLASS .

************************************************************
*** level 1 test configurations -- defines sptkobs cptkopbs aptkobs

test1-ether.txt      *** ether attack model
TEST1-ETHER  inc TEST-ETHER CSPTK0 SSPTK1 CSP1 SSP1 .

test1-lookup.txt      *** lookup attack model
TEST1-LOOKUP inc TEST-LOOKUP CSPTK0 SSPTK1 CSP1 SSP1 .

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

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