Abstractions of non-interference security: probabilistic versus possibilistic

Hoang, Thai Son, McIver, Annabelle K., Meinicke, Larissa, Morgan, Carroll C., Sloane, Anthony and Susatyo, Enrico (2014) Abstractions of non-interference security: probabilistic versus possibilistic. Formal Aspects of Computing, 26 1: 169-194. doi:10.1007/s00165-012-0237-4


Author Hoang, Thai Son
McIver, Annabelle K.
Meinicke, Larissa
Morgan, Carroll C.
Sloane, Anthony
Susatyo, Enrico
Title Abstractions of non-interference security: probabilistic versus possibilistic
Journal name Formal Aspects of Computing   Check publisher's open access policy
ISSN 0934-5043
1433-299X
Publication date 2014-01-01
Sub-type Article (original research)
DOI 10.1007/s00165-012-0237-4
Volume 26
Issue 1
Start page 169
End page 194
Total pages 26
Place of publication London, United Kingdom
Publisher Springer U K
Language eng
Formatted 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.
Keyword Non-interference security
Probabilistic non-interference
Program semantics
Program refinement
Q-Index Code C1
Q-Index Status Provisional Code
Institutional Status Non-UQ

Document type: Journal Article
Sub-type: Article (original research)
Collections: Non HERDC
School of Information Technology and Electrical Engineering Publications
 
Versions
Version Filter Type
Citation counts: TR Web of Science Citation Count  Cited 1 times in Thomson Reuters Web of Science Article | Citations
Scopus Citation Count Cited 2 times in Scopus Article | Citations
Google Scholar Search Google Scholar
Created: Thu, 12 Jun 2014, 00:27:51 EST by Larissa Meinicke on behalf of School of Information Technol and Elec Engineering