Verification of initial-state opacity in security applications of DES
Date
2008ISBN
978-1-4244-2592-1Source
Proceedings - 9th International Workshop on Discrete Event Systems, WODES' 08Proceedings - 9th International Workshop on Discrete Event Systems, WODES' 08
Pages
328-333Google Scholar check
Keyword(s):
Metadata
Show full item recordAbstract
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 event systems. Specifically, a system is initial-state opaque if the membership of its true initial state to a set of secret states remains opaque to an intruder who is modeled as an observer of the system activity through some projection map. In other words, based on observations through this map, the observer is never certain that the initial state of the system is within the set of secret states. To verify initial-state opacity, we address the initial-state estimation problem in discrete event systems via the construction of an initial-state estimator. This estimator captures estimates of the initial state of the system which are consistent with all observations obtained so far. We also analyze the properties and complexity of the initial-state estimator. ©2008 IEEE.