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. Bryans | 1 | 175 | 13.88 |
Maciej Koutny | 2 | 1414 | 117.83 |
Peter Y. A. Ryan | 3 | 728 | 66.96 |