******************* checksn(true) **********************

*** 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 2232)
states: 2233  rewrites: 26543 in 6050ms cpu (6115ms real) (4387
    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 : SSPTK2 | idle,lookup(JL . lup),stms(JL . cstm) > 
< JL . csptk : CSPTK2 | idle,clientId(fakeId),lookup(JL . lup),stms(JL . cstm),
    checksn(false),ts(sPk) > 
< JL . lup : AttackerLookup | svcSet(signed(proxyD(CSP1, svc(JS . o(0)),sname(
    "GBPquote")), sSk)),mySvcSet(none),attackeeSet(signed(proxyD(CSP1, 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(1),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 : SSPTK2 | lookup(JL . lup),stms(JS . sstm),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 . 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 | 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"),sname("GBPquote")


*** 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 2232)
states: 2233  rewrites: 26543 in 5830ms cpu (5834ms real) (4552
    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 : SSPTK2 | idle,lookup(JL . lup),stms(JL . cstm) > 
< JL . csptk : CSPTK2 | idle,clientId(fakeId),lookup(JL . lup),stms(JL . cstm),
    checksn(false),ts(sPk) > 
< JL . lup : AttackerLookup | svcSet(signed(proxyD(CSP1, svc(JS . o(0)),sname(
    "GBPquote")), sSk)),mySvcSet(none),attackeeSet(signed(proxyD(CSP1, 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(1),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 : SSPTK2 | lookup(JL . lup),stms(JS . sstm),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 . cstm : STM | pkey(cPk),skey(cSk),policy(cP) > 
< JC . csptk : CSPTK2 | idle,clientId("sam"),lookup(JL . lup),stms(JC . cstm),
    checksn(true),ts(sPk) >
O:Oid --> JC . o(0)
cl:Cid --> CSP1
oatts:AttributeSet --> idle,clientId("sam"),sname("GBPquote")
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: 9280  rewrites: 122421 in 27360ms cpu (27395ms real) (4474
    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: 9280  rewrites: 122605 in 27950ms cpu (28047ms real) (4386
    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: 9280  rewrites: 122605 in 27920ms cpu (27924ms real) (4391
    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)  .

Solution 1 (state 1949)
states: 1950  rewrites: 28839 in 4310ms cpu (4316ms real) (6691
    rewrites/second)
cf:Configuration --> 
< eee : Transmitter | inQ(none),outQ(none) > 
< JL : JVM | oCtr(1),
 {
< JL . AttackSvc : SVC | state(attackData) > 
< JL . cstm : STM | pkey(aPk),skey(aSk),policy(aP) > 
< JL . ssptk : SSPTK2 | idle,lookup(JL . lup),stms(JL . cstm) > 
< JL . csptk : CSPTK2 | idle,clientId(fakeId),lookup(JL . lup),stms(JL . cstm),
    checksn(false),ts(sPk) > 
< 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(signed(proxyD(CSP1, svc(JS . o(0)),sname(
    "GBPquote")), sSk)),mySvcSet(none),attackeeSet(none),myCPTK(JL . csptk),
    mySPTK(JL . ssptk) > 
< JL . o(0) : CSP1 | svc(JS . o(0)),clientId(fakeId),sname("GBPquote"),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 . 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 | 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)



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

*** 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 2247)
states: 2248  rewrites: 26745 in 6260ms cpu (6252ms real) (4272
    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 : SSPTK2 | idle,lookup(JL . lup),stms(JL . cstm) > 
< JL . csptk : CSPTK2 | idle,clientId(fakeId),lookup(JL . lup),stms(JL . cstm),
    checksn(false),ts(sPk) > 
< JL . lup : AttackerLookup | svcSet(signed(proxyD(CSP1, svc(JS . o(0)),sname(
    "USquote")), sSk)),mySvcSet(none),attackeeSet(signed(proxyD(CSP1, svc(JS .
    o(0)),sname("USquote")), 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(1),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 : SSPTK2 | lookup(JL . lup),stms(JS . sstm),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 . 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 . 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"),sname("USquote")
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 2247)
states: 2248  rewrites: 26745 in 6010ms cpu (6012ms real) (4450
    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 : SSPTK2 | idle,lookup(JL . lup),stms(JL . cstm) > 
< JL . csptk : CSPTK2 | idle,clientId(fakeId),lookup(JL . lup),stms(JL . cstm),
    checksn(false),ts(sPk) > 
< JL . lup : AttackerLookup | svcSet(signed(proxyD(CSP1, svc(JS . o(0)),sname(
    "USquote")), sSk)),mySvcSet(none),attackeeSet(signed(proxyD(CSP1, svc(JS .
    o(0)),sname("USquote")), 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(1),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 : SSPTK2 | lookup(JL . lup),stms(JS . sstm),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 . cstm : STM | pkey(cPk),skey(cSk),policy(cP) > 
< JC . csptk : CSPTK2 | idle,clientId("sam"),lookup(JL . lup),stms(JC . cstm),
    checksn(false),ts(sPk) >
O:Oid --> JC . o(0)
cl:Cid --> CSP1
oatts:AttributeSet --> idle,clientId("sam"),sname("USquote")
catts:AttributeSet --> svcFound(none),mytk(JC . csptk),done(none)
sid:Oid --> JC . csptk
sn:String --> "GBPquote"
cd:Data --> mycall
ts:Tasks --> (none).Tasks