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 two examples, one describing anonymity in a commercial context, and the other modelling requirements upon a simple voting system.
Original language | English |
---|---|
Title of host publication | Formal Aspects in Security and Trust |
Editors | Theo Dimitrakos, Fabio Martinelli, Peter Y. A. Ryan, Steve Schneider |
Place of Publication | Berlin |
Publisher | Springer Verlag |
Pages | 81-95 |
Number of pages | 15 |
Volume | 3866 LNCS |
ISBN (Electronic) | 978-3-540-32629-8 |
ISBN (Print) | 978-3-540-32628-1 |
DOIs | |
Publication status | Published - 2006 |
Event | International Workshop on Formal Aspects in Security and Trust - Newcastle upon Tyne, United Kingdom Duration: 18 Jul 2005 → 19 Jul 2005 Conference number: 3 http://www.iit.cnr.it/FAST2005/ |
Publication series
Name | Lecture Notes in Computer Science (LNCS) |
---|---|
Publisher | Springer |
Volume | 3866 |
Workshop
Workshop | International Workshop on Formal Aspects in Security and Trust |
---|---|
Abbreviated title | FAST |
Country | United Kingdom |
City | Newcastle upon Tyne |
Period | 18/07/05 → 19/07/05 |
Internet address |
Keywords
- opacity
- non-deducibility
- anonymity
- non-inference
- Petri nets
- observable behaviour
- labelled transition systems