Verification of K-Step Opacity and Analysis of Its Complexity

Motivated by security and privacy considerations in a variety of applications of discrete event systems, we describe and analyze the computational complexity required for verifying the notion of K-step opacity for systems that are modeled as nondeterministic finite automata with partial observation on their transitions. Specifically, a system is K-step opaque if, at any specific point within the last observations, the entrance of the system state to a given set of secret states remains opaque (uncertain) to an intruder who has complete knowledge of the system model and observes system activity through some natural projection map. We provide two methods for verifying K-step opacity using two different state estimator constructions, and analyze the computational complexity of both. Note to Practitioners-In many emerging security applications, there exists a need to guarantee that important information regarding a given system remains secret to outsiders, at least for a limited period of time. The notion of K-step opacity that we introduce and analyze in this paper is appropriate for the security analysis of a system that can be modeled as a partially observed and possibly nondeterministic finite automaton. The important information that is to be kept secret is captured by a subset of the system states. Potential applications include the analysis of security requirements when encrypting using pseudorandom generators, the analysis of tracking limitations of mobile agents in a certain terrain with a given sensor coverage, and the analysis of anonymity guarantees in protocols for web transactions.