03mar02

rewrite in TEST2-ETHER : eecf sjcf cjcf ljcf .
rewrites: 384 in 40ms cpu (36ms real) (9600 rewrites/second)
result OConf: 
< eee : Transmitter | inQ(none),outQ(none) > 
< JL : JVM | oCtr(0),
 {
< JL . lup : LOOKUP | svctable(("GBPquote" := signed(proxyD(CSP1, svc(JS . o(
    0)),sname("GBPquote")), sSk)),"USquote" := signed(proxyD(CSP1, svc(JS . o(
    1)),sname("USquote")), sSk)) >},ether(eee) > 
< JS : JVM | oCtr(2),
 {
< JS . GBPsvc : SVC | state(update(update(GBPdata, mycall, "sam"), badcall,
    "sam")) > 
< 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(1),
 {
< 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(b("GBPquote", JC . o(0))),mytk(JC . csptk),
    todo(none),done(result("GBPquote", mycall, reply(GBPdata, mycall, "sam"))
    result("GBPquote", badcall, reply(update(GBPdata, mycall, "sam"), badcall,
    "sam"))) > 
< JC . o(0) : CSP1 | idle,svc(JS . o(0)),clientId("sam"),sname("GBPquote") >},
    ether(eee) >


rewrite in TEST2-ETHER : eacf sjcf cjcf ljcf .
rewrites: 350 in 30ms cpu (34ms real) (11666 rewrites/second)
result OConf: 
< eee : Attacker | inQ(none),outQ(none),clientIds(none),clientDs(none),pxDs(
    signed(proxyD(CSP1, svc(JS . o(0)),sname("GBPquote")), sSk) signed(proxyD(
    CSP1, svc(JS . o(1)),sname("USquote")), sSk)) > 
< JL : JVM | oCtr(0),
 {
< JL . lup : LOOKUP | svctable(none) >},ether(eee) > 
< JS : JVM | oCtr(2),
 {
< JS . GBPsvc : SVC | state(update(update(GBPdata, mycall, "sam"), badcall,
    "sam")) > 
< 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(1),
 {
< 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(b("GBPquote", JC . o(0))),mytk(JC . csptk),
    todo(none),done(result("GBPquote", mycall, reply(GBPdata, mycall, "sam"))
    result("GBPquote", badcall, reply(update(GBPdata, mycall, "sam"), badcall,
    "sam"))) > 
< JC . o(0) : CSP1 | idle,svc(JS . o(0)),clientId("sam"),sname("GBPquote") >},
    ether(eee) >

rewrite in TEST2-ETHER : eecf sjcf ljcf ajcf cjcf .
rewrites: 732 in 70ms cpu (71ms real) (10457 rewrites/second)
result OConf: 
< eee : Transmitter | inQ(none),outQ(none) > 
< JL : JVM | oCtr(0),
 {
< JL . lup : LOOKUP | svctable(("GBPquote" := signed(proxyD(CSP1, svc(JS . o(
    0)),sname("GBPquote")), sSk)),"USquote" := signed(proxyD(CSP1, svc(JS . o(
    1)),sname("USquote")), sSk)) >},ether(eee) > 
< JS : JVM | oCtr(2),
 {
< JS . GBPsvc : SVC | state(update(update(update(GBPdata, mycall, "sam"),
    badcall, "sam"), fakeCall, fakeId)) > 
< JS . USsvc : SVC | state(update(USdata, fakeCall, fakeId)) > 
< 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(1),
 {
< 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(b("GBPquote", JC . o(0))),mytk(JC . csptk),
    todo(none),done(result("GBPquote", mycall, reply(GBPdata, mycall, "sam"))
    result("GBPquote", badcall, reply(update(GBPdata, mycall, "sam"), badcall,
    "sam"))) > 
< JC . o(0) : CSP1 | idle,svc(JS . o(0)),clientId("sam"),sname("GBPquote") >},
    ether(eee) > 
< JA : JVM | oCtr(2),
 {
< JA . cstm : STM | pkey(aPk),skey(aSk),policy(aP) > 
< JA . csptk : CSPTK2 | idle,clientId(fakeId),lookup(JL . lup),stms(JA . cstm),
    checksn(false),ts(sPk) > 
< JA . app : APP | idle,svcFound(b("GBPquote", JA . o(0)) b("USquote", JA . o(
    1))),mytk(JA . csptk),todo(none),done(result("GBPquote", fakeCall, reply(
    update(update(GBPdata, mycall, "sam"), badcall, "sam"), fakeCall, fakeId))
    result("USquote", fakeCall, reply(USdata, fakeCall, fakeId))) > 
< JA . o(0) : CSP1 | idle,svc(JS . o(0)),clientId(fakeId),sname("GBPquote") > 
< JA . o(1) : CSP1 | idle,svc(JS . o(1)),clientId(fakeId),sname("USquote") >},
    ether(eee) >

rewrite in TEST2-ETHER : eacf sjcf ljcf ajcf cjcf .
rewrites: 652 in 70ms cpu (65ms real) (9314 rewrites/second)
result OConf: 
< eee : Attacker | inQ(none),outQ(none),clientIds(none),clientDs(none),pxDs(
    signed(proxyD(CSP1, svc(JS . o(0)),sname("GBPquote")), sSk) signed(proxyD(
    CSP1, svc(JS . o(1)),sname("USquote")), sSk)) > 
< JL : JVM | oCtr(0),
 {
< JL . lup : LOOKUP | svctable(none) >},ether(eee) > 
< JS : JVM | oCtr(2),
 {
< JS . GBPsvc : SVC | state(update(update(update(update(GBPdata, mycall,
    "sam"), badcall, "sam"), fakeCall, fakeId), 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(1),
 {
< 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(b("GBPquote", JC . o(0))),mytk(JC . csptk),
    todo(none),done(result("GBPquote", mycall, reply(GBPdata, mycall, "sam"))
    result("GBPquote", badcall, reply(update(GBPdata, mycall, "sam"), badcall,
    "sam"))) > 
< JC . o(0) : CSP1 | idle,svc(JS . o(0)),clientId("sam"),sname("GBPquote") >},
    ether(eee) > 
< JA : JVM | oCtr(2),
 {
< JA . cstm : STM | pkey(aPk),skey(aSk),policy(aP) > 
< JA . csptk : CSPTK2 | idle,clientId(fakeId),lookup(JL . lup),stms(JA . cstm),
    checksn(false),ts(sPk) > 
< JA . app : APP | idle,svcFound(b("GBPquote", JA . o(0)) b("USquote", JA . o(
    1))),mytk(JA . csptk),todo(none),done(result("GBPquote", fakeCall, reply(
    update(update(GBPdata, mycall, "sam"), badcall, "sam"), fakeCall, fakeId))
    result("USquote", fakeCall, reply(update(update(update(GBPdata, mycall,
    "sam"), badcall, "sam"), fakeCall, fakeId), fakeCall, fakeId))) > 
< JA . o(0) : CSP1 | idle,svc(JS . o(0)),clientId(fakeId),sname("GBPquote") > 
< JA . o(1) : CSP1 | idle,svc(JS . o(0)),clientId(fakeId),sname("GBPquote") >},
    ether(eee) >