*****  in TEST0-ETHER  *******************************************************
*** attacker gets private data sent in call
search [1] (eacf ljcf sjcf cjcf) =>+
  cf:Configuration 
  < eee : Attacker | atts:AttributeSet,clientDs(mycall cds:DataSet) > .

Solution 1 (state 199)
states: 200  rewrites: 1821 in 280ms cpu (292ms real) (6503 rewrites/second)
cf:Configuration --> 
< JL : JVM | oCtr(0),
 {
< JL . lup : LOOKUP | svctable(none) >},ether(eee) > 
< JS : JVM | oCtr(1),
 {
< JS . GBPsvc : SVC | state(GBPdata) > 
< JS . USsvc : SVC | state(USdata) > 
< JS . ssptk : SSPTK0 | lookup(JL . lup),waitfor(JL . lup, JS . fred,
    spRegisterReq("GBPquote", JS . GBPsvc)) > 
< JS . o(0) : SSP0 | idle,svc(JS . GBPsvc),sname("GBPquote") > 
msg(JS . ssptk, JS . fred, spRegisterReq("USquote", JS . USsvc))},ether(eee) > 
< JC : JVM | oCtr(1),
 {
< JC . csptk : CSPTK0 | idle,lookup(JL . lup),clientId("sam") > 
< JC . app : APP | waitfor(JC . o(0)),svcFound(b("GBPquote", JC . o(0))),mytk(
    JC . csptk),todo(task("GBPquote", mycall) task("GBPquote", badcall)),done(
    none) > 
< JC . o(0) : CSP0 | svc(JS . o(0)),clientId("sam"),waitfor(JS . o(0), JC .
    app, svcReq(mycall)) >},ether(eee) >
atts:AttributeSet --> inQ(none),outQ(deliver(JS, 
msg(JS . ssptk, JL . lup, registerReply)) deliver(JS, 
msg(JS . o(0), JC . o(0), svcReq(mycall, "sam")))),clientIds("sam"),pxDs(
    proxyD(CSP0, svc(JS . o(0))))
cds:DataSet --> (none).DataSet


*** attacker gets private data sent in reply (to query with private data)
search [1]  ( eacf ljcf sjcf cjcf ) =>+
  cf:Configuration 
  < eee : Attacker | atts:AttributeSet,
                     clientDs(cds:DataSet reply(d:Data, mycall, "sam")) > .

Solution 1 (state 354)
states: 355  rewrites: 3404 in 510ms cpu (525ms real) (6674 rewrites/second)
cf:Configuration --> 
< JL : JVM | oCtr(0),
 {
< JL . lup : LOOKUP | svctable(none) >},ether(eee) > 
< JS : JVM | oCtr(1),
 {
< JS . GBPsvc : SVC | state(update(GBPdata, mycall, "sam")) > 
< JS . USsvc : SVC | state(USdata) > 
< JS . ssptk : SSPTK0 | lookup(JL . lup),waitfor(JL . lup, JS . fred,
    spRegisterReq("GBPquote", JS . GBPsvc)) > 
< JS . o(0) : SSP0 | idle,svc(JS . GBPsvc),sname("GBPquote") > 
msg(JS . ssptk, JS . fred, spRegisterReq("USquote", JS . USsvc))},ether(eee) > 
< JC : JVM | oCtr(1),
 {
< JC . csptk : CSPTK0 | idle,lookup(JL . lup),clientId("sam") > 
< JC . app : APP | waitfor(JC . o(0)),svcFound(b("GBPquote", JC . o(0))),mytk(
    JC . csptk),todo(task("GBPquote", mycall) task("GBPquote", badcall)),done(
    none) > 
< JC . o(0) : CSP0 | svc(JS . o(0)),clientId("sam"),waitfor(JS . o(0), JC .
    app, svcReq(mycall)) >},ether(eee) >
atts:AttributeSet --> inQ(none),outQ(deliver(JS, 
msg(JS . ssptk, JL . lup, registerReply)) deliver(JC, 
msg(JC . o(0), JS . o(0), svcReply(mycall)))),clientIds("sam"),pxDs(proxyD(
    CSP0, svc(JS . o(0))))
cds:DataSet --> mycall
d:Data --> GBPdata


*** user gets answer from wrong service
search [1] (eacf ljcf sjcf cjcf1) =>+ 
   ( cf:Configuration
    < JC : JVM | jatts:AttributeSet,
      { cfig:Configuration
        < (JC . app) : APP | catts:AttributeSet,
                           todo(task("GBPquote", mycall) ts:Tasks),
                           waitfor(sid:Oid)  >
        msg(JC . app, sid:Oid, svcReply(reply(USdata, mycall, "sam")))
       }  > ) .

Solution 1 (state 431)
states: 432  rewrites: 4228 in 640ms cpu (643ms real) (6606 rewrites/second)
cf:Configuration --> 
< eee : Attacker | inQ(none),outQ(deliver(JS, 
msg(JS . ssptk, JL . lup, registerReply))),clientIds("sam"),clientDs(mycall
    reply(USdata, mycall, "sam")),pxDs(proxyD(CSP0, svc(JS . o(0)))) > 
< JL : JVM | oCtr(0),
 {
< JL . lup : LOOKUP | svctable(none) >},ether(eee) > 
< JS : JVM | oCtr(1),
 {
< JS . GBPsvc : SVC | state(GBPdata) > 
< JS . USsvc : SVC | state(update(USdata, mycall, "sam")) > 
< JS . ssptk : SSPTK0 | lookup(JL . lup),waitfor(JL . lup, JS . fred,
    spRegisterReq("USquote", JS . USsvc)) > 
< JS . o(0) : SSP0 | idle,svc(JS . USsvc),sname("USquote") > 
msg(JS . ssptk, JS . fred, spRegisterReq("GBPquote", JS . GBPsvc))},ether(eee)
    >
jatts:AttributeSet --> oCtr(1),ether(eee)
cfig:Configuration --> 
< JC . csptk : CSPTK0 | idle,lookup(JL . lup),clientId("sam") > 
< JC . o(0) : CSP0 | idle,svc(JS . o(0)),clientId("sam") >
catts:AttributeSet --> svcFound(b("GBPquote", JC . o(0))),mytk(JC . csptk),
    done(none)
sid:Oid --> JC . o(0)
ts:Tasks --> (none).Tasks

*** user gets reply to non-permitted call to GBP
search [1] (eacf ljcf sjcf cjcf) =>+ 
   ( cf:Configuration
    < JC : JVM | jatts:AttributeSet,
      { cfig:Configuration
        < JC . app : APP | catts:AttributeSet,
                           todo(task("GBPquote", badcall) ts:Tasks),
                           waitfor(sid:Oid)  >
        msg(JC . app, sid:Oid, svcReply(reply(d:Data, badcall, "sam")))

       }  > )  such that initData(d:Data) == GBPdata .

Solution 1 (state 1495)
states: 1496  rewrites: 14553 in 2350ms cpu (2346ms real) (6192
    rewrites/second)
cf:Configuration --> 
< eee : Attacker | inQ(none),outQ(deliver(JS, 
msg(JS . ssptk, JL . lup, registerReply))),clientIds("sam"),clientDs(mycall
    badcall reply(GBPdata, mycall, "sam") reply(update(GBPdata, mycall, "sam"),
    badcall, "sam")),pxDs(proxyD(CSP0, svc(JS . o(0)))) > 
< JL : JVM | oCtr(0),
 {
< JL . lup : LOOKUP | svctable(none) >},ether(eee) > 
< JS : JVM | oCtr(1),
 {
< JS . GBPsvc : SVC | state(update(update(GBPdata, mycall, "sam"), badcall,
    "sam")) > 
< JS . USsvc : SVC | state(USdata) > 
< JS . ssptk : SSPTK0 | lookup(JL . lup),waitfor(JL . lup, JS . fred,
    spRegisterReq("GBPquote", JS . GBPsvc)) > 
< JS . o(0) : SSP0 | idle,svc(JS . GBPsvc),sname("GBPquote") > 
msg(JS . ssptk, JS . fred, spRegisterReq("USquote", JS . USsvc))},ether(eee) >
jatts:AttributeSet --> oCtr(1),ether(eee)
cfig:Configuration --> 
< JC . csptk : CSPTK0 | idle,lookup(JL . lup),clientId("sam") > 
< JC . o(0) : CSP0 | idle,svc(JS . o(0)),clientId("sam") >
catts:AttributeSet --> svcFound(b("GBPquote", JC . o(0))),mytk(JC . csptk),
    done(result("GBPquote", mycall, mycall))
sid:Oid --> JC . o(0)
ts:Tasks --> (none).Tasks
d:Data --> update(GBPdata, mycall, "sam")


*** attacker gets reply with data for "sam"
search [1] (eecf ljcf sjcf cjcf ajcf ) =>+ 
   ( cfx:Configuration    < JA : JVM | jatts:AttributeSet,
        { cf:Configuration
          < JA . app : APP | catts:AttributeSet,todo(ts:Tasks),
                             waitfor(sid:Oid) > 
       msg(JA . app, sid:Oid, svcReply(reply(d:Data, dc:Data, "sam"))) } > ) .


Solution 1 (state 13013)
states: 13014  rewrites: 145420 in 26300ms cpu (26401ms real) (5529
    rewrites/second)
cfx:Configuration --> 
< eee : Transmitter | inQ(none),outQ(none) > 
< JL : JVM | oCtr(0),
 {
< JL . lup : LOOKUP | svctable("GBPquote" := proxyD(CSP0, svc(JS . o(0)))) > 
msg(JS . ssptk, JL . lup, registerReply)},ether(eee) > 
< JS : JVM | oCtr(1),
 {
< JS . GBPsvc : SVC | state(update(GBPdata, fakeCall, "sam")) > 
< JS . USsvc : SVC | state(USdata) > 
< JS . ssptk : SSPTK0 | lookup(JL . lup),waitfor(JL . lup, JS . fred,
    spRegisterReq("GBPquote", JS . GBPsvc)) > 
< JS . o(0) : SSP0 | idle,svc(JS . GBPsvc),sname("GBPquote") > 
msg(JS . ssptk, JS . fred, spRegisterReq("USquote", JS . USsvc))},ether(eee) > 
< JC : JVM | oCtr(0),
 {
< JC . csptk : CSPTK0 | idle,lookup(JL . lup),clientId("sam") > 
< JC . app : APP | idle,svcFound(none),mytk(JC . csptk),todo(task("GBPquote",
    mycall) task("GBPquote", badcall)),done(none) >},ether(eee) >
jatts:AttributeSet --> oCtr(1),ether(eee)
cf:Configuration --> 
< JA . csptk : CSPTK0 | idle,lookup(JL . lup),clientId("sam") > 
< JA . o(0) : CSP0 | idle,svc(JS . o(0)),clientId("sam") >
catts:AttributeSet --> svcFound(b("GBPquote", JA . o(0))),mytk(JA . csptk),
    done(none)
sid:Oid --> JA . o(0)
ts:Tasks --> task("GBPquote", fakeCall) task("USquote", fakeCall)
d:Data --> GBPdata
dc:Data --> fakeCall