Abstract. Taking the Shadow Semantics for non-interference security as our starting point we show how to automate its refinement proofs using Rodin’s special-purpose refinement provers to generate (and discharge) the required proof obligations.
A second contribution is to identify a subset of Shadow refinement theorems which can be interpreted in a probabilistic model, thereby promoting the theorems of that subset to a context where a passive adversary may perform statistical analysis. In this way we can use a simple automated approach in the verification of an important class of protocols. We illustrate the technique on some small examples based on secure multi-party computations.