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