Strong Current-State Opacity Verification of Discrete-Event Systems Modeled with Time Labeled Petri Nets

This paper addresses the verification of strong cur-rent-state opacity with respect to real-time observations generated from a discrete-event system that is modeled with time labeled Petri nets. The standard current-state opacity cannot completely characterize higher-level security. To ensure the higher-level security requirements of a time-dependent system, we propose a strong version of opacity known as strong current-state opacity. For any path (state-event sequence with time information) pi derived from a real-time observation that ends at a secret state, the strong current-state opacity of the real-time observation signifies that there is a non-secret path with the same real-time observation as pi. We propose general and non-secret state class graphs, which characterize the general and non-secret states of time-dependent systems, respectively. To capture the observable behavior of non-secret states, a non-secret observer is proposed. Finally, we develop a structure called a real-time concurrent verifier to verify the strong current-state opacity of time labeled Petri nets. This approach is efficient since the real-time concurrent verifier can be constructed by solving a certain number of linear programming problems.