Modelling Opacity Using Petri Nets
Jeremy W. Bryans, Maciej Koutny, Peter Y. A. Ryan · Electronic Notes in Theoretical Computer Science · 2005
We consider opacity as a property of the local states of the secure (or high-level) part of the system, based on the observation of the local states of a low-level part of the system as well as actions. We propose a Petri net modelling technique which allows one to specify different information flow properties, using suitably defined observations of system behaviour. We then discuss expressiveness of the resulting framework and the decidability of the associated verification problems.