\input zb-basic \input zb-ioport \iteman{io-port 06067923} \itemau{McEvoy, Thomas Richard; Wolthusen, Stephen D.} \itemti{A formal adversary capability model for SCADA environments.} \itemso{Xenakis, Christos (ed.) et al., Critical information infrastructures security. 5th international workshop, CRITIS 2010, Athens, Greece, September 23--24, 2010. Revised papers. Berlin: Springer (ISBN 978-3-642-21693-0/pbk). Lecture Notes in Computer Science 6712, 93-103 (2011).} \itemab Summary: Conventional adversary models used in the analysis of cryptographic protocols such as the Dolev-Yao model and variants rely on a simple communication model in which an adversary fully participates in network communication. In the case of control (supervisory control and data acquisition, SCADA) systems, this set of assumptions can lead to undesirable results as constraints on communication affect both defender and adversary capabilities. These include a restricted topology for message passing and real-time processing constraints resulting in message prioritisation. We therefore propose an alternative adversary model explicitly capturing these constraints. We use a $\pi $-calculus variant to reason about priorities and constraints on messages (names) and explicitly model multiple adversarial agents rather than a single omnipotent adversary so as to capture synchronisation and communication effects. As an example of the model's capabilities, we derive targets for intrusion detection based on constraints on adversary action resulting from adversary-agent communication capabilities. \itemrv{~} \itemcc{} \itemut{} \itemli{doi:10.1007/978-3-642-21694-7\_8} \end