Exact Persistent Stochastic Non-Interference

TL;DR

This paper introduces Exact PSNI, a refined security property for stochastic systems, using weak-exact equivalence to better handle internal actions and improve reasoning about non-interference.

Contribution

It proposes weak-exact equivalence and Exact PSNI, extending previous PSNI with a performance-oriented, compositional framework for stochastic non-interference.

Findings

Weak-exact equivalence extends exact equivalence with relaxed internal actions.

Exact PSNI admits bisimulation and unwinding characterisations.

Results confirm weak-exact equivalence as a robust foundation for non-interference reasoning.

Abstract

Persistent Stochastic Non-Interference (PSNI) was introduced to capture a quantitative security property in stochastic process algebras, ensuring that a high-level process does not influence the observable behaviour of a low-level component, as formalised via lumpable bisimulation. In this work, we revisit PSNI from a performance-oriented perspective and propose a new characterisation based on a refined behavioural relation. We introduce \emph{weak-exact equivalence}, which extends exact equivalence with a relaxed treatment of internal (\(\tau\)) actions, enabling precise control over quantitative observables while accommodating unobservable transitions. Based on this, we define \emph{Exact PSNI} (EPSNI), a variant of PSNI characterised via weak-exact equivalence. We show that EPSNI admits the same bisimulation-based and unwinding-style characterisations as PSNI, and enjoys analogous compositionality properties. These results confirm weak-exact equivalence as a robust foundation for reasoning about non-interference in stochastic systems.