Verification of Infinite-Step Opacity and Complexity Considerations

We describe and analyze the complexity of verifying the notion of infinite-step opacity in systems that are modeled as non-deterministic finite automata with partial observation on their transitions. Specifically, a system is infinite-step opaque if the entrance of the system state, at any particular instant, to a set of secret states remains opaque (uncertain), for the length of the system operation, to an intruder who observes system activity through some projection map. Infinite-step opacity can be used to characterize the security requirements in many applications, including encryption using pseudo-random generators, coverage properties in sensor networks, and anonymity requirements in protocols for web transactions. We show that infinite-step opacity can be verified via the construction of a set of appropriate initial state estimators and provide illustrative examples. We also establish that the verification of infinite-step opacity is a PSPACE-hard problem.