Journal
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE
Volume 121, Issue -, Pages 101-115Publisher
ELSEVIER SCIENCE BV
DOI: 10.1016/j.entcs.2004.10.010
Keywords
opacity; non-deducibility; Petri nets; observable behaviour
Categories
Funding
- EPSRC GOLD and SCREEN projects
- DSTL
Ask authors/readers for more resources
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.
Authors
I am an author on this paper
Click your name to claim this paper and add it to your profile.
Reviews
Recommended
No Data Available