Multilevel transitive and intransitive non-interference, causally

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

zbMATH Keywords

verification; Petri nets; true concurrency; intransitive policies and downgrading; multilevel non-interference; unfolding semantics

Mathematics Subject Classification ID

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.)

Uses Software

• PEP
• Anica
• MultiUbic

Cites Work

• 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
• Unnamed Item
• Unnamed Item