*** 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 8090)
states: 8091  rewrites: 103216 in 26520ms cpu (26583ms real) (3892
    rewrites/second)
cf:Configuration --> 
< eee : Transmitter | inQ(none),outQ(none) > 
< JL : JVM | oCtr(0),
 {
< JL . AttackSvc : SVC | state(attackData) > 
< JL . cstm : STM | pkey(aPk),skey(aSk),policy(aP) > 
< JL . ssptk : SSPTK3 | idle,stms(JL . cstm),lookup(JL . lup) > 
< JL . csptk : CSPTK3 | idle,stms(JL . cstm),lookup(JL . lup),cred(aCred),ts(
    sPk) > 
< JL . lup : AttackerLookup | svcSet(signed(proxyD(CAP, svc(JS . o(0)),sname(
    "GBPquote")), sSk)),mySvcSet(none),attackeeSet(signed(proxyD(CAP, svc(JS .
    o(0)),sname("GBPquote")), sSk)),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(2),ether(eee)
socf:Configuration --> 
< JS . GBPsvc : SVC | state(GBPdata) > 
< JS . USsvc : SVC | state(USdata) > 
< JS . sstm : STM | pkey(sPk),skey(sSk),policy(sP) > 
< JS . ssptk : SSPTK3 | stms(JS . sstm),lookup(JL . lup),waitfor(JL . lup, JS .
    fred, spRegisterReq("GBPquote", JS . GBPsvc)) > 
< JS . o(0) : SAP | idle,svc(JS . GBPsvc),sname("GBPquote"),stms(JS . sstm) > 
msg(JS . ssptk, JS . fred, spRegisterReq("USquote", JS . USsvc))
S:Oid --> JS . o(1)
spc:Cid --> SSSP
satts:AttributeSet --> idle,svc(JS . GBPsvc),perms(clientPerm("GBPquote",
    myCred, sP))
sn:String --> "GBPquote"
jcatts:AttributeSet --> oCtr(2),ether(eee)
cocf:Configuration --> 
< JC . cstm : STM | pkey(cPk),skey(cSk),policy(cP) > 
< JC . csptk : CSPTK3 | idle,stms(JC . cstm),lookup(JL . lup),cred(myCred),ts(
    sPk) > 
< JC . app : APP | waitfor(JC . csptk),svcFound(none),mytk(JC . csptk),todo(
    task("GBPquote", mycall)),done(none) > 
< JC . o(0) : CAP | idle,svc(JS . o(0)),stms(JC . cstm) >
O:Oid --> JC . o(1)
cl:Cid --> CSSP
oatts:AttributeSet --> idle


*** 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 8090)
states: 8091  rewrites: 103216 in 26430ms cpu (26449ms real) (3905
    rewrites/second)
cf:Configuration --> 
< eee : Transmitter | inQ(none),outQ(none) > 
< JL : JVM | oCtr(0),
 {
< JL . AttackSvc : SVC | state(attackData) > 
< JL . cstm : STM | pkey(aPk),skey(aSk),policy(aP) > 
< JL . ssptk : SSPTK3 | idle,stms(JL . cstm),lookup(JL . lup) > 
< JL . csptk : CSPTK3 | idle,stms(JL . cstm),lookup(JL . lup),cred(aCred),ts(
    sPk) > 
< JL . lup : AttackerLookup | svcSet(signed(proxyD(CAP, svc(JS . o(0)),sname(
    "GBPquote")), sSk)),mySvcSet(none),attackeeSet(signed(proxyD(CAP, svc(JS .
    o(0)),sname("GBPquote")), sSk)),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(2),ether(eee)
socf:Configuration --> 
< JS . GBPsvc : SVC | state(GBPdata) > 
< JS . USsvc : SVC | state(USdata) > 
< JS . sstm : STM | pkey(sPk),skey(sSk),policy(sP) > 
< JS . ssptk : SSPTK3 | stms(JS . sstm),lookup(JL . lup),waitfor(JL . lup, JS .
    fred, spRegisterReq("GBPquote", JS . GBPsvc)) > 
< JS . o(0) : SAP | idle,svc(JS . GBPsvc),sname("GBPquote"),stms(JS . sstm) > 
msg(JS . ssptk, JS . fred, spRegisterReq("USquote", JS . USsvc))
S:Oid --> JS . o(1)
spc:Cid --> SSSP
satts:AttributeSet --> idle,svc(JS . GBPsvc),perms(clientPerm("GBPquote",
    myCred, sP))
sn:String --> "GBPquote"
jcatts:AttributeSet --> oCtr(2),ether(eee)
cocf:Configuration --> 
< JC . cstm : STM | pkey(cPk),skey(cSk),policy(cP) > 
< JC . csptk : CSPTK3 | idle,stms(JC . cstm),lookup(JL . lup),cred(myCred),ts(
    sPk) > 
< JC . o(0) : CAP | idle,svc(JS . o(0)),stms(JC . cstm) >
O:Oid --> JC . o(1)
cl:Cid --> CSSP
oatts:AttributeSet --> idle
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))
      } > 
    )  .

No solution.
states: 15456  rewrites: 201321 in 53410ms cpu (53533ms real) (3769
    rewrites/second)

*** 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) .

No solution.
states: 15456  rewrites: 201601 in 55210ms cpu (55379ms real) (3651
    rewrites/second)

*** 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) .

No solution.
states: 15456  rewrites: 201601 in 54600ms cpu (54648ms real) (3692
    rewrites/second)

*** 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)  .

No solution.
states: 21308  rewrites: 322807 in 65150ms cpu (65175ms real) (4954
    rewrites/second)