Title
Modelling Opacity Using Petri Nets
Abstract
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.
Year
DOI
Venue
2005
10.1016/j.entcs.2004.10.010
Electr. Notes Theor. Comput. Sci.
Keywords
Field
DocType
low-level part,observable behaviour,resulting framework,modelling technique,local state,non-deducibility,system behaviour,modelling opacity,petri nets,opacity,different information flow property,associated verification problem,information flow,petri net
Information flow (information theory),Petri net,Computer science,Decidability,Theoretical computer science,Opacity,Expressivity
Journal
Volume
Issue
ISSN
121
C
1571-0661
Citations 
PageRank 
References 
26
1.58
5
Authors
3
Name
Order
Citations
PageRank
Jeremy W. Bryans117513.88
Maciej Koutny21414117.83
Peter Y. A. Ryan372866.96