On Intransitive Non-interference in Some Models of Concurrency

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 {em 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.