On-line Algorithm for Current State Opacity Enforcement in a Petri Net Framework

Opacity notion is a security and privacy property that verifies whether an external observer (intruder) can deduce a secret of a system by observing its behaviour. This paper addresses the current state opacity verification and enforcement in the framework of Petri Net (PN): an observation of the system is said to be current-state opaque if an intruder is unable to determine whether the current-state of the system belongs to a set of secret states, otherwise it is said to be not current-state opaque. The run time verifier waits for an observable event and performs an algorithm based on the solution of Integer Linear Programming problem to verify the current state opacity and preserve the secret. Indeed, if the secret may be discovered, then the last event is hidden. An example shows the efficiency of the proposed approach.