Noninterference Analysis of Irreversible Systems and Reversible Systems Featuring both Nondeterminism and Probabilities
Pith reviewed 2026-05-23 04:26 UTC · model grok-4.3
The pith
Noninterference properties for systems mixing nondeterminism and probabilities are defined via probabilistic weak bisimilarity in irreversible cases and probabilistic branching bisimilarity in reversible cases.
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
Core claim
Noninterference can be characterized by requiring that a system is probabilistically weakly bisimilar (irreversible case) or probabilistically branching bisimilar (reversible case) to the system obtained by replacing every high-level action with an unobservable one. The paper shows that the resulting family of properties forms a taxonomy ordered by strength, that the properties are preserved by the usual process-algebra operators, and that they compose in the same way as their nondeterministic predecessors, with the lottery contract serving as a concrete witness that the definitions detect leaks when they exist and accept secure implementations when they do not.
What carries the argument
Probabilistic weak bisimilarity for irreversible systems and probabilistic branching bisimilarity for reversible systems, which equate processes while matching both nondeterministic branches and probability distributions over observable actions.
If this is right
- The taxonomy orders the noninterference notions by inclusion, with the strongest requiring bisimilarity after every possible high-level action sequence.
- Each defined property is preserved by parallel composition, restriction, and relabeling in the process algebra.
- Compositionality results allow secure subsystems to be combined without introducing new leaks.
- The same definitions apply without change to the alternating model used for the lottery contract example.
- Earlier taxonomies for purely nondeterministic and for generative-reactive probabilistic systems are recovered as special cases.
Where Pith is reading between the lines
- The framework could be used to check noninterference in other randomized protocols such as voting or distributed ledgers beyond the lottery example.
- If the alternating model is replaced by a fully generative one, the branching-bisimulation variant might need adjustment to retain the same compositionality.
- Automated decision procedures for the probabilistic bisimilarities would turn the taxonomy into a practical verification tool.
- Reversible systems with probabilities might admit additional equivalences that distinguish more leaks than branching bisimilarity captures.
Load-bearing premise
The probabilistic versions of the bisimilarities preserve noninterference exactly as the nondeterministic versions do.
What would settle it
A concrete alternating probabilistic process in which two states are related by probabilistic weak or branching bisimilarity yet the probability of a low-level observable action changes when a high-level input is varied.
read the original abstract
The theory of noninterference supports the analysis of secure computations in multi-level security systems. Classical equivalence-based approaches to noninterference mainly rely on bisimilarity. In a nondeterministic setting, assessing noninterference through weak bisimilarity is adequate for irreversible systems, whereas for reversible ones branching bisimilarity has been recently proven to be more appropriate. In this paper we address the same two families of systems with the difference that probabilities come into play in addition to nondeterminism according to the alternating model of Hansson and Jonsson. For irreversible systems we extend the results of Aldini, Bravetti, and Gorrieri developed in a generative-reactive probabilistic setting, while for reversible systems we extend the results of Esposito, Aldini, Bernardo, and Rossi developed in a purely nondeterministic setting. We recast noninterference properties by adopting probabilistic variants of weak and branching bisimilarities for irreversible and reversible systems, respectively. Then we investigate a taxonomy of those properties as well as their preservation and compositionality aspects, along with a comparison with earlier taxonomies. The adequacy of the extended noninterference theory is illustrated via a probabilistic smart contract lottery.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper extends noninterference analysis to systems combining nondeterminism and probabilities under the alternating model. For irreversible systems it adapts probabilistic weak bisimilarity to recast noninterference properties, extending Aldini et al.; for reversible systems it uses probabilistic branching bisimilarity, extending Esposito et al. It then develops a taxonomy of the resulting properties, studies their preservation and compositionality, compares the taxonomy with prior ones, and illustrates adequacy via a probabilistic smart-contract lottery example.
Significance. If the claimed extensions and taxonomy hold, the work supplies a uniform equivalence-based framework for noninterference that handles both irreversibility and reversibility in the presence of probabilities, thereby bridging two previously separate lines of research. The explicit comparison with earlier taxonomies and the concrete lottery illustration are positive features that could aid adoption in probabilistic security analysis.
major comments (2)
- [§3–4 (definitions and preservation theorems)] The central claims rest on the assertion that probabilistic weak/branching bisimilarities preserve noninterference exactly as their nondeterministic counterparts do; without the explicit definitions of the probabilistic bisimilarities (presumably in §3 or §4) and the corresponding preservation proofs, it is impossible to confirm that the alternating-model probabilities do not introduce new distinguishing behaviors that would invalidate the taxonomy.
- [§5 (compositionality)] The compositionality results are stated to hold for the new probabilistic properties, yet the manuscript provides no counter-example or proof sketch showing how the alternating scheduler interacts with the reversible transitions; this is load-bearing for the claim that the taxonomy is closed under parallel composition.
minor comments (2)
- [Abstract] The abstract refers to “probabilistic variants of weak and branching bisimilarities” without naming the precise definitions (e.g., whether they are the ones of Hansson–Jonsson or a custom lifting); a brief inline reference to the adopted definition would improve readability.
- [§6 (case study)] The lottery example is presented as an adequacy illustration, but the text does not indicate which specific noninterference property is being verified or which bisimilarity is used; adding a short table mapping example behaviors to the taxonomy entries would clarify the demonstration.
Simulated Author's Rebuttal
We thank the referee for the detailed review and for identifying areas where additional clarity may strengthen the presentation. We address each major comment below.
read point-by-point responses
-
Referee: [§3–4 (definitions and preservation theorems)] The central claims rest on the assertion that probabilistic weak/branching bisimilarities preserve noninterference exactly as their nondeterministic counterparts do; without the explicit definitions of the probabilistic bisimilarities (presumably in §3 or §4) and the corresponding preservation proofs, it is impossible to confirm that the alternating-model probabilities do not introduce new distinguishing behaviors that would invalidate the taxonomy.
Authors: The definitions of probabilistic weak bisimilarity (for irreversible systems) and probabilistic branching bisimilarity (for reversible systems) appear explicitly in Sections 3 and 4. Both are formulated directly in the alternating model of Hansson and Jonsson, with the usual distinction between nondeterministic and probabilistic transitions. The preservation theorems for the corresponding noninterference properties are stated and proved in the same sections; the proofs adapt the standard arguments from Aldini et al. and Esposito et al. by replacing ordinary bisimulation relations with their probabilistic counterparts while preserving the scheduler quantification. Because the bisimilarities are defined to match probability distributions over matching actions, the alternating scheduler does not create new distinguishing behaviors beyond those already ruled out in the nondeterministic setting. revision: no
-
Referee: [§5 (compositionality)] The compositionality results are stated to hold for the new probabilistic properties, yet the manuscript provides no counter-example or proof sketch showing how the alternating scheduler interacts with the reversible transitions; this is load-bearing for the claim that the taxonomy is closed under parallel composition.
Authors: Section 5 contains the compositionality theorems together with their proofs. The proofs explicitly treat the interaction between the alternating scheduler and reversible transitions by defining the parallel composition operator on the combined transition relation and showing that probabilistic branching bisimilarity is a congruence. A short proof sketch can be extracted from the existing argument if the referee finds the current presentation insufficiently detailed; we are prepared to insert such a sketch (or an expanded appendix) in a revision. revision: partial
Circularity Check
No significant circularity
full rationale
The provided abstract and context describe an extension of noninterference results from prior cited works (Aldini et al. for irreversible systems; Esposito et al. for reversible systems) by adopting probabilistic variants of weak and branching bisimilarities. No equations, definitions, or derivation steps are exhibited that reduce a claimed prediction or result to its own inputs by construction, nor is there evidence of fitted parameters renamed as predictions or ansatzes smuggled via self-citation. The central taxonomy and preservation analysis builds on external prior results without load-bearing self-referential loops visible in the given material. This is the expected outcome for an extension paper whose claims remain independently verifiable against the cited foundations.
Axiom & Free-Parameter Ledger
axioms (1)
- domain assumption Probabilistic variants of weak and branching bisimilarities are appropriate for defining noninterference
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.