Language-based Opacity Verification and Enforcement in the Framework of Labeled Petri Nets

This work deals with the language-based opacity verification and enforcement problems in discrete event systems modeled with labeled Petri nets. Opacity is a security property that relates to privacy protection by hiding secret information of a system from an external observer called an "intruder". A secret can be a subset of a system's language. In this case, opacity is referred to as language-based opacity. A system is said to be language-based opaque if an intruder, with a partial observation on the system's behavior, cannot deduce whether the sequences of events corresponding to the generated observations are included in the secret language or not. We propose a novel and efficient approach for language-based opacity verification and enforcement, using the concepts of basis markings and basis partition. First, a sufficient condition is formulated to check language-based opacity for labeled Petri nets by solving an integer-programming problem. A unique graph, called a modified basis reachability graph (MBRG), is then derived to verify different language-based opacity properties. The proposed method relaxes the acyclicity assumption of the unobservable transition subnet thanks to the basis partition notion. A new embedded insertion function technique is also provided to deal with opacity enforcement. This technique ensures that no new observed behavior is created. A verification algorithm is developed to check the enforceability of a system. Finally, once a system is proved to be enforceable, an algorithm is given to construct a new structure, called an insertion automaton, which synthesizes all possible insertion functions that ensure opacity.