03mar03

rewrite in TEST3-LOOKUP : eecf aljcf sjcf cjcf .
rewrites: 850 in 80ms cpu (78ms real) (10625 rewrites/second)
result OConf: 
< eee : Transmitter | inQ(none),outQ(none) > 
< JL : JVM | oCtr(3),
 {
< JL . AttackSvc : SVC | state(attackData) > 
< JL . cstm : STM | pkey(aPk),skey(aSk),policy(aP) > 
< JL . ssptk : SSPTK3 | idle,stms(JL . cstm),lookup(JL . lup) > 
< JL . csptk : CSPTK3 | idle,stms(JL . cstm),lookup(JL . lup),cred(aCred),ts(
    sPk) > 
< JL . app : APP | idle,svcFound(b("GBPquote", JL . o(2))),mytk(JL . csptk),
    todo(none),done(result("GBPquote", fakeCall, badData)) > 
< JL . lup : AttackerLookup | svcSet(signed(proxyD(CAP, svc(JS . o(0)),sname(
    "GBPquote")), sSk) signed(proxyD(CAP, svc(JS . o(1)),sname("USquote")),
    sSk)),mySvcSet(signed(proxyD(CAP, svc(JL . o(0)),sname("Attack")), aSk)),
    attackeeSet(signed(proxyD(CAP, svc(JS . o(1)),sname("USquote")), sSk)),
    myCPTK(JL . csptk),mySPTK(JL . ssptk) > 
< JL . o(0) : SAP | idle,svc(JL . AttackSvc),sname("Attack"),stms(JL . cstm) > 
< JL . o(1) : CAP | idle,svc(JS . o(0)),stms(JL . cstm) > 
< JL . o(2) : CSSP | idle,svc(JS . o(2)) > 
msg(JL . fred, JL . ssptk, registerReply)},ether(eee) > 
< JS : JVM | oCtr(3),
 {
< JS . GBPsvc : SVC | state(GBPdata) > 
< JS . USsvc : SVC | state(USdata) > 
< JS . sstm : STM | pkey(sPk),skey(sSk),policy(sP) > 
< JS . ssptk : SSPTK3 | idle,stms(JS . sstm),lookup(JL . lup) > 
< JS . o(0) : SAP | idle,svc(JS . GBPsvc),sname("GBPquote"),stms(JS . sstm) > 
< JS . o(1) : SAP | idle,svc(JS . USsvc),sname("USquote"),stms(JS . sstm) > 
< JS . o(2) : SSSP | idle,svc(JS . GBPsvc),sname("GBPquote"),perms(clientPerm(
    "GBPquote", aCred, sP)) > 
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 : CSPTK3 | idle,stms(JC . cstm),lookup(JL . lup),cred(myCred),ts(
    sPk) > 
< JC . app : APP | idle,svcFound(none),mytk(JC . csptk),todo(none),done(result(
    "GBPquote", mycall, noService) result("GBPquote", badcall, noService)) >},
    ether(eee) >