Compositional Closure for Bayes Risk in Probabilistic Noninterference

We give a quantitative sequential model for noninterference security with probability (but not demonic choice), and a novel refinement order that we prove to be the greatest compositional relation consistent with an “elementary” order based on Bayes Risk. This compositional closure complements our earlier work defining refinement similarly for qualitative noninterference with demonic choice (but not probability). The Three-Judges Protocol illustrates our model’s utility: with compositionality, the embedded sub-protocols can be treated in isolation.

• Type: Conference
• Year: 2010
• Where: ICALP
• Authors: Annabelle McIver, Larissa Meinicke, Carroll Morgan
• Keywords: Demonic Choice, Greatest Compositional Relation, ICALP 2010, Programming Languages, Quantitative Sequential Model