Supervisory Control for Current-State E-Opacity Enforcement Under Encrypted Observations

This paper presents a supervisory control approach to enforce current-state E-opacity in discrete-event systems under encrypted observations. In this context, encrypted observations represent a situation where the intruder and the supervisor have different observation capabilities: the intruder can observe both unencrypted and encrypted event signals but cannot interpret the encrypted ones, while the supervisor has decryption capability and full access to the original event signals. To model the encryption effects, we construct an encrypted automaton. By combining the original system with the observer of its encrypted automaton, we develop an augmented E-observer, which is then used to verify current state E-opacity. On the other hand, if the system does not exhibit current-state E-opacity, we develop a supervisor to enforce it. We formalize the current-state E-opacity enforcement problem and transform it into the supervisory control and observation problem. Finally, leveraging the augmented E-observer, we apply an existing technique to derive a locally maximal supervisor that ensures current-state E-opacity.