A Formal Adversary Capability Model for SCADA Environments

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 π-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.