Modelling dynamic opacity using Petri Nets with silent actions

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

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

    13 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 languageEnglish
    Title of host publicationFormal Aspects in Security and Trust
    EditorsTheo Dimitrakos, Fabio Martinelli
    Place of PublicationBoston
    PublisherSpringer Verlag
    Pages159-172
    Number of pages14
    Volume173
    ISBN (Electronic)978-0-387-24098-5
    ISBN (Print)978-0-387-24050-3
    DOIs
    Publication statusPublished - 2005
    EventIFIP World Computer Congress - Toulouse, France
    Duration: 22 Aug 200427 Aug 2004
    Conference number: 18
    http://webhost.laas.fr/TSF/wcc2004/

    Publication series

    NameIFIP International Federation for Information Processing (IFIPAICT)
    PublisherSpringer
    Volume173

    Conference

    ConferenceIFIP World Computer Congress
    Abbreviated titleIFIP WCC
    CountryFrance
    CityToulouse
    Period22/08/0427/08/04
    Internet address

    Keywords

    • opacity
    • non-deducibility
    • anonymity
    • Petri nets
    • observable behaviour
    • silent actions

    Fingerprint Dive into the research topics of 'Modelling dynamic opacity using Petri Nets with silent actions'. Together they form a unique fingerprint.

  • Cite this

    Bryans, J. W., Koutny, M., & Ryan, P. Y. A. (2005). Modelling dynamic opacity using Petri Nets with silent actions. In T. Dimitrakos, & F. Martinelli (Eds.), Formal Aspects in Security and Trust (Vol. 173, pp. 159-172). (IFIP International Federation for Information Processing (IFIPAICT); Vol. 173). Boston: Springer Verlag. https://doi.org/10.1007/0-387-24098-5_12