2011 | OriginalPaper | Buchkapitel
On Intransitive Non-interference in Some Models of Concurrency
verfasst von : Roberto Gorrieri, Matteo Vernali
Erschienen in: Foundations of Security Analysis and Design VI
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Intransitive non-interference (
INI
for short) is a behavioural property extensively studied by Rushby over deterministic automata with outputs associated to transitions (Mealy machines) in order to discuss the security of systems where declassification of secret information is allowed. In this paper, we first propose a natural transposition of Rushby’s definition on deterministic labelled transition systems, we call
INI
as well, and then an alternative, yet more easily checkable, formulation of
INI
, called
NI with downgraders
(
NID
for short). We show how
NID
can be naturally extended to the case of nondeterministic automata by using a variation of it based on bisimulation equivalence (
BNID
). The most novel contribution of this paper is the extension of this theory on the class of Petri nets called elementary net systems: we propose a semi-static technique, called
PBNID
and based on the inspection of the net structure, that is shown to be equivalent to
BNID
.