Verification of initial-state opacity in security applications of discrete event systems
Ημερομηνία
2013Source
Information SciencesVolume
246Issue
Journal ArticlePages
115-132Google Scholar check
Keyword(s):
Metadata
Εμφάνιση πλήρους εγγραφήςΕπιτομή
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. © 2013 Elsevier Inc. All rights reserved.
Collections
Cite as
Related items
Showing items related by title, author, creator and subject.
-
Conference Object
Consensus Approach to Secure State Estimation for a Class of Remotely Sensed Networked Systems
Tsiakkas, Mihalis; Nicolaou, Nicolas; Polycarpou, Marios; Panayiotou, Christos (2018)Remote sensing is often a crucial part of cyber-physical and networked systems. Measurements taken at remote locations can both serve as monitoring tools as well as to inform control decisions. Over the past few years, a ...
-
Conference Object
Verification of initial-state opacity in security applications of DES
Saboori, A.; Hadjicostis, Christoforos N. (2008)Motivated by security applications where the initial state of a system needs to be kept secret (opaque) to outside observers (intruders), we formulate, analyze and verify the notion of initial-state opacity in discrete ...
-
Conference Object
Resolution of initial-state in security applications of des
Hadjicostis, Christoforos N. (2012)A non-deterministic labeled finite automaton is initial-state opaque if the membership of its true initial state to a set of secret states S remains opaque (i.e., uncertain) to an intruder who observes system activity ...