Assessment of Bisimulation Non-Interference in Discrete Event Systems Modelled With Bounded Petri Nets

Non-interference in discrete event systems deals with the possibility by an intruder to infer the occurrences of private and non observable events, the so called high-level ones, by interacting with the system at a user level, i.e., by observing the occurrence of the so called low-level ones. When bisimulation non-interference is considered, the security objective is not only to avoid the detection of high-level event occurrences, but also to avoid the detection of their non occurrences; i.e., the secret includes also the non occurrences of some events. This letter deals with such a more restrictive security property in the framework of discrete event systems modelled as Petri nets. A necessary and sufficient condition is given to assess bisimulation non-interference in bounded Petri nets. Such a condition requires the solution of integer linear programming optimization problems, whose solution can be used also to statically enforce bisimulation non-interference when this condition is not satisfied by the original system.