Decentralized Opacity Enforcement in Discrete Event Systems Using Supervisory Control

Current-state opacity is a key security property in discrete event systems. A system is said to be current-state opaque if the intruder, who only has partial observation on the system's evolution, is never able to establish if the current state of the system is within a set of secret states. This paper addresses the problem of enforcing decentralized current state opacity using supervisory control. In particular, it is assumed that there are multiple intruders trying to determine if the current state is in the secret. Given a system that is not decentralized current-state opaque, based on the notion of augmented I-observer, we propose a modular supervisory synthesis method to design a set of supervisors to enforce opacity.