Recently, opacity has proved 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 literature on information flow. In particular, we establish links between opacity
and the information flow concepts of anonymity and 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.
Keywords Opacity - Non-deducibility - Anonymity - Petri nets - Observable behaviour - Labelled transition systems - Abstract interpretation