Modelling opacity using petri nets

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

    Research output: Contribution to journalArticle

    81 Citations (Scopus)
    11 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 languageEnglish
    Pages (from-to)101-115
    Number of pages15
    JournalElectronic Notes in Theoretical Computer Science
    Volume121
    DOIs
    Publication statusPublished - 10 Feb 2005

    Keywords

    • opacity
    • non-deducibility
    • Petri nets
    • observable behaviour

    Fingerprint Dive into the research topics of 'Modelling opacity using petri nets'. Together they form a unique fingerprint.

  • Cite this