Verification of infinite-step opacity and complexity considerations
Hadjicostis, Christoforos N.
SourceIEEE Transactions on Automatic Control
Google Scholar check
MetadataShow full item record
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. © 2012 IEEE.