Program Refinement, Perfect Secrecy and Information Flow

Abstract

“Classical” proofs of secure systems are based on reducing the hardness of one problem (defined by the protocol) to that of another (a known difficult computational problem). In standard program development [1, 3, 14] this “comparative approach” features in stepwise refinement: describe a system as simply as possible so that it has exactly the required properties and then apply sound refinement rules to obtain an implementation comprising specific algorithms and data-structures.

More recently the stepwise refinement method has been extended to include “information flow” properties as well as functional properties, thus supporting proofs about secrecy within a program refinement method.

In this paper we review the security-by-refinement approach and illustrate how it can be used to give an elementary treatment of some well known security principles.

A.K. McIver — We acknowledge the support of the Australian Research Council Grant DP140101119.

A   Some Proofs

1.1 A.1   Learning a Value

We prove (9) for the special case where E is the exclusive-OR, $\oplus$. We re-state (9) here for $\oplus$.

$$\begin{aligned} \begin{aligned} P;\mathbf{reveal }_B(Y, X)&= P \Rightarrow \quad \quad \quad \\ P';\mathbf{reveal }_B~Y&= P' \vee P';\mathbf{reveal }_B~X\oplus Y = P', \end{aligned} \end{aligned}$$

(11)

where $P= P'; \mathbf{vis }_B ~b {:}{=}\,X; \mathbf{reveal }~X$.

Assume that B has (private) variables $b_1, b_2 , \dots b_k$, and that A has (private) variables $a_1, a_2 \dots a_m$. We also assume that each variable is assigned exactly once and then never changed.

B’s knowledge of the state after executing $P'$ can be summarised as follows:

• 1. B knows the values of all its own variables $b_1, b_2 , \dots b_k$.

• 2. B knows the values of any encrypted value sent over the public channel. Each of those values is of the form

  $$\begin{aligned} a_{i_1} \oplus a_{i_2} \oplus \dots \oplus a_{i_n}, \end{aligned}$$

  for some selection of variables drawn from $a_1, a_2 \dots a_m$.

• 3. B can learn new facts by using the facts he already has and computing new values using $\oplus$. Let $\mathcal{K}$ be the set of facts so-computed using $\oplus$.

Notice that whenever a value $\alpha \in \mathcal{K}$ we have that $P'; \mathbf{reveal }_B~ \alpha = P'$.

Assume that $Y \not \in \mathcal{K}$, but that when B learns X then he can deduce Y. We will show that $X \oplus Y$ is contained in $\mathcal{K}$.

Since $Y \not \in \mathcal{K}$, this means that $Y = X \oplus \alpha$ for some fact $\alpha \in \mathcal{K}$. But with this we reason:

implying that $X \oplus Y$ (i.e. E.Y.X as at (9)) is contained in $\mathcal{K}$.