Modelling opacity using petri nets

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

doi:10.1016/j.entcs.2004.10.010

Modelling opacity using petri nets

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

Newcastle University

Research output: Contribution to journal › Article › peer-review

153 Citations (Scopus)

90 Downloads (Pure)

Abstract

We consider opacity as a property of the local states of the secure (or high-level) part of the system, based on the observation of the local states of a low-level part of the system as well as actions. We propose a Petri net modelling technique which allows one to specify different information flow properties, using suitably defined observations of system behaviour. We then discuss expressiveness of the resulting framework and the decidability of the associated verification problems.

Publisher Statement: This is an Open Access article distributed under the terms of the Creative Commons Attribution Non-Commercial License (http://creativecommons.org/licenses/by/4.0/), which permits non-commercial re-use, distribution, and reproduction in any medium, provided the original work is properly cited.

Original language	English
Pages (from-to)	101-115
Number of pages	15
Journal	Electronic Notes in Theoretical Computer Science
Volume	121
DOIs	https://doi.org/10.1016/j.entcs.2004.10.010
Publication status	Published - 10 Feb 2005

Keywords

opacity
non-deducibility
Petri nets
observable behaviour

Access to Document

10.1016/j.entcs.2004.10.010Licence: CC BY

PublishedFinal published version, 532 KBLicence: CC BY

Cite this

@article{63cd7c7554684fa898b54ec9daede01e,

title = "Modelling opacity using petri nets",

abstract = "We consider opacity as a property of the local states of the secure (or high-level) part of the system, based on the observation of the local states of a low-level part of the system as well as actions. We propose a Petri net modelling technique which allows one to specify different information flow properties, using suitably defined observations of system behaviour. We then discuss expressiveness of the resulting framework and the decidability of the associated verification problems.Publisher Statement: This is an Open Access article distributed under the terms of the Creative Commons Attribution Non-Commercial License (http://creativecommons.org/licenses/by/4.0/), which permits non-commercial re-use, distribution, and reproduction in any medium, provided the original work is properly cited.",

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

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

year = "2005",

month = feb,

day = "10",

doi = "10.1016/j.entcs.2004.10.010",

language = "English",

volume = "121",

pages = "101--115",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

publisher = "Elsevier",

}

TY - JOUR

T1 - Modelling opacity using petri nets

AU - Bryans, Jeremy W.

AU - Koutny, Maciej

AU - Ryan, Peter Y.A.

PY - 2005/2/10

Y1 - 2005/2/10

N2 - We consider opacity as a property of the local states of the secure (or high-level) part of the system, based on the observation of the local states of a low-level part of the system as well as actions. We propose a Petri net modelling technique which allows one to specify different information flow properties, using suitably defined observations of system behaviour. We then discuss expressiveness of the resulting framework and the decidability of the associated verification problems.Publisher Statement: This is an Open Access article distributed under the terms of the Creative Commons Attribution Non-Commercial License (http://creativecommons.org/licenses/by/4.0/), which permits non-commercial re-use, distribution, and reproduction in any medium, provided the original work is properly cited.

AB - We consider opacity as a property of the local states of the secure (or high-level) part of the system, based on the observation of the local states of a low-level part of the system as well as actions. We propose a Petri net modelling technique which allows one to specify different information flow properties, using suitably defined observations of system behaviour. We then discuss expressiveness of the resulting framework and the decidability of the associated verification problems.Publisher Statement: This is an Open Access article distributed under the terms of the Creative Commons Attribution Non-Commercial License (http://creativecommons.org/licenses/by/4.0/), which permits non-commercial re-use, distribution, and reproduction in any medium, provided the original work is properly cited.

KW - opacity

KW - non-deducibility

KW - Petri nets

KW - observable behaviour

U2 - 10.1016/j.entcs.2004.10.010

DO - 10.1016/j.entcs.2004.10.010

M3 - Article

SN - 1571-0661

VL - 121

SP - 101

EP - 115

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

ER -

Modelling opacity using petri nets

Abstract

Keywords

Access to Document

Fingerprint

Cite this