Verification of initial-state opacity in security applications of DES

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.