Abstract. The Shadow Semantics is a possibilistic (qualitative) model for noninterference security. Subsequent work 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 together 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. We illustrate the technique on some small examples based on secure multi-party computations.
Keywords: Non-interference security; probabilistic non-interference; program semantics; program refinement.