Verification and enforcement of state-based notions of opacity in discrete event systems

Motivated by security and privacy considerations in applications of discrete event systems, we describe and analyze the complexity of verifying various state-based notions of opacity in systems that are modeled as (possibly non-deterministic) finite automata with partial observation on their transitions. Assuming that the intruder observes system activity through some projection map and has complete knowledge of the system model, we define three notions of opacity with respect to a set of secret states: (i) initial-state opacity is a notion that requires the membership of the system true initial state to the set of secret states remain opaque (i.e., uncertain) to the intruder; (ii) K-step opacity is a notion that requires that at any specific point in time within the last K observations, the entrance of the system state to the given set of secret states remain opaque to the intruder; (iii) infinite-step opacity is a notion that requires the entrance of the system state at any particular instant to the set of secret states remain opaque, for the length of the system operation, to the intruder. As illustrated via examples in the thesis, the above state-based notions of opacity can be used to characterize the security requirements in many applications, including encryption using pseudo-random generators, coverage properties in sensor networks, and anonymity requirements in protocols for web transactions.;In order to model the intruder capabilities regarding initial-state opacity, we address the initial-state estimation problem in a non-deterministic finite automaton under partial observations on its transitions 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 (i.e., it does not change over time). We also establish that the verification of initial-state opacity is a PSPACE-complete problem.;In order to verify K-step opacity, we introduce the K-delay state estimator which constructs the estimate of the state of the system K observations ago (K-delayed state estimates) for a given non-deterministic finite automaton under partial observation on its transitions. We provide two methods for constructing K-delay state estimators, and hence two methods for verifying K-step opacity, and analyze the computational complexity of both. In the process, we also establish that the verification of K-step opacity is an NP-hard problem. We also investigate the role of the delay K in K-step opacity and show that there exists a delay K* such that K-step opacity implies K'-step opacity for any K and K' such that K' > K ≥ K*. This is not true for arbitrary K' > K though the converse holds trivially.;Infinite-step opacity can be verified via the construction of a current-state estimator and a bank of appropriate initial-state estimators. The verification of infinite-step opacity is also shown to be a PSPACE-hard problem.;Finally, we tackle the problem of constructing a minimally restrictive opacity-enforcing supervisor (MOES) which limits the system's behavior within some pre-specified legal behavior while enforcing opacity requirements. We characterize the solution to MOES, under some mild assumptions, in terms of the supremal element of certain controllable, normal, and opaque languages. We also show that this supremal element always exists and that it can be implemented using state estimators. The result is a supervisor that achieves conformance to the pre-specified legal behavior while enforcing opacity by disabling, at any given time, a subset of the controllable system events, in a way that minimally restricts the range of allowable system behavior.