Compositional closure for Bayes risk in probabilistic noninterference

DOI10.1007/978-3-642-14162-1_19MaRDI QIDQ3587441zbMATH OpenOpenAlexFDO

Authors Annabelle McIver, Larissa A. Meinicke, Carroll Morgan

Publication date 7 September 2010

Published in Automata, Languages and Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1007.1054

Mathematics Subject Classification ID

Network protocols (68M12) Semantics in the theory of computing (68Q55) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Abstract: We give a sequential model for noninterference security including probability (but not demonic choice), thus supporting reasoning about the likelihood that high-security values might be revealed by observations of low-security activity. Our novel methodological contribution is the definition of a refinement order and its use to compare security measures between specifications and (their supposed) implementations. This contrasts with the more common practice of evaluating the security of individual programs in isolation. The appropriateness of our model and order is supported by our showing that our refinement order is the greatest compositional relation --the compositional closure-- with respect to our semantics and an "elementary" order based on Bayes Risk --- a security measure already in widespread use. We also relate refinement to other measures such as Shannon Entropy. By applying the approach to a non-trivial example, the anonymous-majority Three-Judges protocol, we demonstrate by example that correctness arguments can be simplified by the sort of layered developments --through levels of increasing detail-- that are allowed and encouraged by compositional semantics.

Recommendations

• Abstractions of non-interference security: probabilistic versus possibilistic
• Computational probabilistic non-interference
• Compositional noninterference from first principles
• On quantitative analysis of probabilistic protocols
• Foundations of Security Analysis and Design II

Cited in

(19)

• Abstractions of non-interference security: probabilistic versus possibilistic
• Processing text for privacy: an information flow perspective
• An algebraic approach for reasoning about information flow
• A better composition operator for quantitative information flow analyses
• An axiomatization of information flow measures
• Program algebra for quantitative information flow
• Quantifying information leakage of randomized protocols
• Compositional methods for information-hiding
• On the relation between differential privacy and quantitative information flow
• Quantifying Vulnerability of Secret Generation Using Hyper-Distributions
• Algebra for quantitative information flow
• Beyond Differential Privacy: Composition Theorems and Relational Logic for f-divergences between Probabilistic Programs
• Hidden-Markov program algebra with iteration
• Quantifying opacity
• On the Additive Capacity Problem for Quantitative Information Flow
• Proving that programs are differentially private
• Probabilistic datatypes
• Composition theorems for f-differential privacy
• Probabilistic predicate transformers. II: Partially observable probability

This page was built for publication: Compositional closure for Bayes risk in probabilistic noninterference

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3587441)