Verification of State-Based Opacity Using Petri Nets

Tong, Yin

First

;Li, Zhiwu

Second

;Seatzu, Carla

Penultimate

;Giua, Alessandro

Last

2017-01-01

---

Abstract

A system is said to be opaque if a given secret behavior remains opaque (uncertain) to an intruder who can partially observe system activities. This work addresses the verification of state-based opacity in systems modeled with Petri nets. The secret behavior of a system is defined as a set of states. More precisely, two state-based opacity properties are considered: current-state opacity and initial-state opacity. We show that both current-state and initial-state opacity problems in bounded Petri nets can be efficiently solved by using a compact representation of the reachability graph, called basis reachability graph (BRG). This approach is practically efficient since the exhaustive enumeration of the reachability space can be avoided.