
***(
Attacker Lookup and Attacker App and AttackerSvc on Attacker JVM

  ALup is seeded with proxy for AttackerSvc
  upon receiving register request it
        stores the pxd in the lookup db (with the attack pxy)
        puts pxd in the list of attackees
  upon receiving a lookup request
     if from my sptk it replies with the first on list of attackees 
       and removes from that pxd from the list
     ow choses a random pxd from the store and replies
         (actually in non-signing case could always send attack pxy)

  The Attacker node also has a csptk and if needed a tms (with its own cred)
    
  The AttackApp sends findSvc("*") to the csptk -- which will get the
   next registered proxy from the attackLookup, install and return
   a pxy handle.  Now the attack app sends a svc call with fakeCall, fakeId
   as arguments.   These represent arbitrary publicly available arguments.
   the fakeId will not match the attackCred.

)


*** the attacker lookup service
*** used by SSPTK, CSPTK


fmod ATTACKER-LOOKUP-CLASS is
  inc LOOKUP-IFACE .
  inc ATTACKER-AUX .
  ops AttackerLookup : -> Cid .
  ops svcSet mySvcSet attackeeSet : DataSet -> Attribute .
  ops myCPTK mySPTK : Oid -> Attribute .
endfm


mod ATTACKER-LOOKUP is
  inc ATTACKER-LOOKUP-CLASS .

  ops choose : DataSet -> DataX .
  rl[choseD]: choose(d:Data ds:DataSet) => d:Data .
 
  rl[lookup.register]:
    < O:Oid : AttackerLookup | myCPTK(T:Oid), mySPTK(ST:Oid),
            mySvcSet(ds:DataSet), svcSet(ss:DataSet), attackeeSet(as:DataSet) >
    msg(O:Oid, C:Oid, registerReq(sname:String, sp:Data))
    =>
   (if (C:Oid == ST:Oid)
    then
     < O:Oid : AttackerLookup | myCPTK(T:Oid), mySPTK(ST:Oid),
                                mySvcSet(ds:DataSet sp:Data), 
                                svcSet(ss:DataSet), attackeeSet(as:DataSet) >
    else
     < O:Oid : AttackerLookup | myCPTK(T:Oid), mySPTK(ST:Oid),
               mySvcSet(ds:DataSet), 
               svcSet(ss:DataSet  sp:Data), attackeeSet(as:DataSet  sp:Data) >
    fi)
    msg(C:Oid, O:Oid, registerReply) .

  rl[lookup.alookup]:
    < O:Oid : AttackerLookup | myCPTK(T:Oid), mySPTK(ST:Oid), 
                         mySvcSet(ds:DataSet), 
                         svcSet(ss:DataSet), attackeeSet(sp:Data as:DataSet) >
    msg(O:Oid, T:Oid, lookupReq(sname:String))
    =>
    < O:Oid : AttackerLookup | myCPTK(T:Oid), mySPTK(ST:Oid),
                               mySvcSet(ds:DataSet), 
                               svcSet(ss:DataSet), attackeeSet(as:DataSet) >
     msg(T:Oid, O:Oid, lookupOk(sname:String, sp:Data))
  .

  crl[lookup.lookup]:
    < O:Oid : AttackerLookup | myCPTK(T:Oid), mySPTK(ST:Oid),
                               mySvcSet(ds:DataSet), 
                               svcSet(ss:DataSet), attackeeSet(as:DataSet) >
    msg(O:Oid, C:Oid, lookupReq(sname:String))
    =>
    < O:Oid : AttackerLookup | myCPTK(T:Oid), mySPTK(ST:Oid), 
                               mySvcSet(ds:DataSet), 
                               svcSet(ss:DataSet), attackeeSet(as:DataSet) >
     msg(C:Oid, O:Oid, lookupOk(sname:String, sp:Data))
  if C:Oid =/= T:Oid 
  /\ choose(ss:DataSet ds:DataSet) => sp:Data
  .  

endm

