In: Theo Dimitrakos, Fabio Martinelli, Peter Y.A. Ryan, Steve Schneider (Eds.): Lecture Notes in Computer Science, 3866: Formal Aspects in Security and Trust: Thrid International Workshop, FAST 2005, Newcastle upon Tyne, UK, July 18-19, 2005, Revised Selected Papers, pages 81-95. Springer-Verlag, February 2006. URL: http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/116792197,.
Abstract: 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 an example modelling requirements upon a simple voting system.
Keywords: opacity, non-deducibility, anonymity, non-inference, Petri nets, observable behaviour, labelled transition systems..