Verification of K-step Non-Interference for Live Bounded and Reversible Discrete Event Systems Modeled with Petri Nets

The concept of K-step non-interference for discrete event systems deals with the possibility of inferring a secret after at most K observations following the occurrence of the secret itself. K-step non-interference accounts for the possibility of not being able to infer a secret in due time to threaten system’s security. Indeed, if a secret is detected after a maximum delay, the inferred information may be no longer useful, hence nullifying the malicious intrusion. From this point-of-view, the concept of K-step non-interference deals with practical security. This paper formally introduces the concept of K-step non-interference and gives a necessary and sufficient condition to verify such a property when discrete event systems are modeled as bounded, live, and reversible Petri nets. The effectiveness of the proposed approach is shown by means of two examples.