Verification of Opacity in Networked Supervisory Control Systems with Insecure Control Channels

We investigate security and privacy issues in networked discrete-event systems, where supervisory controllers are connected with actuators and sensors via communication networks. In this paper, we consider the case where the control channel between the supervisor and the actuators may not be secure in the sense that the control decisions sent by the supervisor can be "listened" by an intruder. We adopt the concept of an information-flow property called opacity to capture whether or not the networked supervisory control system is secure. Specifically, we say that the supervisory control system is opaque with insecure control channel if the intruder can never determine for sure that the system is in a secret state based on the control decisions sent by the supervisor. Based on different control decision transmission mechanisms, two notions of opacity are defined. Effective algorithms are also provided to verify different notions of opacity for networked supervisory control systems.