Verification of language-based opacity in Petri nets using verifier

Abstract

A system is said to be language opaque if the intruder cannot infer if the generated event sequence belongs to a secret based on its partial observation. In this paper we address the problem of verifying language-based opacity in systems modeled by bounded labeled Petri nets. We generalize the notion of language opacity to strict language opacity to deal with the case where the intruder is only interested in a subset of transitions. Furthermore, we show that strict language opacity is identical to language opacity for a special class of secrets. A verifier is constructed to analyze strict language opacity under the assumption that the intruder only cares about observable transitions.