Language-Based Opacity Verification in Partially Observed Petri Nets through Linear Constraints

Information security is an important area of concern in modern computer-integrated systems. It involves implementing preventative measures to protect confidential data from potential vulnerabilities, such as unauthorized access, secret disclosure, modification, or destruction. Considering such threats, we investigate a particular confidentiality property called opacity, which specifies a system’s ability to cover its ‘secret’ data from being interfered with by outside observers, termed as intruders. This paper discusses language-based opacity formulation and verification in the context of discrete event systems represented by partially observed Petri nets. In this context, we identify two opacity properties, called consistency and non-secrecy; then, we exploit the mathematical characterization of a net system, to separately check each property, by specifying two feasibility problems. The proposed method is carried out for two distinct settings of a system. The first setting is centralized, where an intruder is granted complete information about the system structure but a partial observation of its behavior. The second setting is decentralized, where a group of intruders cooperates to reveal the secret language, by using a coordinator. Finally, experimental findings are given, to demonstrate the proficiency of the proposed approach.