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.
Verification of K-step and infinite-step opacity of bounded labeled Petri nets
Yin Tong
Primo
;Hao LanSecondo
;Carla SeatzuUltimo
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.File | Dimensione | Formato | |
---|---|---|---|
Automatica2022 Lan Editoriale.pdf
Solo gestori archivio
Tipologia:
versione editoriale (VoR)
Dimensione
644.37 kB
Formato
Adobe PDF
|
644.37 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
Automatica2022 Lan Postprint.pdf
Open Access dal 19/03/2023
Tipologia:
versione post-print (AAM)
Dimensione
1.2 MB
Formato
Adobe PDF
|
1.2 MB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.