Jeremy W. Bryans, Maciej Koutny, Laurent Mazare and Peter Y.A. Ryan
Opacity Generalised to Transition Systems (2004)
Opacity Generalised to Transition Systems (2004)
TR-2004-25.ps
Keywords: opacity, non-deducibility, anonymity, non-interference, Petri nets, observable behaviour, labelled transition systems, abstract interpretation
Abstract: Recently, opacity has proved to be a promising technique for describing security properties. Much of the work has been couched in terms of Petri nets. Here, we extend the notion of opacity to the model of labelled transition systems and generalise opacity in order to better represent concepts from the work on information flow. In particular, we establish links between opacity and the information flow concepts of anonymity and non-interference such as non-inference. We also investigate ways of verifying opacity when working with Petri nets. Our work is illustrated by two examples, one describing anonymity in a commercial context, and the other modelling requirements upon a simple voting system.
