DocumentCode :
1363142
Title :
Verification of Infinite-Step Opacity and Complexity Considerations
Author :
Saboori, Anooshiravan ; Hadjicostis, Christoforos N.
Author_Institution :
Dept. of Electr. & Comput. Eng., Univ. of Illinois at Urbana-Champaign, Champaign, IL, USA
Volume :
57
Issue :
5
fYear :
2012
fDate :
5/1/2012 12:00:00 AM
Firstpage :
1265
Lastpage :
1269
Abstract :
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.
Keywords :
computational complexity; cryptography; finite automata; formal verification; state estimation; PSPACE-hard problem; Web transactions; anonymity requirements; complexity considerations; coverage properties; encryption; infinite-step opacity verification; initial state estimators; nondeterministic finite automata; partial observation; projection map; pseudo-random generators; security requirements; sensor networks; Automata; Complexity theory; Educational institutions; Observers; Security; Zinc; Discrete event systems (DES);
fLanguage :
English
Journal_Title :
Automatic Control, IEEE Transactions on
Publisher :
ieee
ISSN :
0018-9286
Type :
jour
DOI :
10.1109/TAC.2011.2173774
Filename :
6062385
Link To Document :
بازگشت