*** level independent
load ../ALL/all-ether.m
*** level specific
load sp0.m       *** CSP0 SSP0
load sptk0.m     *** CSPTK0  SSPTK0

mod TEST0-ETHER is
  inc TEST-ETHER .
  inc CSPTK0 .
  inc SSPTK0 .
  inc CSP0 .
  inc SSP0 .

  eq sptkobs = < (JS . ssptk) : SSPTK0 | lookup(JL . lup),idle >  .

  eq cptkobs = 
     < (JC . csptk) : CSPTK0 | lookup(JL . lup), clientId("sam"), idle >  .

  eq aptkobs = 
***     < (JA .  csptk) : CSPTK0 | lookup(JL . lup), clientId(fakeId), idle > .
     < (JA .  csptk) : CSPTK0 | lookup(JL . lup), clientId("sam"), idle > .

endm


***(
*** see runs0-ether.txt
rew eecf sjcf ljcf cjcf  .
rew eecf sjcf ljcf cjcf ajcf .
rew eacf sjcf ljcf cjcf  .

)


***( Patterns

*** 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 324)
states: 325  rewrites: 3973 in 400ms cpu (402ms real) (9932 rewrites/second)
cf:Configuration --> 
< JL : JVM | oCtr(0),
 {
< JL . lup : LOOKUP | svctable(none) >},ether(eee) > 
< JS : JVM | oCtr(0),
 {
< 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)) > 
msg(JS . ssptk, JS . fred, spRegisterReq("USquote", JS . USsvc))},ether(eee) > 
< JC : JVM | oCtr(1),
 {
< JC . csptk : CSPTK0 | idle,clientId("sam"),lookup(JL . lup) > 
< JC . app : APP | svcFound(b("GBPquote", JC . o(0))),mytk(JC . csptk),waitfor(
    JC . o(0), JC . sam, svcCall("GBPquote", mycall)) > 
< JC . o(0) : CP0 | svc(JS . GBPsvc),clientId("sam"),waitfor(JS . GBPsvc, JC .
    app, svcReq(mycall)) > 
msg(JC . app, JC . sam, svcCall("GBPquote", badcall))},ether(eee) >
atts:AttributeSet --> inQ(none),outQ(deliver(JS, 
msg(JS . GBPsvc, JC . o(0), svcReq(mycall, "sam"))) deliver(JS, 
msg(JS . ssptk, JL . lup, registerReply))),clientIds("sam"),pxDs(proxyD(CP0,
    svc(JS . GBPsvc)))
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(reply(d:Data, mycall,"sam") cds:DataSet)> ) .

Solution 1 (state 484)
states: 485  rewrites: 6222 in 610ms cpu (612ms real) (10200 rewrites/second)
cf:Configuration --> 
< JL : JVM | oCtr(0),
 {
< JL . lup : LOOKUP | svctable(none) >},ether(eee) > 
< JS : JVM | oCtr(0),
 {
< 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)) > 
msg(JS . ssptk, JS . fred, spRegisterReq("USquote", JS . USsvc))},ether(eee) > 
< JC : JVM | oCtr(1),
 {
< JC . csptk : CSPTK0 | idle,clientId("sam"),lookup(JL . lup) > 
< JC . app : APP | svcFound(b("GBPquote", JC . o(0))),mytk(JC . csptk),waitfor(
    JC . o(0), JC . sam, svcCall("GBPquote", mycall)) > 
< JC . o(0) : CP0 | svc(JS . GBPsvc),clientId("sam"),waitfor(JS . GBPsvc, JC .
    app, svcReq(mycall)) > 
msg(JC . app, JC . sam, svcCall("GBPquote", badcall))},ether(eee) >
atts:AttributeSet --> inQ(none),outQ(deliver(JS, 
msg(JS . ssptk, JL . lup, registerReply)) deliver(JC, 
msg(JC . o(0), JS . GBPsvc, svcReply(mycall)))),clientIds("sam"),pxDs(proxyD(
    CP0, svc(JS . GBPsvc)))
cds:DataSet --> mycall
d:Data --> GBPdata

*** user gets answer from wrong service

search [1] (eacf ljcf sjcf cjcf) =>+ 
   ( cf:Configuration
    < JC : JVM | atts:AttributeSet,
      { cfig:Configuration
        msg(JC . sam, o:Oid, svcAns("GBPquote", reply(USdata, mycall, "sam"))) 
       }  > ) .

Solution 1 (state 661)
states: 662  rewrites: 8655 in 820ms cpu (818ms real) (10554 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(CP0, svc(JS . USsvc))) > 
< JL : JVM | oCtr(0),
 {
< JL . lup : LOOKUP | svctable(none) >},ether(eee) > 
< JS : JVM | oCtr(0),
 {
< 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)) > 
msg(JS . ssptk, JS . fred, spRegisterReq("GBPquote", JS . GBPsvc))},ether(eee)
    >
atts:AttributeSet --> oCtr(1),ether(eee)
cfig:Configuration --> 
< JC . csptk : CSPTK0 | idle,clientId("sam"),lookup(JL . lup) > 
< JC . app : APP | idle,svcFound(b("GBPquote", JC . o(0))),mytk(JC . csptk) > 
< JC . o(0) : CP0 | idle,svc(JS . USsvc),clientId("sam") > 
msg(JC . app, JC . sam, svcCall("GBPquote", badcall))
o:Oid --> JC . app

*** user gets reply to non-permitted call

search [1] (eacf ljcf sjcf cjcf) =>+ 
   ( cf:Configuration
   < JC : JVM | atts:AttributeSet,
     { cfig:Configuration
       msg(JC . sam, o:Oid, svcAns("GBPquote", reply(d:Data, badcall, "sam"))) 
      }  > ) .

Solution 1 (state 637)
states: 638  rewrites: 8345 in 780ms cpu (781ms real) (10698 rewrites/second)
cf:Configuration --> 
< eee : Attacker | inQ(none),outQ(deliver(JS, 
msg(JS . ssptk, JL . lup, registerReply))),clientIds("sam"),clientDs(badcall
    reply(GBPdata, badcall, "sam")),pxDs(proxyD(CP0, svc(JS . GBPsvc))) > 
< JL : JVM | oCtr(0),
 {
< JL . lup : LOOKUP | svctable(none) >},ether(eee) > 
< JS : JVM | oCtr(0),
 {
< JS . GBPsvc : SVC | state(update(GBPdata, badcall, "sam")) > 
< JS . USsvc : SVC | state(USdata) > 
< JS . ssptk : SSPTK0 | lookup(JL . lup),waitfor(JL . lup, JS . fred,
    spRegisterReq("GBPquote", JS . GBPsvc)) > 
msg(JS . ssptk, JS . fred, spRegisterReq("USquote", JS . USsvc))},ether(eee) >
atts:AttributeSet --> oCtr(1),ether(eee)
cfig:Configuration --> 
< JC . csptk : CSPTK0 | idle,clientId("sam"),lookup(JL . lup) > 
< JC . app : APP | idle,svcFound(b("GBPquote", JC . o(0))),mytk(JC . csptk) > 
< JC . o(0) : CP0 | idle,svc(JS . GBPsvc),clientId("sam") > 
msg(JC . app, JC . sam, svcCall("GBPquote", mycall))
o:Oid --> JC . app
d:Data --> GBPdata

*** msg(JC . sam, JC . app, svcAns("GBPquote", badData)) 


)