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 Lan
Secondo
;
Carla Seatzu
Ultimo
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.
2022
Discrete event systems; Petri nets; K-step opacity; Infinite-step opacity
File in questo prodotto:
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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11584/345573
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 16
  • ???jsp.display-item.citation.isi??? 11
social impact