Synthesis of State-Attack Strategies for Anonymity and Opacity Violation in Discrete Event Systems

TL;DR

This paper develops methods to synthesize attack strategies that can violate anonymity and opacity in nondeterministic finite automata-based discrete event systems, analyzing their complexity and providing illustrative examples.

Contribution

It introduces a systematic approach for designing state attack strategies that ensure violation of anonymity and opacity in discrete event systems.

Findings

Algorithms for verifying anonymity and opacity violations.

Strategies for guaranteed violation of system secrecy.

Complexity analysis of attack synthesis methods.

Abstract

Attacks, including the manipulation of sensor readings and the modification of actuator commands, pose a significant challenge to the security and privacy of automated systems. This paper considers discrete event systems that can be modeled with nondeterministic finite state automata that are susceptible to state attacks. A state attack allows an intruder to learn whether or not the current state of a system falls into certain subsets of states. The intruder has a limited total number of state attacks at its disposal, but can launch state attacks at arbitrary instants of its choosing. We are interested on violations of current-state anonymity (resp. opacity), i.e., situations where the intruder, based on the sequence of observations generated by the system and the outcome of any performed state attacks, can ascertain the exact current state of the system (resp. that the current state of the system definitely resides in a subset of secret states). When the system violates current-state anonymity (resp. opacity) under a bounded number of state attacks, a subsequent question is whether the intruder can design an attack strategy such that anonymity-violating (resp. opacity-violating) situations will always be reached. In this latter case, we also design an attack strategy that guarantees that the system will reach a violating situation regardless of system actions. We provide pertinent complexity analysis of the corresponding verification algorithms and examples to illustrate the proposed methods.