Alessandro Pisano
Verification of -step and infinite-step opacity of bounded labeled Petri nets
Yin Tong
;Hao Lan;Carla Seatzu
2022-01-01
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. (c) 2022 Elsevier Ltd. All rights reserved.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.