03mar02

rewrite in TEST3-ETHER : eecf sjcf cjcf ljcf .
rewrites: 493 in 60ms cpu (64ms real) (8216 rewrites/second)
result OConf: 
< eee : Transmitter | inQ(none),outQ(none) > 
< JL : JVM | oCtr(0),
 {
< JL . lup : LOOKUP | svctable(("GBPquote" := signed(proxyD(CAP, svc(JS . o(
    0)),sname("GBPquote")), sSk)),"USquote" := signed(proxyD(CAP, svc(JS . o(
    1)),sname("USquote")), sSk)) >},ether(eee) > 
< JS : JVM | oCtr(3),
 {
< JS . GBPsvc : SVC | state(update(GBPdata, mycall, "sam")) > 
< 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", myCred, sP)) > 
msg(JS . fred, JS . ssptk, registerReply) 
msg(JS . fred, JS . ssptk, registerReply)},ether(eee) > 
< JC : JVM | oCtr(2),
 {
< 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(b("GBPquote", JC . o(1))),mytk(JC . csptk),
    todo(none),done(result("GBPquote", mycall, reply(GBPdata, mycall, "sam"))
    result("GBPquote", badcall, badData)) > 
< JC . o(0) : CAP | idle,svc(JS . o(0)),stms(JC . cstm) > 
< JC . o(1) : CSSP | idle,svc(JS . o(2)) >},ether(eee) >


rewrite in TEST3-ETHER : eacf sjcf cjcf ljcf .
rewrites: 459 in 50ms cpu (52ms real) (9180 rewrites/second)
result OConf: 
< eee : Attacker | inQ(none),outQ(none),clientIds(none),clientDs(none),pxDs(
    signed(proxyD(CAP, svc(JS . o(0)),sname("GBPquote")), sSk) signed(proxyD(
    CAP, svc(JS . o(1)),sname("USquote")), sSk)) > 
< JL : JVM | oCtr(0),
 {
< JL . lup : LOOKUP | svctable(none) >},ether(eee) > 
< JS : JVM | oCtr(3),
 {
< JS . GBPsvc : SVC | state(update(GBPdata, mycall, "sam")) > 
< 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", myCred, sP)) > 
msg(JS . fred, JS . ssptk, registerReply) 
msg(JS . fred, JS . ssptk, registerReply)},ether(eee) > 
< JC : JVM | oCtr(2),
 {
< 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(b("GBPquote", JC . o(1))),mytk(JC . csptk),
    todo(none),done(result("GBPquote", mycall, reply(GBPdata, mycall, "sam"))
    result("GBPquote", badcall, badData)) > 
< JC . o(0) : CAP | idle,svc(JS . o(0)),stms(JC . cstm) > 
< JC . o(1) : CSSP | idle,svc(JS . o(2)) >},ether(eee) >


rewrite in TEST3-ETHER : eecf sjcf ljcf ajcf cjcf .
rewrites: 1053 in 130ms cpu (124ms real) (8100 rewrites/second)
result OConf: 
< eee : Transmitter | inQ(none),outQ(none) > 
< JL : JVM | oCtr(0),
 {
< JL . lup : LOOKUP | svctable(("GBPquote" := signed(proxyD(CAP, svc(JS . o(
    0)),sname("GBPquote")), sSk)),"USquote" := signed(proxyD(CAP, svc(JS . o(
    1)),sname("USquote")), sSk)) >},ether(eee) > 
< JS : JVM | oCtr(5),
 {
< JS . GBPsvc : SVC | state(update(GBPdata, mycall, "sam")) > 
< 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", myCred, sP)) > 
< JS . o(3) : SSSP | idle,svc(JS . GBPsvc),sname("GBPquote"),perms(clientPerm(
    "GBPquote", fakeCred, sP)) > 
< JS . o(4) : SSSP | idle,svc(JS . USsvc),sname("USquote"),perms(clientPerm(
    "USquote", fakeCred, sP)) > 
msg(JS . fred, JS . ssptk, registerReply) 
msg(JS . fred, JS . ssptk, registerReply)},ether(eee) > 
< JC : JVM | oCtr(2),
 {
< 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(b("GBPquote", JC . o(1))),mytk(JC . csptk),
    todo(none),done(result("GBPquote", mycall, reply(GBPdata, mycall, "sam"))
    result("GBPquote", badcall, badData)) > 
< JC . o(0) : CAP | idle,svc(JS . o(0)),stms(JC . cstm) > 
< JC . o(1) : CSSP | idle,svc(JS . o(2)) >},ether(eee) > 
< JA : JVM | oCtr(4),
 {
< JA . cstm : STM | pkey(aPk),skey(aSk),policy(aP) > 
< JA . csptk : CSPTK3 | idle,stms(JA . cstm),lookup(JL . lup),cred(fakeCred),
    ts(sPk) > 
< JA . app : APP | idle,svcFound(b("GBPquote", JA . o(1)) b("USquote", JA . o(
    3))),mytk(JA . csptk),todo(none),done(result("GBPquote", fakeCall, badData)
    result("USquote", fakeCall, badData)) > 
< JA . o(0) : CAP | idle,svc(JS . o(0)),stms(JA . cstm) > 
< JA . o(1) : CSSP | idle,svc(JS . o(3)) > 
< JA . o(2) : CAP | idle,svc(JS . o(1)),stms(JA . cstm) > 
< JA . o(3) : CSSP | idle,svc(JS . o(4)) >},ether(eee) >


rewrite in TEST3-ETHER : eacf sjcf ljcf ajcf cjcf .
rewrites: 795 in 90ms cpu (92ms real) (8833 rewrites/second)
result OConf: 
< eee : Attacker | inQ(none),outQ(none),clientIds(none),clientDs(none),pxDs(
    signed(proxyD(CAP, svc(JS . o(0)),sname("GBPquote")), sSk) signed(proxyD(
    CAP, svc(JS . o(1)),sname("USquote")), sSk)) > 
< JL : JVM | oCtr(0),
 {
< JL . lup : LOOKUP | svctable(none) >},ether(eee) > 
< JS : JVM | oCtr(4),
 {
< JS . GBPsvc : SVC | state(update(GBPdata, mycall, "sam")) > 
< 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", myCred, sP)) > 
< JS . o(3) : SSSP | idle,svc(JS . GBPsvc),sname("GBPquote"),perms(clientPerm(
    "GBPquote", fakeCred, sP)) > 
msg(JS . fred, JS . ssptk, registerReply) 
msg(JS . fred, JS . ssptk, registerReply)},ether(eee) > 
< JC : JVM | oCtr(2),
 {
< 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(b("GBPquote", JC . o(1))),mytk(JC . csptk),
    todo(none),done(result("GBPquote", mycall, reply(GBPdata, mycall, "sam"))
    result("GBPquote", badcall, badData)) > 
< JC . o(0) : CAP | idle,svc(JS . o(0)),stms(JC . cstm) > 
< JC . o(1) : CSSP | idle,svc(JS . o(2)) >},ether(eee) > 
< JA : JVM | oCtr(3),
 {
< JA . cstm : STM | pkey(aPk),skey(aSk),policy(aP) > 
< JA . csptk : CSPTK3 | idle,stms(JA . cstm),lookup(JL . lup),cred(fakeCred),
    ts(sPk) > 
< JA . app : APP | idle,svcFound(b("GBPquote", JA . o(1))),mytk(JA . csptk),
    todo(none),done(result("GBPquote", fakeCall, badData) result("USquote",
    fakeCall, noService)) > 
< JA . o(0) : CAP | idle,svc(JS . o(0)),stms(JA . cstm) > 
< JA . o(1) : CSSP | idle,svc(JS . o(3)) >},ether(eee) >