Verification of K-step and infinite-step opacity of bounded labeled Petri nets. (June 2022)

• Record Type: Journal Article
• Authors: Tong, Yin; Lan, Hao; Seatzu, Carla
• Is Part Of: Automatica. Volume 140(2022)
• Publication Date: 2022-06
• Subjects: Discrete event systems -- Petri nets -- K-step opacity -- Infinite-step opacity; Automatic control -- Periodicals; Automation -- Periodicals; 629.805
• DOI: 10.1016/j.automatica.2022.110221
• Languages: English
• ISSNs: 0005-1098

Abstract

Abstract: Opacity is an important information security property. Given a discrete event system, a set of secret states, and an intruder who observes the system evolution through an observation mask, the system is said to be K -step opaque if the intruder is not able to ascertain that the system is or was in a secret state at some time within K steps, namely within the observation of K events. If the intruder is never able to ascertain that the system is or was in a secret state at any time, the system is said to be infinite-step opaque. This work aims at verifying the two opacity properties when the discrete event system is modeled as a bounded labeled Petri net. Using the notion of basis reachability graph, new approaches are proposed to check K -step opacity and infinite-step opacity. The proposed approaches are shown to be more efficient than the standard methods based on the reachability graph.