*** all-lookup.m

mod TEST-LOOKUP is
  inc TEST .
  inc ATTACKER-LOOKUP .


*** eq acptkobs = 
***   < (JL . csptk) : CSPTK0 | lookup(JL . lup), clientId(fakeId), idle >

  eq aljcf = 
    < JL : JVM | oCtr(0),  ether(eee), 
     {  acptkobs
       < (JL . app) : APP |  svcFound(none), mytk(JL . csptk),
                            todo(task("GBPquote",fakeCall)), done(none), idle >
       < (JL .  lup) : AttackerLookup | myCPTK(JL . csptk), mySPTK(JL . ssptk),
                             mySvcSet(none), svcSet(none), attackeeSet(none) >
       < (JL . AttackSvc) : SVC | state(attackData) >
      } > 
  .

  eq aljcf0 = 
    < JL : JVM | oCtr(0),  ether(eee), 
     {  acptkobs
       < (JL .  lup) : AttackerLookup | myCPTK(JL . csptk), mySPTK(JL . ssptk),
                             mySvcSet(none), svcSet(none), attackeeSet(none) >
       < (JL . AttackSvc) : SVC | state(attackData) >
      } > 
  .


*** test configurations 

  ops icf icf-a icf-aa icf1 icf2 : -> Configuration .
  eq icf =  eecf aljcf sjcf cjcf .
  eq icf-a =  eecf aljcf sjcf .
  eq icf-aa =  eecf aljcf0 sjcf cjcf1 .
  eq icf1 =  eecf aljcf sjcf cjcf1 .
  eq icf2 =  eecf aljcf sjcf cjcf2 .


  op hasUpdate : Data Data String -> Bool .
  eq hasUpdate(update(sd:Data,call:Data,cId:String), cd:Data, cn:String) =
       (if (call:Data == cd:Data and cn:String == cId:String)
        then true
        else hasUpdate(sd:Data,cd:Data,cn:String) 
        fi )
  .

  eq hasUpdate(sd:Data,cd:Data,cn:String) = false [owise] .

endm


***( Patterns

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

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

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

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

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


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

)

