Enforcement of Current-State Opacity in Signal Interpreted Petri Nets

This article proposes a new approach for the enforcement of current-state opacity in signal interpreted Petri nets (SIPN). In order to enforce current-state opacity in SIPNs, the properties of iterative firing and simultaneous firing of transitions are considered. To prevent the intruder from inferring the current marking, signals associated with the secret marking are compared to signals associated with alternative markings. This allows to determine which signals need to be encrypted to confuse the secret marking with markings leading to the secret marking, markings directly reachable from the secret marking or markings reachable from the premarking of the secret marking. The proposed approach applies to any system that can be described by an SIPN.