Journal
INFORMATION SCIENCES
Volume 246, Issue -, Pages 115-132Publisher
ELSEVIER SCIENCE INC
DOI: 10.1016/j.ins.2013.05.033
Keywords
Discrete event system; Formal methods in security analysis; Initial state estimation; Initial state estimator; Tracking in sensor network
Categories
Funding
- U.S. National Science Foundation under NSF ITR [0426831]
- U.S. National Science Foundation under NSF CNS [0834409]
- European Commission [INFSO-ICT-223844, PIRG02-GA-2007-224877]
- Div Of Electrical, Commun & Cyber Sys
- Directorate For Engineering [0426831] Funding Source: National Science Foundation
Ask authors/readers for more resources
In this paper, we formulate and analyze methodologies for verifying the notion of initial-state opacity in discrete event systems that are modeled as non-deterministic finite automata with partial observation on their transitions. A system is initial-state opaque if the membership of its true initial state to a set of secret states remains opaque (i.e., uncertain) to an intruder who observes system activity through some projection map. Initial-state opacity can be used to characterize security requirements in a variety of applications, including tracking problems in sensor networks. In order to model and analyze the intruder capabilities regarding initial-state opacity, we first address the initial-state estimation problem in a non-deterministic finite automaton via the construction of an initial-state estimator. We analyze the properties and complexity of the initial-state estimator, and show how the complexity of the verification method can be greatly reduced in the special case when the set of secret states is invariant. We also establish that the verification of initial-state opacity is a PSPACE-.complete problem. (C) 2013 Elsevier Inc. All rights reserved.
Authors
I am an author on this paper
Click your name to claim this paper and add it to your profile.
Reviews
Recommended
No Data Available