Opacity-Enforcing Supervisory Strategies for Secure Discrete Event Systems

Initial-state opacity emerges as a key property in numerous security applications of discrete event systems including key-stream generators for cryptographic protocols. Specifically, a system is initial-state opaque if the membership of its true initial state to a set of secret states remains uncertain (opaque) to an outside intruder who observes system activity through a given projection map. In this paper, we consider 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 the initial-state opacity requirement. To tackle this problem, we extend the state-based definition of initial-state opacity to languages and characterize the solution to MOES in terms of the supremal element of certain controllable, observable and opaque languages. We also derive conditions under which this supremal element exists and show how the initial-state estimator, which was introduced in our earlier work for verifying initial-state opacity, can be used to implement the solution to MOES.