K-Step Opacity in Discrete Event Systems: Verification, Complexity, and Relations
This work addresses security verification for systems with passive observers, offering incremental improvements in algorithm efficiency for a specific domain.
The paper tackles the problem of verifying K-step opacity in discrete event systems, which determines if an intruder can infer secret states within the last K observable steps, and presents a new algorithm with lower complexity independent of K.
Opacity is a property expressing whether a system may reveal its secret to a passive observer (an intruder) who knows the structure of the system but has a limited observation of its behavior. Several notions of opacity have been studied, including current-state opacity, K-step opacity, and infinite-step opacity. We study K-step opacity that generalizes both current-state opacity and infinite-step opacity, and asks whether the intruder cannot decide, at any time, whether or when the system was in a secret state during the last K observable steps. We design a new algorithm deciding K-step opacity the complexity of which is lower than that of existing algorithms and that does not depend on K. We then compare K-step opacity with other opacity notions and provide new transformations among the notions that do not use states that are neither secret nor non-secret (neutral states) and that are polynomial with respect to both the size of the system and the binary encoding of K.