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

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

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

(17)

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

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)