Opacity generalised to transition systems

Jeremy W. Bryans; Maciej Koutny; Laurent Mazaro; Peter Y.A. Ryan

doi:10.1007/11679219_7

Opacity generalised to transition systems

Jeremy W. Bryans, Maciej Koutny, Laurent Mazaro, Peter Y.A. Ryan

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding

45 Citations (Scopus)

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	https://doi.org/10.1007/11679219_7
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	http://www.iit.cnr.it/FAST2005/

Keywords

opacity
non-deducibility
anonymity
non-inference
Petri nets
observable behaviour
labelled transition systems

Access to Document

10.1007/11679219_7

Fingerprint Dive into the research topics of 'Opacity generalised to transition systems'. Together they form a unique fingerprint.

Cite this

Bryans, J. W., Koutny, M., Mazaro, L., & Ryan, P. Y. A. (2006). Opacity generalised to transition systems. In T. Dimitrakos, F. Martinelli, P. Y. A. Ryan, & S. Schneider (Eds.), Formal Aspects in Security and Trust (Vol. 3866 LNCS, pp. 81-95). (Lecture Notes in Computer Science (LNCS); Vol. 3866). Berlin: Springer Verlag. https://doi.org/10.1007/11679219_7

Opacity generalised to transition systems. / Bryans, Jeremy W.; Koutny, Maciej; Mazaro, Laurent; Ryan, Peter Y.A.

Formal Aspects in Security and Trust. ed. / Theo Dimitrakos; Fabio Martinelli; Peter Y. A. Ryan; Steve Schneider. Vol. 3866 LNCS Berlin : Springer Verlag, 2006. p. 81-95 (Lecture Notes in Computer Science (LNCS); Vol. 3866).

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding

Bryans, JW, Koutny, M, Mazaro, L & Ryan, PYA 2006, Opacity generalised to transition systems. in T Dimitrakos, F Martinelli, PYA Ryan & S Schneider (eds), Formal Aspects in Security and Trust. vol. 3866 LNCS, Lecture Notes in Computer Science (LNCS), vol. 3866, Springer Verlag, Berlin, pp. 81-95, International Workshop on Formal Aspects in Security and Trust, Newcastle upon Tyne, United Kingdom, 18/07/05. https://doi.org/10.1007/11679219_7

@inproceedings{30bf3f30c8fd4b7da22ec621b34d8f0a,

title = "Opacity generalised to transition systems",

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.",

keywords = "opacity, non-deducibility, anonymity, non-inference, Petri nets, observable behaviour, labelled transition systems",

author = "Bryans, {Jeremy W.} and Maciej Koutny and Laurent Mazaro and Ryan, {Peter Y.A.}",

year = "2006",

doi = "10.1007/11679219_7",

language = "English",

isbn = "978-3-540-32628-1",

volume = "3866 LNCS",

series = "Lecture Notes in Computer Science (LNCS)",

publisher = "Springer Verlag",

pages = "81--95",

editor = "Theo Dimitrakos and Fabio Martinelli and Ryan, {Peter Y. A.} and Steve Schneider",

booktitle = "Formal Aspects in Security and Trust",

address = "Austria",

}

TY - GEN

T1 - Opacity generalised to transition systems

AU - Bryans, Jeremy W.

AU - Koutny, Maciej

AU - Mazaro, Laurent

AU - Ryan, Peter Y.A.

PY - 2006

Y1 - 2006

N2 - 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.

AB - 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.

KW - opacity

KW - non-deducibility

KW - anonymity

KW - non-inference

KW - Petri nets

KW - observable behaviour

KW - labelled transition systems

U2 - 10.1007/11679219_7

DO - 10.1007/11679219_7

M3 - Conference proceeding

SN - 978-3-540-32628-1

VL - 3866 LNCS

T3 - Lecture Notes in Computer Science (LNCS)

SP - 81

EP - 95

BT - Formal Aspects in Security and Trust

A2 - Dimitrakos, Theo

A2 - Martinelli, Fabio

A2 - Ryan, Peter Y. A.

A2 - Schneider, Steve

PB - Springer Verlag

CY - Berlin

ER -