Multilevel transitive and intransitive non-interference, causally

DOI10.1016/j.tcs.2017.10.004zbMath1380.68292OpenAlexW2769121349MaRDI QIDQ1680560

Paolo Baldan, Alessandro Beggiato

Publication date: 16 November 2017

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/hal-01631722/file/416253_1_En_1_Chapter.pdf

zbMATH Keywords

verificationPetri netstrue concurrencyintransitive policies and downgradingmultilevel non-interferenceunfolding semantics

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items (3)

An optimization-based approach to assess non-interference in labeled and bounded Petri net systems ⋮ Assessment of initial-state-opacity in live and bounded labeled Petri net systems via optimization techniques ⋮ Current-state opacity modelling and verification in partially observed Petri nets

Uses Software

• PEP
• Anica
• MultiUbic

Cites Work

• Unnamed Item
• Unnamed Item
• Petri nets, event structures and domains. I
• A technique of state space search based on unfolding
• An improvement of McMillan's unfolding algorithm
• Canonical prefixes of Petri net unfoldings
• Unfoldings: A partial-order approach to model checking.
• A Causal View on Non-Interference*
• Deciding Selective Declassification of Petri Nets
• Discretionary Information Flow Control for Interaction-Oriented Specifications
• On Intransitive Non-interference in Some Models of Concurrency
• Causality, Behavioural Equivalences, and the Security of Cyberphysical Systems
• Structural non-interference in elementary and trace nets
• A lattice model of secure information flow
• Types of Asynchronous Diagnosability and the Reveals-Relation in Occurrence Nets
• Programming Languages and Systems
• Refinement of actions and equivalence notions for concurrent systems

This page was built for publication: Multilevel transitive and intransitive non-interference, causally