*** client app can get good proxy
search [1] icf-aa =>+ 
   ( cf:Configuration 
    < JC : JVM | jcatts:AttributeSet,
      { cocf:Configuration
        < O:Oid : cl:Cid | svc(S:Oid), oatts:AttributeSet >
       msg(JC . app, JC . csptk, findServiceOk(sn:String, O:Oid))
      } >
    < JS : JVM | jsatts:AttributeSet,
     {  socf:Configuration
       < S:Oid : spc:Cid |  sname(sn:String), satts:AttributeSet >
      } > 
    )
   .

Solution 1 (state 1377)
states: 1378  rewrites: 15647 in 2480ms cpu (2482ms real) (6309
    rewrites/second)
cf:Configuration --> 
< eee : Transmitter | inQ(none),outQ(none) > 
< JL : JVM | oCtr(0),
 {
< JL . AttackSvc : SVC | state(attackData) > 
< JL . ssptk : SSPTK1 | idle,lookup(JL . lup) > 
< JL . csptk : CSPTK0 | idle,clientId(fakeId),lookup(JL . lup) > 
< JL . lup : AttackerLookup | svcSet(proxyD(CSP1, svc(JS . o(0)))),mySvcSet(
    none),attackeeSet(proxyD(CSP1, svc(JS . o(0)))),myCPTK(JL . csptk),mySPTK(
    JL . ssptk) > 
msg(JL . ssptk, JL . fred, spRegisterReq("Attack", JL . AttackSvc)) 
msg(JS . ssptk, JL . lup, registerReply)},ether(eee) >
jsatts:AttributeSet --> oCtr(1),ether(eee)
socf:Configuration --> 
< JS . GBPsvc : SVC | state(GBPdata) > 
< JS . USsvc : SVC | state(USdata) > 
< JS . ssptk : SSPTK1 | lookup(JL . lup),waitfor(JL . lup, JS . fred,
    spRegisterReq("GBPquote", JS . GBPsvc)) > 
msg(JS . ssptk, JS . fred, spRegisterReq("USquote", JS . USsvc))
S:Oid --> JS . o(0)
spc:Cid --> SSP1
satts:AttributeSet --> idle,svc(JS . GBPsvc)
sn:String --> "GBPquote"
jcatts:AttributeSet --> oCtr(1),ether(eee)
cocf:Configuration --> 
< JC . csptk : CSPTK0 | idle,clientId("sam"),lookup(JL . lup) > 
< JC . app : APP | waitfor(JC . csptk),svcFound(none),mytk(JC . csptk),todo(
    task("GBPquote", mycall)),done(none) >
O:Oid --> JC . o(0)
cl:Cid --> CSP1
oatts:AttributeSet --> idle,clientId("sam")


*** client app can get good proxy -- alternative
search [1] icf-aa =>+ 
   ( cf:Configuration 
    < JC : JVM | jcatts:AttributeSet,
      { cocf:Configuration
        < O:Oid : cl:Cid | svc(S:Oid), oatts:AttributeSet >
        < (JC . app) : APP | catts:AttributeSet,
                             todo(task(sn:String, cd:Data) ts:Tasks),
                             waitfor(sid:Oid)  >
          msg(JC . app, sid:Oid, findServiceOk(sn:String, O:Oid))
      } >
    < JS : JVM | jsatts:AttributeSet,
     {  socf:Configuration
       < S:Oid : spc:Cid |  sname(sn:String), satts:AttributeSet >
      } > 
    )    .

Solution 1 (state 1377)
states: 1378  rewrites: 15647 in 2450ms cpu (2448ms real) (6386
    rewrites/second)
cf:Configuration --> 
< eee : Transmitter | inQ(none),outQ(none) > 
< JL : JVM | oCtr(0),
 {
< JL . AttackSvc : SVC | state(attackData) > 
< JL . ssptk : SSPTK1 | idle,lookup(JL . lup) > 
< JL . csptk : CSPTK0 | idle,clientId(fakeId),lookup(JL . lup) > 
< JL . lup : AttackerLookup | svcSet(proxyD(CSP1, svc(JS . o(0)))),mySvcSet(
    none),attackeeSet(proxyD(CSP1, svc(JS . o(0)))),myCPTK(JL . csptk),mySPTK(
    JL . ssptk) > 
msg(JL . ssptk, JL . fred, spRegisterReq("Attack", JL . AttackSvc)) 
msg(JS . ssptk, JL . lup, registerReply)},ether(eee) >
jsatts:AttributeSet --> oCtr(1),ether(eee)
socf:Configuration --> 
< JS . GBPsvc : SVC | state(GBPdata) > 
< JS . USsvc : SVC | state(USdata) > 
< JS . ssptk : SSPTK1 | lookup(JL . lup),waitfor(JL . lup, JS . fred,
    spRegisterReq("GBPquote", JS . GBPsvc)) > 
msg(JS . ssptk, JS . fred, spRegisterReq("USquote", JS . USsvc))
S:Oid --> JS . o(0)
spc:Cid --> SSP1
satts:AttributeSet --> idle,svc(JS . GBPsvc)
sn:String --> "GBPquote"
jcatts:AttributeSet --> oCtr(1),ether(eee)
cocf:Configuration --> 
< JC . csptk : CSPTK0 | idle,clientId("sam"),lookup(JL . lup) >
O:Oid --> JC . o(0)
cl:Cid --> CSP1
oatts:AttributeSet --> idle,clientId("sam")
catts:AttributeSet --> svcFound(none),mytk(JC . csptk),done(none)
sid:Oid --> JC . csptk
cd:Data --> mycall
ts:Tasks --> (none).Tasks


*** client accepts proxy to attacker svc -- svc on compromised LUP
search [1] icf-aa =>+ 
   ( cf:Configuration 
    < JC : JVM | atts:AttributeSet,
      { ocf:Configuration
        < O:Oid : cl:Cid | svc(JL . o(i:Nat) ), satts:AttributeSet >
       msg(JC . app, JC . csptk, findServiceOk(sn:String, O:Oid))
      } > 
    )  .

Solution 1 (state 884)
states: 885  rewrites: 10044 in 1510ms cpu (1507ms real) (6651 rewrites/second)
cf:Configuration --> 
< eee : Transmitter | inQ(none),outQ(none) > 
< JL : JVM | oCtr(1),
 {
< JL . AttackSvc : SVC | state(attackData) > 
< JL . ssptk : SSPTK1 | lookup(JL . lup),waitfor(JL . lup, JL . fred,
    spRegisterReq("Attack", JL . AttackSvc)) > 
< JL . csptk : CSPTK0 | idle,clientId(fakeId),lookup(JL . lup) > 
< JL . lup : AttackerLookup | svcSet(none),mySvcSet(proxyD(CSP1, svc(JL . o(
    0)))),attackeeSet(none),myCPTK(JL . csptk),mySPTK(JL . ssptk) > 
< JL . o(0) : SSP1 | idle,svc(JL . AttackSvc),sname("Attack") > 
msg(JL . ssptk, JL . lup, registerReply)},ether(eee) > 
< JS : JVM | oCtr(0),
 {
< JS . GBPsvc : SVC | state(GBPdata) > 
< JS . USsvc : SVC | state(USdata) > 
< JS . ssptk : SSPTK1 | idle,lookup(JL . lup) > 
msg(JS . ssptk, JS . fred, spRegisterReq("GBPquote", JS . GBPsvc)) 
msg(JS . ssptk, JS . fred, spRegisterReq("USquote", JS . USsvc))},ether(eee) >
atts:AttributeSet --> oCtr(1),ether(eee)
ocf:Configuration --> 
< JC . csptk : CSPTK0 | idle,clientId("sam"),lookup(JL . lup) > 
< JC . app : APP | waitfor(JC . csptk),svcFound(none),mytk(JC . csptk),todo(
    task("GBPquote", mycall)),done(none) >
O:Oid --> JC . o(0)
cl:Cid --> CSP1
satts:AttributeSet --> idle,clientId("sam")
i:Nat --> 0
sn:String --> "GBPquote"


*** client accepts proxy to wrong service at trusted server
search [1] icf-aa =>+ 
   ( cf:Configuration 
    < JC : JVM | jcatts:AttributeSet,
      { cocf:Configuration
        < O:Oid : cl:Cid | svc(S:Oid), oatts:AttributeSet >
       msg(JC . app, JC . csptk, findServiceOk(sn:String, O:Oid))
      } >
    < JS : JVM | jsatts:AttributeSet,
     {  socf:Configuration
       < S:Oid : spc:Cid |  sname(ssn:String), satts:AttributeSet >
      } > 
    )
   such that (ssn:String =/= sn:String) .

Solution 1 (state 1390)
states: 1391  rewrites: 15805 in 2480ms cpu (2486ms real) (6372
    rewrites/second)
cf:Configuration --> 
< eee : Transmitter | inQ(none),outQ(none) > 
< JL : JVM | oCtr(0),
 {
< JL . AttackSvc : SVC | state(attackData) > 
< JL . ssptk : SSPTK1 | idle,lookup(JL . lup) > 
< JL . csptk : CSPTK0 | idle,clientId(fakeId),lookup(JL . lup) > 
< JL . lup : AttackerLookup | svcSet(proxyD(CSP1, svc(JS . o(0)))),mySvcSet(
    none),attackeeSet(proxyD(CSP1, svc(JS . o(0)))),myCPTK(JL . csptk),mySPTK(
    JL . ssptk) > 
msg(JL . ssptk, JL . fred, spRegisterReq("Attack", JL . AttackSvc)) 
msg(JS . ssptk, JL . lup, registerReply)},ether(eee) >
jsatts:AttributeSet --> oCtr(1),ether(eee)
socf:Configuration --> 
< JS . GBPsvc : SVC | state(GBPdata) > 
< JS . USsvc : SVC | state(USdata) > 
< JS . ssptk : SSPTK1 | lookup(JL . lup),waitfor(JL . lup, JS . fred,
    spRegisterReq("USquote", JS . USsvc)) > 
msg(JS . ssptk, JS . fred, spRegisterReq("GBPquote", JS . GBPsvc))
S:Oid --> JS . o(0)
spc:Cid --> SSP1
satts:AttributeSet --> idle,svc(JS . USsvc)
ssn:String --> "USquote"
jcatts:AttributeSet --> oCtr(1),ether(eee)
cocf:Configuration --> 
< JC . csptk : CSPTK0 | idle,clientId("sam"),lookup(JL . lup) > 
< JC . app : APP | waitfor(JC . csptk),svcFound(none),mytk(JC . csptk),todo(
    task("GBPquote", mycall)),done(none) >
O:Oid --> JC . o(0)
cl:Cid --> CSP1
oatts:AttributeSet --> idle,clientId("sam")
sn:String --> "GBPquote"


*** client accepts proxy to wrong service at trusted server -- alternative
search [1] icf-aa =>+ 
   ( cf:Configuration 
    < JC : JVM | jcatts:AttributeSet,
      { cocf:Configuration
        < O:Oid : cl:Cid | svc(S:Oid), oatts:AttributeSet >
        < (JC . app) : APP | catts:AttributeSet,
                             todo(task(sn:String, cd:Data) ts:Tasks),
                             waitfor(sid:Oid)  >
          msg(JC . app, sid:Oid, findServiceOk(sn:String, O:Oid))
      } >
    < JS : JVM | jsatts:AttributeSet,
     {  socf:Configuration
       < S:Oid : spc:Cid |  sname(ssn:String), satts:AttributeSet >
      } > 
    )
   such that (ssn:String =/= sn:String) .

Solution 1 (state 1390)
states: 1391  rewrites: 15805 in 2470ms cpu (2476ms real) (6398
    rewrites/second)
cf:Configuration --> 
< eee : Transmitter | inQ(none),outQ(none) > 
< JL : JVM | oCtr(0),
 {
< JL . AttackSvc : SVC | state(attackData) > 
< JL . ssptk : SSPTK1 | idle,lookup(JL . lup) > 
< JL . csptk : CSPTK0 | idle,clientId(fakeId),lookup(JL . lup) > 
< JL . lup : AttackerLookup | svcSet(proxyD(CSP1, svc(JS . o(0)))),mySvcSet(
    none),attackeeSet(proxyD(CSP1, svc(JS . o(0)))),myCPTK(JL . csptk),mySPTK(
    JL . ssptk) > 
msg(JL . ssptk, JL . fred, spRegisterReq("Attack", JL . AttackSvc)) 
msg(JS . ssptk, JL . lup, registerReply)},ether(eee) >
jsatts:AttributeSet --> oCtr(1),ether(eee)
socf:Configuration --> 
< JS . GBPsvc : SVC | state(GBPdata) > 
< JS . USsvc : SVC | state(USdata) > 
< JS . ssptk : SSPTK1 | lookup(JL . lup),waitfor(JL . lup, JS . fred,
    spRegisterReq("USquote", JS . USsvc)) > 
msg(JS . ssptk, JS . fred, spRegisterReq("GBPquote", JS . GBPsvc))
S:Oid --> JS . o(0)
spc:Cid --> SSP1
satts:AttributeSet --> idle,svc(JS . USsvc)
ssn:String --> "USquote"
jcatts:AttributeSet --> oCtr(1),ether(eee)
cocf:Configuration --> 
< JC . csptk : CSPTK0 | idle,clientId("sam"),lookup(JL . lup) >
O:Oid --> JC . o(0)
cl:Cid --> CSP1
oatts:AttributeSet --> idle,clientId("sam")
catts:AttributeSet --> svcFound(none),mytk(JC . csptk),done(none)
sid:Oid --> JC . csptk
sn:String --> "GBPquote"
cd:Data --> mycall
ts:Tasks --> (none).Tasks

*** svc integrity violated
search [1] icf-a =>+ 
   ( cf:Configuration
    < JS : JVM | jsatts:AttributeSet,
     {  locf:Configuration < svc:Oid : SVC | state(sd:Data) > }
     > 
   )
    such that hasUpdate(sd:Data,fakeCall, fakeId)  .

Solution 1 (state 1247)
states: 1248  rewrites: 16943 in 2010ms cpu (2012ms real) (8429
    rewrites/second)
cf:Configuration --> 
< eee : Transmitter | inQ(none),outQ(none) > 
< JL : JVM | oCtr(1),
 {
< JL . AttackSvc : SVC | state(attackData) > 
< JL . ssptk : SSPTK1 | idle,lookup(JL . lup) > 
< JL . csptk : CSPTK0 | idle,clientId(fakeId),lookup(JL . lup) > 
< JL . app : APP | waitfor(JL . o(0)),svcFound(b("GBPquote", JL . o(0))),mytk(
    JL . csptk),todo(task("GBPquote", fakeCall)),done(none) > 
< JL . lup : AttackerLookup | svcSet(proxyD(CSP1, svc(JS . o(0)))),mySvcSet(
    none),attackeeSet(none),myCPTK(JL . csptk),mySPTK(JL . ssptk) > 
< JL . o(0) : CSP1 | svc(JS . o(0)),clientId(fakeId),waitfor(JS . o(0), JL .
    app, svcReq(fakeCall)) > 
msg(JL . ssptk, JL . fred, spRegisterReq("Attack", JL . AttackSvc)) 
msg(JS . ssptk, JL . lup, registerReply)},ether(eee) >
jsatts:AttributeSet --> oCtr(1),ether(eee)
locf:Configuration --> 
< JS . USsvc : SVC | state(USdata) > 
< JS . ssptk : SSPTK1 | lookup(JL . lup),waitfor(JL . lup, JS . fred,
    spRegisterReq("GBPquote", JS . GBPsvc)) > 
< JS . o(0) : SSP1 | svc(JS . GBPsvc),sname("GBPquote"),waitfor(JS . GBPsvc, JL
    . o(0), svcReq(fakeCall)) > 
msg(JS . ssptk, JS . fred, spRegisterReq("USquote", JS . USsvc)) 
msg(JS . o(0), JS . GBPsvc, svcReply(reply(GBPdata, fakeCall, fakeId)))
svc:Oid --> JS . GBPsvc
sd:Data --> update(GBPdata, fakeCall, fakeId)