Notions of security and opacity in discrete event systems

In this paper, we follow a state-based approach to extend the notion of opacity in computer security to discrete event systems. A system is (S, P)-opaque if the evolution of its true state through a set of secret states S remains opaque to an observer who is observing activity in the system through the projection map P. In other words, based on observations through the mapping P, the observer is never certain that the current state of the system is within the set of secret states S. We also introduce the stronger notion of (S, P, K)-opacity which requires opacity to remain true for K observations following the departure of the system's state from the set S. We show that the state-based definition of opacity enables the use of observer constructions for verification purposes. In particular, the verification of (S, P, K)-opacity is accomplished via an observer with K-delay which is constructed to capture state estimates with K-delay. These are the estimates of the state of the system K observations ago and are consistent with all observations (including the last K observations). We also analyze the properties and complexity of the observer with K-delay.