Modelling dynamic opacity using Petri Nets with silent actions

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

doi:10.1007/0-387-24098-5_12

Modelling dynamic opacity using Petri Nets with silent actions

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

Newcastle University

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding › peer-review

18 Citations (Scopus)

Abstract

In a previous work, [1], we presented a Petri Net based framework in which various confidentiality properties may be expressed in terms of predicates over system state and abstraction mappings from the reachable states and transitions of the underlying Petri Net. Here we extend that work by generalising these mappings by allowing them to be state dependent. This provides a natural framework in which to model various situations of importance in security, for example key compromise and refresh, downgrading of secrecy labels and conditional anonymity. We also show how global changes in the abstraction mappings can be used to model how some secrecy requirements depend on the status of the observer. We illustrate this by modelling the various flavours of anonymity that arise in the dining cryptographers example.

A further development on the earlier work is to provide a more complete treatment of silent actions. We also discuss the expressiveness of the resulting framework and the decidability of the associated verification problems.1

Original language	English
Title of host publication	Formal Aspects in Security and Trust
Editors	Theo Dimitrakos, Fabio Martinelli
Place of Publication	Boston
Publisher	Springer Verlag
Pages	159-172
Number of pages	14
Volume	173
ISBN (Electronic)	978-0-387-24098-5
ISBN (Print)	978-0-387-24050-3
DOIs	https://doi.org/10.1007/0-387-24098-5_12
Publication status	Published - 2005
Event	IFIP World Computer Congress - Toulouse, France Duration: 22 Aug 2004 → 27 Aug 2004 Conference number: 18 http://webhost.laas.fr/TSF/wcc2004/

Publication series

Name	IFIP International Federation for Information Processing (IFIPAICT)
Publisher	Springer
Volume	173

Conference

Conference	IFIP World Computer Congress
Abbreviated title	IFIP WCC
Country/Territory	France
City	Toulouse
Period	22/08/04 → 27/08/04
Internet address	http://webhost.laas.fr/TSF/wcc2004/

Keywords

opacity
non-deducibility
anonymity
Petri nets
observable behaviour
silent actions

Access to Document

10.1007/0-387-24098-5_12

Cite this

Modelling dynamic opacity using Petri Nets with silent actions. / Bryans, Jeremy W.; Koutny, Maciej; Ryan, Peter Y.A.
Formal Aspects in Security and Trust. ed. / Theo Dimitrakos; Fabio Martinelli. Vol. 173 Boston: Springer Verlag, 2005. p. 159-172 (IFIP International Federation for Information Processing (IFIPAICT); Vol. 173).

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding › peer-review

Bryans, JW, Koutny, M & Ryan, PYA 2005, Modelling dynamic opacity using Petri Nets with silent actions. in T Dimitrakos & F Martinelli (eds), Formal Aspects in Security and Trust. vol. 173, IFIP International Federation for Information Processing (IFIPAICT), vol. 173, Springer Verlag, Boston, pp. 159-172, IFIP World Computer Congress, Toulouse, France, 22/08/04. https://doi.org/10.1007/0-387-24098-5_12

@inproceedings{e06300517baa4acb9287c536623a6169,

title = "Modelling dynamic opacity using Petri Nets with silent actions",

abstract = "In a previous work, [1], we presented a Petri Net based framework in which various confidentiality properties may be expressed in terms of predicates over system state and abstraction mappings from the reachable states and transitions of the underlying Petri Net. Here we extend that work by generalising these mappings by allowing them to be state dependent. This provides a natural framework in which to model various situations of importance in security, for example key compromise and refresh, downgrading of secrecy labels and conditional anonymity. We also show how global changes in the abstraction mappings can be used to model how some secrecy requirements depend on the status of the observer. We illustrate this by modelling the various flavours of anonymity that arise in the dining cryptographers example.A further development on the earlier work is to provide a more complete treatment of silent actions. We also discuss the expressiveness of the resulting framework and the decidability of the associated verification problems.1",

keywords = "opacity, non-deducibility, anonymity, Petri nets, observable behaviour, silent actions",

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

year = "2005",

doi = "10.1007/0-387-24098-5_12",

language = "English",

isbn = "978-0-387-24050-3",

volume = "173",

series = "IFIP International Federation for Information Processing (IFIPAICT)",

publisher = "Springer Verlag",

pages = "159--172",

editor = "Theo Dimitrakos and Fabio Martinelli",

booktitle = "Formal Aspects in Security and Trust",

address = "Austria",

note = "IFIP World Computer Congress, IFIP WCC ; Conference date: 22-08-2004 Through 27-08-2004",

url = "http://webhost.laas.fr/TSF/wcc2004/",

}

TY - GEN

T1 - Modelling dynamic opacity using Petri Nets with silent actions

AU - Bryans, Jeremy W.

AU - Koutny, Maciej

AU - Ryan, Peter Y.A.

N1 - Conference code: 18

PY - 2005

Y1 - 2005

N2 - In a previous work, [1], we presented a Petri Net based framework in which various confidentiality properties may be expressed in terms of predicates over system state and abstraction mappings from the reachable states and transitions of the underlying Petri Net. Here we extend that work by generalising these mappings by allowing them to be state dependent. This provides a natural framework in which to model various situations of importance in security, for example key compromise and refresh, downgrading of secrecy labels and conditional anonymity. We also show how global changes in the abstraction mappings can be used to model how some secrecy requirements depend on the status of the observer. We illustrate this by modelling the various flavours of anonymity that arise in the dining cryptographers example.A further development on the earlier work is to provide a more complete treatment of silent actions. We also discuss the expressiveness of the resulting framework and the decidability of the associated verification problems.1

AB - In a previous work, [1], we presented a Petri Net based framework in which various confidentiality properties may be expressed in terms of predicates over system state and abstraction mappings from the reachable states and transitions of the underlying Petri Net. Here we extend that work by generalising these mappings by allowing them to be state dependent. This provides a natural framework in which to model various situations of importance in security, for example key compromise and refresh, downgrading of secrecy labels and conditional anonymity. We also show how global changes in the abstraction mappings can be used to model how some secrecy requirements depend on the status of the observer. We illustrate this by modelling the various flavours of anonymity that arise in the dining cryptographers example.A further development on the earlier work is to provide a more complete treatment of silent actions. We also discuss the expressiveness of the resulting framework and the decidability of the associated verification problems.1

KW - opacity

KW - non-deducibility

KW - anonymity

KW - Petri nets

KW - observable behaviour

KW - silent actions

U2 - 10.1007/0-387-24098-5_12

DO - 10.1007/0-387-24098-5_12

M3 - Conference proceeding

SN - 978-0-387-24050-3

VL - 173

T3 - IFIP International Federation for Information Processing (IFIPAICT)

SP - 159

EP - 172

BT - Formal Aspects in Security and Trust

A2 - Dimitrakos, Theo

A2 - Martinelli, Fabio

PB - Springer Verlag

CY - Boston

T2 - IFIP World Computer Congress

Y2 - 22 August 2004 through 27 August 2004

ER -

Modelling dynamic opacity using Petri Nets with silent actions

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this