03mar02

***checksn(true)
rewrite in TEST2-LOOKUP : eecf aljcf sjcf cjcf .
rewrites: 699 in 60ms cpu (56ms real) (11650 rewrites/second)
result OConf: 
< eee : Transmitter | inQ(none),outQ(none) > 
< JL : JVM | oCtr(2),
 {
< JL . AttackSvc : SVC | state(attackData) > 
< JL . cstm : STM | pkey(aPk),skey(aSk),policy(aP) > 
< JL . ssptk : SSPTK2 | idle,lookup(JL . lup),stms(JL . cstm) > 
< JL . csptk : CSPTK2 | idle,clientId(fakeId),lookup(JL . lup),stms(JL . cstm),
    checksn(false),ts(sPk) > 
< JL . app : APP | idle,svcFound(b("GBPquote", JL . o(1))),mytk(JL . csptk),
    todo(none),done(result("GBPquote", fakeCall, reply(GBPdata, fakeCall,
    fakeId))) > 
< JL . lup : AttackerLookup | svcSet(signed(proxyD(CSP1, svc(JS . o(0)),sname(
    "GBPquote")), sSk) signed(proxyD(CSP1, svc(JS . o(1)),sname("USquote")),
    sSk)),mySvcSet(signed(proxyD(CSP1, svc(JL . o(0)),sname("Attack")), aSk)),
    attackeeSet(signed(proxyD(CSP1, svc(JS . o(1)),sname("USquote")), sSk)),
    myCPTK(JL . csptk),mySPTK(JL . ssptk) > 
< JL . o(0) : SSP1 | idle,svc(JL . AttackSvc),sname("Attack") > 
< JL . o(1) : CSP1 | idle,svc(JS . o(0)),clientId(fakeId),sname("GBPquote") > 
msg(JL . fred, JL . ssptk, registerReply)},ether(eee) > 
< JS : JVM | oCtr(2),
 {
< JS . GBPsvc : SVC | state(update(GBPdata, fakeCall, fakeId)) > 
< JS . USsvc : SVC | state(USdata) > 
< JS . sstm : STM | pkey(sPk),skey(sSk),policy(sP) > 
< JS . ssptk : SSPTK2 | idle,lookup(JL . lup),stms(JS . sstm) > 
< JS . o(0) : SSP1 | idle,svc(JS . GBPsvc),sname("GBPquote") > 
< JS . o(1) : SSP1 | idle,svc(JS . USsvc),sname("USquote") > 
msg(JS . fred, JS . ssptk, registerReply) 
msg(JS . fred, JS . ssptk, registerReply)},ether(eee) > 
< JC : JVM | oCtr(0),
 {
< JC . cstm : STM | pkey(cPk),skey(cSk),policy(cP) > 
< JC . csptk : CSPTK2 | idle,clientId("sam"),lookup(JL . lup),stms(JC . cstm),
    checksn(true),ts(sPk) > 
< JC . app : APP | idle,svcFound(none),mytk(JC . csptk),todo(none),done(result(
    "GBPquote", mycall, noService) result("GBPquote", badcall, noService)) >},
    ether(eee) >

***checksn(false)
rewrite in TEST2-LOOKUP : eecf aljcf sjcf cjcf .
rewrites: 699 in 50ms cpu (57ms real) (13980 rewrites/second)
result OConf: 
< eee : Transmitter | inQ(none),outQ(none) > 
< JL : JVM | oCtr(2),
 {
< JL . AttackSvc : SVC | state(attackData) > 
< JL . cstm : STM | pkey(aPk),skey(aSk),policy(aP) > 
< JL . ssptk : SSPTK2 | idle,lookup(JL . lup),stms(JL . cstm) > 
< JL . csptk : CSPTK2 | idle,clientId(fakeId),lookup(JL . lup),stms(JL . cstm),
    checksn(false),ts(sPk) > 
< JL . app : APP | idle,svcFound(b("GBPquote", JL . o(1))),mytk(JL . csptk),
    todo(none),done(result("GBPquote", fakeCall, reply(GBPdata, fakeCall,
    fakeId))) > 
< JL . lup : AttackerLookup | svcSet(signed(proxyD(CSP1, svc(JS . o(0)),sname(
    "GBPquote")), sSk) signed(proxyD(CSP1, svc(JS . o(1)),sname("USquote")),
    sSk)),mySvcSet(signed(proxyD(CSP1, svc(JL . o(0)),sname("Attack")), aSk)),
    attackeeSet(signed(proxyD(CSP1, svc(JS . o(1)),sname("USquote")), sSk)),
    myCPTK(JL . csptk),mySPTK(JL . ssptk) > 
< JL . o(0) : SSP1 | idle,svc(JL . AttackSvc),sname("Attack") > 
< JL . o(1) : CSP1 | idle,svc(JS . o(0)),clientId(fakeId),sname("GBPquote") > 
msg(JL . fred, JL . ssptk, registerReply)},ether(eee) > 
< JS : JVM | oCtr(2),
 {
< JS . GBPsvc : SVC | state(update(GBPdata, fakeCall, fakeId)) > 
< JS . USsvc : SVC | state(USdata) > 
< JS . sstm : STM | pkey(sPk),skey(sSk),policy(sP) > 
< JS . ssptk : SSPTK2 | idle,lookup(JL . lup),stms(JS . sstm) > 
< JS . o(0) : SSP1 | idle,svc(JS . GBPsvc),sname("GBPquote") > 
< JS . o(1) : SSP1 | idle,svc(JS . USsvc),sname("USquote") > 
msg(JS . fred, JS . ssptk, registerReply) 
msg(JS . fred, JS . ssptk, registerReply)},ether(eee) > 
< JC : JVM | oCtr(0),
 {
< JC . cstm : STM | pkey(cPk),skey(cSk),policy(cP) > 
< JC . csptk : CSPTK2 | idle,clientId("sam"),lookup(JL . lup),stms(JC . cstm),
    checksn(false),ts(sPk) > 
< JC . app : APP | idle,svcFound(none),mytk(JC . csptk),todo(none),done(result(
    "GBPquote", mycall, noService) result("GBPquote", badcall, noService)) >},
    ether(eee) >