******************* checksn(true) **********************
*** 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: 1048  rewrites: 10550 in 2550ms cpu (2550ms real) (4137
    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: 1048  rewrites: 10550 in 2230ms cpu (2225ms real) (4730
    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")))
       }  > ) .

No solution.
states: 568  rewrites: 5868 in 1210ms cpu (1208ms real) (4849 rewrites/second)

*** 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 876)
states: 877  rewrites: 8959 in 1820ms cpu (1874ms real) (4922 rewrites/second)
cf:Configuration --> 
< eee : Attacker | inQ(none),outQ(deliver(JS, 
msg(JS . ssptk, JL . lup, registerReply))),clientIds(none),clientDs(none),pxDs(
    signed(proxyD(CSP1, svc(JS . o(0)),sname("GBPquote")), sSk)) > 
< 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 . sstm : STM | pkey(sPk),skey(sSk),policy(sP) > 
< JS . ssptk : SSPTK2 | lookup(JL . lup),stms(JS . sstm),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 . 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 . o(0) : CSP1 | idle,svc(JS . o(0)),clientId("sam"),sname("GBPquote") >
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 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 17835)
states: 17836  rewrites: 209655 in 47430ms cpu (47477ms real) (4420
    rewrites/second)
cfx:Configuration --> 
< 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)) > 
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 . sstm : STM | pkey(sPk),skey(sSk),policy(sP) > 
< JS . ssptk : SSPTK2 | lookup(JL . lup),stms(JS . sstm),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 . 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(none),mytk(JC . csptk),todo(task("GBPquote",
    mycall) task("GBPquote", badcall)),done(none) >},ether(eee) >
jatts:AttributeSet --> oCtr(1),ether(eee)
cf:Configuration --> 
< 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 . o(0) : CSP1 | idle,svc(JS . o(0)),clientId(fakeId),sname("GBPquote") >
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


******* reload test2-ether.m with alternative checksn line
         ******************* checksn(false) **********************

*** 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 525)
states: 526  rewrites: 5324 in 1460ms cpu (1452ms real) (3646 rewrites/second)
cf:Configuration --> 
< eee : Attacker | inQ(none),outQ(deliver(JS, 
msg(JS . ssptk, JL . lup, registerReply))),clientIds(none),clientDs(none),pxDs(
    signed(proxyD(CSP1, svc(JS . o(0)),sname("USquote")), sSk)) > 
< 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 . sstm : STM | pkey(sPk),skey(sSk),policy(sP) > 
< JS . ssptk : SSPTK2 | lookup(JL . lup),stms(JS . sstm),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 . cstm : STM | pkey(cPk),skey(cSk),policy(cP) > 
< JC . csptk : CSPTK2 | idle,clientId("sam"),lookup(JL . lup),stms(JC . cstm),
    checksn(false),ts(sPk) > 
< JC . o(0) : CSP1 | idle,svc(JS . o(0)),clientId("sam"),sname("USquote") >
catts:AttributeSet --> svcFound(b("GBPquote", JC . o(0))),mytk(JC . csptk),
    done(none)
sid:Oid --> JC . o(0)
ts:Tasks --> (none).Tasks