On-line verification of initial-state opacity by Petri nets and integer linear programming

This paper deals with a problem related to the observability of discrete event systems: the initial-state opacity. Given a set of system states (the secret), a system observation is called initial-state opaque if an agent (named intruder), who can partially observe the system, cannot determine whether the set of initial states consistent with an event sequence is included in the secret. Such a character can describe security problems in cyber-infrastructures, such as Internet and mobile communication networks or national defense service systems. This work presents a novel on-line methodology to verify the notion of initial-state opacity of discrete event systems that are modeled by labeled Petri nets. By working on-line, the intruder records an event and exploits integer linear programming problem for checking the initial-state opacity of the system's evolution under the given observation. A set of examples are shown to shed light on the efficiency of the presented methodology.