Multilevel transitive and intransitive non-interference, causally
From MaRDI portal
Publication:1680560
DOI10.1016/j.tcs.2017.10.004zbMath1380.68292MaRDI 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
verification; Petri nets; true concurrency; intransitive policies and downgrading; multilevel non-interference; unfolding semantics
68Q55: Semantics in the theory of computing
68Q60: Specification and verification (program logics, model checking, etc.)
68Q85: Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Related Items
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, An optimization-based approach to assess non-interference in labeled and bounded Petri net systems
Uses Software
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