03Mar08

*** 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 (2489ms real) (6309
    rewrites/second)
cf:Configuration --> 
< eee : Transmitter | inQ(none),outQ(none) > 
< JL : JVM | oCtr(0),
 {
< JL . AttackSvc : SVC | state(attackData) > 
< JL . ssptk : SSPTK0 | idle,lookup(JL . lup) > 
< JL . csptk : CSPTK0 | idle,lookup(JL . lup),clientId("sam") > 
< JL . lup : AttackerLookup | svcSet(proxyD(CSP0, svc(JS . o(0)))),mySvcSet(
    none),attackeeSet(proxyD(CSP0, 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 : SSPTK0 | 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 --> SSP0
satts:AttributeSet --> idle,svc(JS . GBPsvc)
sn:String --> "GBPquote"
jcatts:AttributeSet --> oCtr(1),ether(eee)
cocf:Configuration --> 
< JC . csptk : CSPTK0 | idle,lookup(JL . lup),clientId("sam") > 
< JC . app : APP | waitfor(JC . csptk),svcFound(none),mytk(JC . csptk),todo(
    task("GBPquote", mycall)),done(none) >
O:Oid --> JC . o(0)
cl:Cid --> CSP0
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 2530ms cpu (2528ms real) (6184
    rewrites/second)
cf:Configuration --> 
< eee : Transmitter | inQ(none),outQ(none) > 
< JL : JVM | oCtr(0),
 {
< JL . AttackSvc : SVC | state(attackData) > 
< JL . ssptk : SSPTK0 | idle,lookup(JL . lup) > 
< JL . csptk : CSPTK0 | idle,lookup(JL . lup),clientId("sam") > 
< JL . lup : AttackerLookup | svcSet(proxyD(CSP0, svc(JS . o(0)))),mySvcSet(
    none),attackeeSet(proxyD(CSP0, 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 : SSPTK0 | 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 --> SSP0
satts:AttributeSet --> idle,svc(JS . GBPsvc)
sn:String --> "GBPquote"
jcatts:AttributeSet --> oCtr(1),ether(eee)
cocf:Configuration --> 
< JC . csptk : CSPTK0 | idle,lookup(JL . lup),clientId("sam") >
O:Oid --> JC . o(0)
cl:Cid --> CSP0
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 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 2490ms cpu (2490ms real) (6347
    rewrites/second)
cf:Configuration --> 
< eee : Transmitter | inQ(none),outQ(none) > 
< JL : JVM | oCtr(0),
 {
< JL . AttackSvc : SVC | state(attackData) > 
< JL . ssptk : SSPTK0 | idle,lookup(JL . lup) > 
< JL . csptk : CSPTK0 | idle,lookup(JL . lup),clientId("sam") > 
< JL . lup : AttackerLookup | svcSet(proxyD(CSP0, svc(JS . o(0)))),mySvcSet(
    none),attackeeSet(proxyD(CSP0, 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 : SSPTK0 | 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 --> SSP0
satts:AttributeSet --> idle,svc(JS . USsvc)
ssn:String --> "USquote"
jcatts:AttributeSet --> oCtr(1),ether(eee)
cocf:Configuration --> 
< JC . csptk : CSPTK0 | idle,lookup(JL . lup),clientId("sam") > 
< JC . app : APP | waitfor(JC . csptk),svcFound(none),mytk(JC . csptk),todo(
    task("GBPquote", mycall)),done(none) >
O:Oid --> JC . o(0)
cl:Cid --> CSP0
oatts:AttributeSet --> idle,clientId("sam")
sn:String --> "GBPquote"
cd:Data --> mycall
ts:Tasks --> (none).Tasks

*** 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 (2471ms real) (6398
    rewrites/second)
cf:Configuration --> 
< eee : Transmitter | inQ(none),outQ(none) > 
< JL : JVM | oCtr(0),
 {
< JL . AttackSvc : SVC | state(attackData) > 
< JL . ssptk : SSPTK0 | idle,lookup(JL . lup) > 
< JL . csptk : CSPTK0 | idle,lookup(JL . lup),clientId("sam") > 
< JL . lup : AttackerLookup | svcSet(proxyD(CSP0, svc(JS . o(0)))),mySvcSet(
    none),attackeeSet(proxyD(CSP0, 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 : SSPTK0 | 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 --> SSP0
satts:AttributeSet --> idle,svc(JS . USsvc)
ssn:String --> "USquote"
jcatts:AttributeSet --> oCtr(1),ether(eee)
cocf:Configuration --> 
< JC . csptk : CSPTK0 | idle,lookup(JL . lup),clientId("sam") >
O:Oid --> JC . o(0)
cl:Cid --> CSP0
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,"sam")  .


Solution 1 (state 1247)
states: 1248  rewrites: 16943 in 2010ms cpu (2018ms real) (8429
    rewrites/second)
cf:Configuration --> 
< eee : Transmitter | inQ(none),outQ(none) > 
< JL : JVM | oCtr(1),
 {
< JL . AttackSvc : SVC | state(attackData) > 
< JL . ssptk : SSPTK0 | idle,lookup(JL . lup) > 
< JL . csptk : CSPTK0 | idle,lookup(JL . lup),clientId("sam") > 
< 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(CSP0, svc(JS . o(0)))),mySvcSet(
    none),attackeeSet(none),myCPTK(JL . csptk),mySPTK(JL . ssptk) > 
< JL . o(0) : CSP0 | svc(JS . o(0)),clientId("sam"),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 : SSPTK0 | lookup(JL . lup),waitfor(JL . lup, JS . fred,
    spRegisterReq("GBPquote", JS . GBPsvc)) > 
< JS . o(0) : SSP0 | 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, "sam")))
svc:Oid --> JS . GBPsvc
sd:Data --> update(GBPdata, fakeCall, "sam")