***(
An attacker can
  listen to the communications between proxies and services
    (possibly learning sensitive information)
  actively attack the communication channel
    replace the service proxy with a one of its own choosing
     (malicious one that  tries to damage clients VMs
      learns sensitive information communicated between clients and services
      by impersonating services)
    modify service request or reply data
  impersonate clients when accessing services

This is modelled by modifying the Ether behavior.
An attacking transmitter keeps a set of  client identifiers,
a set client data (from service calls and replies) and a set of
ProxyDescriptions, some known initially, some learned
by collecting data from messages seen.
It  non-deterministically replaces client ids, data and proxy descriptions
in clear messages by those in its store.
)


fmod ATTACKER-CLASS is
  inc ATTACKER-AUX .
  inc LOOKUP-IFACE .           *** attackable messages
  inc ETHER-CLASS .
  inc SVC-CLASS .
  op Attacker : -> EtherCid .
  ops clientIds : StringSet -> Attribute .
  ops clientDs pxDs : DataSet -> Attribute .    *** proxy and client data
endfm

mod ATTACKER is
  inc ATTACKER-CLASS .
  sorts StringX .
  subsort String < StringX .
  op choose : StringSet -> StringX .
  op choose : DataSet -> DataX .

  
  rl[choseQ]: choose(q:String qs:StringSet) => q:String .
  rl[choseD]: choose(d:Data ds:DataSet) => d:Data .
  rl[choseNone]: choose((none).DataSet) => badData .


  rl[attack.registerReq]:
    < A:Oid : Attacker | pxDs(pds:DataSet), 
                         clientIds(ids:StringSet), clientDs(cds:DataSet),
      inQ(deliver(J:Oid, msg(O:Oid, C:Oid, registerReq(sn:String, sp:Data)))
          imc:MConf), 
      outQ(omc:MConf) >
    =>
    < A:Oid : Attacker | pxDs(addElt(sp:Data, pds:DataSet)),
                         clientIds(ids:StringSet), clientDs(cds:DataSet),
                         inQ(imc:MConf), 
          outQ(deliver(loctgt(C:Oid), msg(C:Oid,O:Oid, registerReply))
               omc:MConf) >
    .

  crl[attack.lookupReq]:
    < A:Oid : Attacker | pxDs(pds:DataSet),
                         clientIds(ids:StringSet), clientDs(cds:DataSet),
      inQ(deliver(J:Oid, msg(O:Oid, C:Oid, lookupReq(sn:String))) imc:MConf), 
      outQ(omc:MConf) >
    =>
    < A:Oid : Attacker | pxDs(pds:DataSet),
                         clientIds(ids:StringSet), clientDs(cds:DataSet),
                         inQ(imc:MConf),
       outQ(deliver(loctgt(C:Oid),
                    msg(C:Oid, O:Oid, lookupOk(sn:String, pxd:Data)))
            omc:MConf) >
    if  choose(pds:DataSet) => pxd:Data
  .


  rl[xmit.smsg]:
    < E:Oid : ec:EtherCid | inQ(deliver(J:Oid, smsg(O:Oid, C:Oid, mb:MsgBody)) 
                                imc:MConf), 
                            outQ(omc:MConf), 
                            atts:AttributeSet >
    =>
    < E:Oid : ec:EtherCid | inQ(imc:MConf), 
                            outQ(deliver(J:Oid, smsg(O:Oid, C:Oid, mb:MsgBody))
                                 omc:MConf),
                            atts:AttributeSet >
 .

***  op svcReq : Data -> MsgBody .
***  op svcReply : DataX -> MsgBody .

  crl[attack.svcReq]:
    < A:Oid : Attacker | pxDs(pds:DataSet),
                         clientIds(ids:StringSet), clientDs(cds:DataSet),
       inQ(deliver(J:Oid, msg(C:Oid, O:Oid, svcReq(req:Data,id:String)))
           imc:MConf),
       outQ(omc:MConf) > 
    =>
    < A:Oid : Attacker | pxDs(pds:DataSet),
                         clientIds(addElt(id:String,ids:StringSet)),
                         clientDs(addElt(req:Data, cds:DataSet)),
                         inQ(imc:MConf),
      outQ(deliver(J:Oid, msg(C:Oid,O:Oid,svcReq(d:Data,ii:String)))
           omc:MConf) >
    if  choose(addElt(id:String,ids:StringSet)) => ii:String 
       /\ choose(addElt(req:Data, cds:DataSet)) => d:Data 
  .

  crl[attack.svcReply]:
    < A:Oid : Attacker | pxDs(pds:DataSet),
                         clientIds(ids:StringSet), clientDs(cds:DataSet),
       inQ(deliver(J:Oid, msg(C:Oid, O:Oid, svcReply(dx:DataX)))
           imc:MConf),
       outQ(omc:MConf) > 
    =>
    < A:Oid : Attacker | pxDs(pds:DataSet),
                         clientIds(ids:StringSet),
                         (if (dx:DataX :: Data) 
                          then clientDs(addElt(dx:DataX, cds:DataSet))
                          else clientDs(cds:DataSet) fi),
                         inQ(imc:MConf),
      outQ(deliver(J:Oid, msg(C:Oid,O:Oid,svcReply(d:Data)))
           omc:MConf) >
    if choose(addElt(dx:DataX, cds:DataSet)) => d:Data 
  .


endm

