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

No solution.
states: 922  rewrites: 8628 in 1440ms cpu (1480ms real) (5991 rewrites/second)


*** 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(reply(d:Data, mycall,"sam") cds:DataSet)> ) .
                    
No solution.
states: 922  rewrites: 8628 in 1450ms cpu (1466ms real) (5950 rewrites/second)

*** 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 419)
states: 420  rewrites: 3820 in 610ms cpu (615ms real) (6262 rewrites/second)
cf:Configuration --> 
< eee : Attacker | inQ(none),outQ(deliver(JS, 
msg(JS . ssptk, JL . lup, registerReply))),clientIds(none),clientDs(none),pxDs(
    proxyD(CSP1, 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 : SSPTK1 | lookup(JL . lup),waitfor(JL . lup, JS . fred,
    spRegisterReq("USquote", JS . USsvc)) > 
< JS . o(0) : SSP1 | 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,clientId("sam"),lookup(JL . lup) > 
< JC . o(0) : CSP1 | 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 744)
states: 745  rewrites: 6881 in 1140ms cpu (1143ms real) (6035 rewrites/second)
cf:Configuration --> 
< eee : Attacker | inQ(none),outQ(deliver(JS, 
msg(JS . ssptk, JL . lup, registerReply))),clientIds(none),clientDs(none),pxDs(
    proxyD(CSP1, 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 : SSPTK1 | lookup(JL . lup),waitfor(JL . lup, JS . fred,
    spRegisterReq("GBPquote", JS . GBPsvc)) > 
< JS . o(0) : SSP1 | 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,clientId("sam"),lookup(JL . lup) > 
< JC . o(0) : CSP1 | idle,svc(JS . o(0)),clientId("sam") >
catts:AttributeSet --> svcFound(b("GBPquote", JC . o(0))),mytk(JC . csptk),
    done(result("GBPquote", mycall, reply(GBPdata, mycall, "sam")))
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"))) } > ) .

No solution.  *** the attack app id is fakeId
states: 148145  rewrites: 1734332 in 336620ms cpu (337072ms real) (5152
    rewrites/second)
*** sam works if use "sam" version of aptkobs in test1-ether.m

*** attacker gets reply with data for fakeId
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, fakeId))) } > ) .

Solution 1 (state 13013)
states: 13014  rewrites: 145528 in 28700ms cpu (28713ms real) (5070
    rewrites/second)
cfx:Configuration --> 
< eee : Transmitter | inQ(none),outQ(none) > 
< JL : JVM | oCtr(0),
 {
< JL . lup : LOOKUP | svctable("GBPquote" := proxyD(CSP1, svc(JS . o(0)))) > 
msg(JS . ssptk, JL . lup, registerReply)},ether(eee) > 
< JS : JVM | oCtr(1),
 {
< JS . GBPsvc : SVC | state(update(GBPdata, fakeCall, fakeId)) > 
< JS . USsvc : SVC | state(USdata) > 
< JS . ssptk : SSPTK1 | lookup(JL . lup),waitfor(JL . lup, JS . fred,
    spRegisterReq("GBPquote", JS . GBPsvc)) > 
< JS . o(0) : SSP1 | 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,clientId("sam"),lookup(JL . lup) > 
< 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,clientId(fakeId),lookup(JL . lup) > 
< JA . o(0) : CSP1 | idle,svc(JS . o(0)),clientId(fakeId) >
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