Abstractions of non-interference security

Probabilistic versus possibilistic

T. S. Hoang, A. K. McIver*, L. Meinicke, C. C. Morgan, A. Sloane, E. Susatyo

*Corresponding author for this work

Research output: Contribution to journalArticle

3 Citations (Scopus)

Abstract

The Shadow Semantics (Morgan, Math Prog Construction, vol 4014, pp 359-378, 2006; Morgan, Sci Comput Program 74(8):629-653, 2009) is a possibilistic (qualitative) model for noninterference security. Subsequent work (McIver et al., Proceedings of the 37th international colloquium conference on Automata, languages and programming: Part II, 2010) presents a similar but more general quantitative model that treats probabilistic information flow. Whilst the latter provides a framework to reason about quantitative security risks, that extra detail entails a significant overhead in the verification effort needed to achieve it. Our first contribution in this paper is to study the relationship between those two models (qualitative and quantitative) in order to understand when qualitative Shadow proofs can be "promoted" to quantitative versions, i.e. in a probabilistic context. In particular we identify a subset of the Shadow's refinement theorems that, when interpreted in the quantitative model, still remain valid even in a context where a passive adversary may perform probabilistic analysis. To illustrate our technique we show how a semantic analysis together with a syntactic restriction on the protocol description, can be used so that purely qualitative reasoning can nevertheless verify probabilistic refinements for an important class of security protocols. We demonstrate the semantic analysis by implementing the Shadow semantics in Rodin, using its special-purpose refinement provers to generate (and discharge) the required proof obligations (Abrial et al., STTT 12(6):447-466, 2010). We apply the technique to some small examples based on secure multi-party computations.

Original languageEnglish
Pages (from-to)169-194
Number of pages26
JournalFormal Aspects of Computing
Volume26
Issue number1
DOIs
Publication statusPublished - Jan 2014

Fingerprint Dive into the research topics of 'Abstractions of non-interference security: Probabilistic versus possibilistic'. Together they form a unique fingerprint.

  • Cite this