Safe Equivalences for Security Properties

Mário S. Alvim^{1}, Miguel E. Andrés^{2}, Catuscia Palamidessi^{1}, and Peter van Rossum^{2}.

1INRIA and LIX, École Polytechnique Palaiseau, France. 2Institute for Computing and Information Sciences, The Netherlands.

Abstract. In the field of Security, process equivalences have been used to characterize various information-hiding properties (for instance secrecy, anonymity and non-interference) based on the principle that a protocol P with a variable x satisfies such property if and only if, for every pair of secrets s_{1} and s_{2}, P [s_{1}/x] is equivalent to P [s_{2}/x]. We argue that, in the presence of nondeterminism, the above principle relies on the assumption that the scheduler ”works for the benefit of the protocol”, and this is usually not a safe assumption. Non-safe equivalences, in this sense, include (partial-) trace equivalence, bisimulation and testing. We present a formalism in which we can specify admissible schedulers and, correspondingly, safe versions of these equivalences. We then show these variants are still congruences. Finally, we investigate the relation with the recent notion of ”demonic bisimulation” proposed by Chatzikokolakis, Gethin and Parker.

1 Introduction

Let ã ∈ Σ^{⋆}, we define the set of paths with trace ã as [ã] =^{def} {σ ∈ CPaths(M) | trace(σ) = ã}.

Motivation Consider the system

S =^{def} (c, out)(A || H_{1} || H_{2} || Cor )

where

A =^{def} \overline{c}(sec) H_{1} =^{def} c(s).\overline{out}⟨a⟩ H_{2} =^{def} c(s).\overline{out}⟨b⟩ Corr =^{def} c(s).\overline{out}⟨s⟩

Then we have S {^{a}/_{sec}} ≡ S {^{b}/_{sec}}.

Schedulers:

Bad: They can see the secrets and induce a leakage by making different choices based

on the different secrets Neutral (safe): They do not see the secrets. Same choices for different secrets. Good: They see the secrets and protect from leakage by making different choices based

on the secrets (this is what the “bad” use of bisimulation is based on)

Demonic Angelic

Restricted Omniscient

Table 1.

2 Preliminaries

In this section we gather preliminary notions and results related to probabilistic automata [?,?].

2.1 Probabilistic automata

A function μ: Q → [0, 1] is a discrete probability distribution on a set Q if the support of μ is countable and ∑_{q∈Q} μ(q) = 1. The set of all discrete probability distributions on Q is denoted by D(Q).

Mig: The support of μ does not need to be countable anymore Cat: In the non countable case we would need to use an integral, so let’s leave it this way

A probabilistic automaton is a quadruple M = (Q, Σ, q̂, α) where

– Q is a countable set of states,

– Σ a finite set of actions,

– q̂ the initial state, and

– α a transition function α : Q → P(Σ × D(Q)).

Where P(X) is the set of all finite subsets of X.

If α(q) = ∅ then q is a terminal state. We write q →^{a} μ for (a, μ) ∈ α(q). Moreover, we write q→^{a}r whenever q →^{a} μ and μ(r) > 0. A fully probabilistic automaton is a probabilistic automaton satisfying |α(q)| ≤ 1 for all states. In case α(q) ≠ ∅ in a fully probabilistic automaton, we will overload notation and use α(q) to denote the distribution outgoing from q.

Cat: Should we say that these are called “simple Probabilistic Automata”, althoug we will often use “Probabilistic Automata” for simplicity? In the rest of the paper I have used “simple” to point out the difference with the QEST paper.

A path in a probabilistic automaton is a sequence σ = q_{0} →^{a_{1}} q_{1} →^{a_{2}} ⋯ where q_{i} ∈ Q, a_{i} ∈ Σ and q_{i}⟶^{a_{i+1}}q_{i+1}. A path can be finite in which case it ends with a state. A path is complete if it is either infinite or finite ending in a terminal state. Given a path σ, first(σ) denotes its first state, and if σ is finite then last(σ) denotes its last state. Let Paths_{q}(M) denote the set of all paths, Paths^{⋆}_{q}(M) the set of all finite paths, and

Mig: Catuscia: Is this what you like for first, last, etc?

Cat: Yes, thanks

CPaths_{q}(M) the set of all complete paths of an automaton M, starting from the state q. We will omit q if q = q̂. Paths are ordered by the prefix relation, which we denote by ≤. The trace of a path is the sequence of actions in Σ^{∗} ∪ Σ^{∞} obtained by removing the states, hence for the above path σ we have trace(σ) = a_{1}a_{2} . . .. If Σ′ ⊆ Σ, then trace_{Σ′}(σ) is the projection of trace(σ) on the elements of Σ′. The length of a finite path σ, denoted by |σ|, is the number of actions in its trace.

Let M = (Q, Σ, q̂, α) be a (fully) probabilistic automaton, q ∈ Q a state, and let σ ∈ Paths^{⋆}_{q}(M) be a finite path starting in q. The cone generated by σ is the set of complete paths ⟨σ⟩ = {σ′ ∈ CPaths_{q}(M) | σ ≤ σ′}. Given a fully probabilistic automaton M = (Q, Σ, q̂, α) and a state q, we can calculate the probability value, denoted by P_{q}(σ), of any finite path σ starting in q as follows: P_{q}(q) = 1 and P_{q}(σ →^{a} q′) = P_{q}(σ) · μ(q′), where last(σ) →^{a} μ.

Let Ω_{q} =^{def} CPaths_{q}(M) be the sample space, and let F_{q} be the smallest σ-algebra generated by the cones. Then P_{q} induces a unique probability measure on F_{q} (which we will also denote by P_{q}) such that P_{q}(⟨σ⟩) = P_{q}(σ) for every finite path σ starting in q. For q = q̂ we write P instead of Pq̂.

A scheduler for a probabilistic automaton M is a function

ζ: Paths^{⋆}(M) → (Σ × D(Q) ∪ ⊥)

satisfying ζ(σ) = (a, μ) implies last(σ) →^{a} μ, for each finite path σ. Hence, a scheduler selects an available transitions in each state. It is history dependent since it takes into account the path (history) and not only the current state. It is partial since it gives a sub-probability distribution, i.e., it may halt the execution at any time.

3 Systems

In this section we describe the kind of systems we are dealing with. We start by introducing a variant of probabilistic automata, that we call Tagged Probabilistic Automata. These systems are parallel compositions of probabilistic processes, called components. Each component is equipped with a unique identifier, called tag. Whenever a component

Cat: I have removed the requirement that the components are purely probabilistic. It’s not needed here

(or a pair of components in case of synchronization) makes a step, the corresponding transition will be decorated with the associated tag (or pair of tags).

Similar systems have been already introduced in [?]. The main difference is that here the components are simple probablistic automata, i.e. they may contain internal nondetermism, and each transition goes from a node and a label to a distributions over nodes. In [?] the components are fully probabilistic (except for the input guards, that may receive different values), and the secrets can appear only in a probabilistic choice.

Cat: Make sure we introduce simple (labeled) probabilistic automata in the preliminaries. In this paper, we will use the word “label” to refer to pairs tag: action or (tag,tag):action.

Definition 1. A Tagged Probabilistic Automaton (TPA) is a tuple (Q, L, Σ, q̂, α), where

– Q is a set of states,

– L is a set of tags,

– Σ is a set of actions,

– q̂ ∈ Q is the initial state,

– α: Q → P(L × Σ × D(Q)) is a transition function.

Cat: I have eliminated the restriction that α should be a finite set of transitions

In the following we write q ⟶^{l:a} μ for (ℓ, a, μ) ∈ α(q), and we use Enabled(q) to denote the tags of the components that are enabled to make a transition. Namely,

Enabled(q) =^{def} {ℓ ∈ L | there exists a ∈ Σ, μ ∈ D(Q) such that q ⟶^{l:a} μ}

In these systems, we can decompose the scheduler in two: a global scheduler, which decides which component or pair of components makes the move next, and a local scheduler, which solves the internal nondeterminism of the selected component.

We assume that the local scheduler can select only a transition which is enabled, and that the global scheduler can only select a component among those which are enabled. This means that the execution does not stop unless all components are blocked (suspended or terminated). This is in line with the spirit of process algebra, and also with the tradition of Markov Decision Processes, but contrasts with that of the Probabilistic Automata of Lynch and Segala [?]. However, the results in this paper do not depend on this assumption; we could as well allow schedulers which decide to terminate the execution even though there are transitions enabled in the last state.

Definition 2. Let M = (Q, L, Σ, q̂, α) be a Tagged Probabilistic Automaton.

– A global scheduler for M is a function ζ: Paths^{⋆}(M) → (L ∪ {⊥}) such that for all finite paths σ, if Enabled(last(σ)) ≠ ∅ then ζ(σ) ∈ Enabled(last(σ)), and ζ(σ) = ⊥ otherwise.

Cat: Please use italics for “last”, and for all the other function names.

– A local scheduler for M is a function ξ: Paths^{⋆}(M) → (L × Σ × D(Q) ∪ {⊥}) such that, for all finite paths σ, if α(last(σ)) ≠ ∅ then ξ(σ) ∈ α(last(σ)), and ξ(σ) = ⊥ otherwise.

– A global scheduler ζ and a local scheduler ξ for M are compatible if, for all finite paths σ, ξ(σ) = (ℓ, a, μ) implies ζ(σ) = ℓ, and ξ(σ) = ⊥ implies ζ(σ) = ⊥.

– A scheduler for M is a pair (ζ, ξ) of compatible global and local schedulers for M.

We are going to use a simple probabilistic process calculus (a sort of probabilistic version of CCS [?,?]) to specify the components.

Components’ syntax: We assume a set of actions Σ with elements a, a_{1}, a_{2}, ⋯, including the special symbol τ denoting a silent step. With the exception of τ, each action a has a unique co-action ā ∈ Σ and we assume ¯ ā = a.

A component q is a process specified by the following grammar:

Components q ::= 0  termination
| a.q  prefix
| q_{1} + q_{2} nondeterministic choice
| ∑_{i} p_{i} : q_{i} probabilistic choice
| q_{1} | q_{2} parallel composition
| (a)q  restriction
| A  process call

The p_{i}, in the blind and secret choices, represents the probability of the i-th branch and must satisfy 0 ≤ p_{i} ≤ 1 and ∑_{i} p_{i} = 1. The process call A is a simple process identifier. For each identifier, we assume a corresponding unique process declaration of the form A =^{def} q. The idea is that, whenever A is executed, it triggers the execution of q. Note that q can contain A or another process identifier, which means that our language allows (mutual) recursion.

Components’ semantics: The operational semantics consists of probabilistic transitions of the form q→^{a}μ where q ∈ Q is a process, a ∈ Σ is an action and μ ∈ D(Q) is a distribution on processes. They are specified by the following rules:

PRF \overline{a.q →^{a} δ_{q}}  NDT \frac{q_{1} →^{a} μ}{q_{1} + q_{2} →^{a} μ}

PRB \overline{∑_{i} p_{i} : q_{i} →^{τ} ∘ ∑_{i} p_{i} · δ_{q_{i}}} PAR \frac{q_{1} →^{a} μ}{q_{1} | q_{2} →^{a} μ | q_{2}}

CALL \frac{q →^{a} μ}{A →^{a} μ} if A =^{def} q  COM \frac{q_{1} →^{a} δ_{r_{1}} q_{2} →^{ā} δ_{r_{2}}}{q_{1} | q_{2} →^{τ} δ_{r_{1}|r_{2}}}

RST \frac{q →^{a} μ}{(b)q →^{a} μ} a, ā ≠ b

We assume also the symmetric versions of the rules NDT, PAR and COM. The symbol δ_{q} is the delta of Dirac, which assigns probability 1 to q and 0 to all other processes. The symbol ∘ ∑_{i} represents summation on distributions. Namely, ∘ ∑_{i} p_{i} · μ_{i} is the distribution μ such that μ(x) = ∑_{i} p_{i} · μ_{i}(x). The notation μ | q represents the distribution μ′ such that μ′(r) = μ(q′) if r = q′ | q, and μ′(r) = 0 otherwise.

Systems A system is composed by n processes (components) in parallel, and restricted at the top-level on a subset of actions A ⊆ Σ:

(A) q_{1} ∥ q_{2} ∥ ⋯ ∥ q_{n}.

The restriction on A enforces synchronization on the channel names belonging to A, in accordance with the CCS spirit.

Systems’ semantics The semantics of a system gives rise to a TPA, where the states are terms representing systems during their evolution. A transition now is of the form q ⟶^{ℓ:a} μ where a ∈ Σ, μ ∈ D(Q), and ℓ ∈ L is either the tag of the component which makes the move, or a (unordered) pair of tags representing the two partners of a synchronization. We will set L to be the indexes of the componets, i.e. L = I ∪ I^{2} where I = {1, 2, …, n}.

Interleaving

\frac{q_{i} →^{a} ∘ ∑_{j} p_{j} · δ_{q_{ij}}}{(A) q_{1} ∥ ⋯ ∥ q_{i} ∥ ⋯ ∥ q_{n} ⟶^{i:a} ∘ ∑_{j} p_{j} · δ_{(A)q_{1}∥···∥q_{ij}∥···∥q_{n}}} a ∉ A

where i is the tag indicating that the component i is making the step.

Note that we assume that the probabilistic choices in the syntax of the components are finite. This implies that every transition q ⟶^{ℓ:a} μ can be written as q ⟶^{ℓ:a} ∘ ∑_{i} p_{i} ·δ_{q_{i}}, thus justifying the notation used in the interleaving rule.

Synchronization

\frac{q_{i} →^{a} δ_{q′_{i}} q_{j} →^{ā} δ_{q′_{j}}}{(A) q_{1} ∥ ⋯ ∥ q_{i} ∥ ⋯ ∥ q_{j} ∥ ⋯ ∥ q_{n} ⟶^{i,j:τ} δ_{(A)q_{1}∥···∥q′_{i}∥···∥q′_{j}∥···∥q_{n}}}

here {i, j} is the tag indicating that the components making the step are i and j. We write i, j instead than {i, j}, for simplicity.

Example 1. We now show the semantic of the example presented in the Introduction. Figure ?(a) shows the semantic of S {^{a}/_{sec}}, for simplicity we do not write neither the restriction on channels c and out neither the termination symbol 0 of each component, furthermore, we use − to denote a component that is stuck. Similarly the semantic of S {^{a}/_{sec}} is shown in Figure ?(b).

The set of enable transitions also become clear in the figures, we have, for instance, Enabled(S \{^{b}/_{sec}\}) = \{(1, 2), (1, 3), (1, 4)\} and Enabled( 0 || \overline{out}⟨a⟩ || − || − ) = {2}. Finally, the scheduler ζ defined as

ζ(σ) =^{def} \begin{cases}(1, 4) & if σ = S \{^{a}/_{sec}\} , \\ 2 & if σ = S \{^{a}/_{sec}\} ⟶^{1,2:τ} ( 0 || \overline{out}⟨a⟩ || − || − ), \\ 3 & if σ = S \{^{a}/_{sec}\} ⟶^{1,3:τ} ( 0 || − || \overline{out}⟨b⟩ || − ), \\ 4 & if σ = S \{^{a}/_{sec}\} ⟶^{1,4:τ} ( 0 || − || − || \overline{out}⟨a⟩ ), \\ ⊥ & otherwiase, \end{cases}

is a global scheduler for S {^{a}/_{sec}}.

1(a) S {^{a}/_{sec}}  1(b) S {^{b}/_{sec}}

Mig: I am having some issues with the numbering of this figure, try to solve it, otherwise insert the figure number explicitly in the text

4 Safe equivalences

In this section we revise some of the main equivalence notions used in literature so to guarantee their safe use in security.

In the following we assume that any probabilistic automaton is unfolded into a tree (this is a standard construction, see for instance [?]). This way, every finite path σ is determined by its last state, last(σ). Consequently, we can view a scheduler as a function on states, and we write ζ(q) instead than ζ(σ), where q = last(σ).

4.1 Safe Traces

We define here a safe version of complete-trace semantics. The idea is that we want to compare two processes on the basis not only of their traces, but also of the choices that the global scheduler makes at every step. One way of doing this is by recording explicitly the tags in the traces.

Definition 3.

– Given a TAP M = (Q, L, Σ, q̂, α) the (complete) safe traces of M, denoted here by Traces_{s}(M), are defined as the sequence of tags and actions in all possible complete executions, i.e.

Traces_{s}(M) =

{ℓ_{1} : a_{1} · ℓ_{2} : a_{2} · . . . · ℓ_{n} : a_{n} | q̂ ⟶^{ℓ_{1}:a_{1}} q_{1} ⟶^{ℓ_{2}:a_{2}} … ⟶^{ℓ_{n}:a_{n}} q_{n} −̸→}  finite

∪

{ℓ_{1} : a_{1} · ℓ_{2} : a_{2} · . . . · ℓ_{n} : a_{n} · . . . | q̂ ⟶^{ℓ_{1}:a_{1}} q_{1} ⟶^{ℓ_{2}:a_{2}} … ⟶^{ℓ_{n}:a_{n}} q_{n} …} infinite

– Given a system q, we will denote by Traces_{s}(q) the safe traces of the automaton associated to q.

– Two systems q_{1} and q_{2} are safe-trace equivalent, denoted by q_{1} ≃_{s} q_{2}, if and only if Traces_{s}(q_{1}) = Traces_{s}(q_{2}).

It is clear that safe-trace equivalence is at least as discriminating as the standard (complete-) trace equivalence, denoted here by ≃, which compares only the sequences of actions. In fact, the latter is obtained from the former by abstracting from the tags. The following example points out the converse does not hold.

Example 2. Consider the system S given in the introduction. There we have

Traces(S {^{a}/_{sec}}) = {a, b} = Traces(S {^{b}/_{sec}}).

On the other hand we have

Traces_{s}(S {^{a}/_{sec}}) = {1, 2 : τ · 2 : a, 1, 3 : τ · 3 : b, 1, 4 : τ · 4 : a}

≠

Traces_{s}(S {^{b}/_{sec}}) = {1, 2 : τ · 2 : a, 1, 3 : τ · 3 : b, 1, 4 : τ · 4 : b}.

4.2 Safe Bisimilarity

In this section we propose a security-safe version of bisimulation, that we call safe bisimulation. This is an equivalence relation stricter than safe-trace equivalence, with the advantage of being a congruence.

We start with some notation. Given a TPA M = (Q, L, Σ, q̂, α), and a global scheduler ζ, we denote by α_{ζ} the restriction of α to ζ, i.e. for every q ∈ Q,

α_{ζ}(q) = {(a, μ) | there exists ℓ ∈ L such that (ℓ, a, μ) ∈ α(q) and ζ(q) = ℓ}

We will also write q ⟶^{a}_{ζ} μ for (a, μ) ∈ α_{ζ}(q), and M_{ζ} for the automaton obtained by pruning M from all the choices not compatible with ζ, i.e. M_{ζ} = (Q, L, Σ, q̂, α_{ζ}). Note that M_{ζ} still contains nondeterminism, since there may be μ_{1}, μ_{2}, with μ_{1} ≠ μ_{2}, such that (a_{1}, μ_{1}), (a_{2}, μ_{2}) ∈ α_{ζ} (with either a_{1} = a_{2} or a_{1} ≠ a_{2}).

We now define the notion of safe bisimulation. The idea is that, if q and q′ are bisimilar states, then every move from q should be mimicked by a move from q′ using the same scheduler.

Definition 4. Given a TPA M = (Q, L, Σ, q̂, α), we say that a relation R ⊆ Q × Q is a safe bisimulation if, whenever q_{1}Rq_{2}, then, for all global schedulers ζ for M:

– if q_{1} ⟶^{a}_{ζ} μ_{1}, then there exists μ_{2} such that q_{2} ⟶^{a}_{ζ} μ_{2}, ζ(q_{1}) = ζ(q_{2}), μ_{1}Rμ_{2}, and

– if q_{2} ⟶^{a}_{ζ} μ_{2}, then there exists μ_{1} such that q_{1} ⟶^{a}_{ζ} μ_{1}, ζ(q_{1}) = ζ(q_{2}), μ_{1}Rμ_{2}.

where μ_{1}Rμ_{2} means that for all equivalence classes X ∈ Q/R, we have μ_{1}(X) = μ_{2}(X).

The following result is immediate:

Proposition 1. The union of all the safe bisimulations for M is still a safe bisimulation for M.

Therefore the largest safe bisimulation exists, and coincides with the union of all safe bisimulations. We call it safe bisimilarity, and we denote it by ∼_{s}.

Given two TPA’s on the same L and Σ, M_{1} = (Q_{1}, L, Σ, q̂_{1}, α_{1}) and M_{2} = (Q_{2}, L, Σ, q̂_{2}, α_{2}), we can define bisimulation and bisimilarity across their states, i.e. as relations on (Q_{1} ∪ Q_{2}), in the obvious way, by constructing the TPA M with a new initial state q̂ and two transitions to δq̂_{1} and to δq̂_{2}, respectively.

Given two components or systems, q_{1} and q_{2}, we will say that q_{1} and q_{2} are safely bisimilar, denoted by q_{1} ∼_{s} q_{2}, if the initial states of the corresponding TPA’s are safely bisimilar. Note that q_{1} ∼_{s} q_{2} is possible only if q_{1} and q_{2} have the same number of active components, where “active”, for a component, means that during the execution of the system it will make at least one step.

Note that in the case of components, or of systems constituted by one component only, safe bisimulation and safe bisimilarity coincide with standard bisimulation and bisimilarity, respectively. For systems, safe bisimulation is at least as strong as standard bisimulation (denoted by ∼):

Remark 1. Given two systems q_{1} and q_{2}, if q_{1} ∼_{s} q_{2} then q_{1} ∼ q_{2}.

The converse does not hold in general, as shown by the following example.

Example 3. We consider again the system S presented in the Introduction. It is easy to see that S {^{a}/_{sec}} ∼ S {^{b}/_{sec}}. In order to show that S {^{a}/_{sec}} ≁_{s} S {^{b}/_{sec}} we take the two automata of S {^{a}/_{sec}} and S {^{b}/_{sec}} (see Figure ?), and construct a

new automaton (as described above) with initial state q̂ such that q̂ ⟶^{ℓ:τ} S {^{a}/_{sec}} and q̂ ⟶^{ℓ:τ} S {^{b}/_{sec}}. Now consider the scheduler ζ such that

ζ(σ) =^{def} \begin{cases}ℓ & if σ = q̂, \\ (1, 4) & if σ = q̂ ⟶^{ℓ:τ} S \{^{a}/_{sec}\} , \\ 2 & if σ = q̂ ⟶^{ℓ:τ} S \{^{a}/_{sec}\} ⟶^{1,2:τ} ( 0 || \overline{out}⟨a⟩ || − || − ), \\ 3 & if σ = q̂ ⟶^{ℓ:τ} S \{^{a}/_{sec}\} ⟶^{1,3:τ} ( 0 || − || \overline{out}⟨b⟩ || − ), \\ 4 & if σ = q̂ ⟶^{ℓ:τ} S \{^{a}/_{sec}\} ⟶^{1,4:τ} ( 0 || − || − || \overline{out}⟨a⟩ ), \\ (1, 4) & if σ = q̂ ⟶^{ℓ:τ} S \{^{b}/_{sec}\} , \\ 2 & if σ = q̂ ⟶^{ℓ:τ} S \{^{b}/_{sec}\} ⟶^{1,2:τ} ( 0 || \overline{out}⟨a⟩ || − || − ), \\ 3 & if σ = q̂ ⟶^{ℓ:τ} S \{^{b}/_{sec}\} ⟶^{1,3:τ} ( 0 || − || \overline{out}⟨b⟩ || − ), \\ 4 & if σ = q̂ ⟶^{ℓ:τ} S \{^{b}/_{sec}\} ⟶^{1,4:τ} ( 0 || − || − || \overline{out}⟨b⟩ ), \\ ⊥ & otherwiase. \end{cases}

It is easy to see that, under ζ, S {^{b}/_{sec}} cannot simulate the transition 4:a produced by S {^{a}/_{sec}}.

It turns out that safe bisimulation is a congruence with respect to all the operators of our language, as expressed by the following theorem. Note that the first two items are just the standard compositionality result for probabilistic bisimulation.

Theorem 1. Let a ∈ Σ and A, B, B′ ⊆ Σ. Let p_{1}, …, p_{n} be probability values, and q, q_{1}, q_{2}, …, q_{n}, q′_{1}, q′_{2}, …, q′_{n} be components.

– If q_{1} ∼_{s} q_{2}, then a.q_{1} ∼_{s} a.q_{2}, q_{1} + q ∼_{s} q_{2} + q, and (a)q_{1} ∼_{s} (a)q_{2}.

– If q_{1} ∼_{s} q′_{1}, …, q_{n} ∼_{s} q′_{n} , then ∑_{i} p_{i} : q_{i} ∼_{s} ∑_{i} p_{i} : q′_{i}.

– If (B) q_{1} ∥ … ∥ q_{n} ∼_{s} (B′) q′_{1} ∥ … ∥ q′_{n}, then

(A ∪ B) q_{1} ∥ … ∥ q ∥ … ∥ q_{n} ∼_{s} (A ∪ B′) q′_{1} ∥ … ∥ q ∥ … ∥ q′_{n}.

The following property shows that bisimulation is stronger than safe-trace equivalence, like in the standard case.

Proposition 2. For every pair of components or systems, q_{1} and q_{2}, if q_{1} ∼_{s} q_{2} then q_{1} ≃_{s} q_{2}.

Like in the standard case, the vice-versa does not hold, and safe-trace equivalence is not a congruence.

5 Admissible schedulers

In this section we restrict the discerning power of the global and local schedulers in order to avoid the problem of the information leakage induced in security by clairvoyant schedulers. We impose two kinds of restrictions: For the global scheduler, following the framework proposed in [?], we assume that it can only see, and keep memory of, the observable actions and the components that are enabled. It cannot see the secret actions and the internal choices of the various components. As for the local scheduler, we assume that the local nondeterminism of each component is solved on the basis of the local view of the history (local to that component), i.e. the projection of the history of the system on that component. In other words, each component has to make decisions based only on the history of its own execution; it cannot see anything of the other components.

5.1 Restricting Global Schedulers

We assume that the set of actions σ is divided in two parts, the secret actions S and the observable actions O. The secret actions are supposed to be invisible to the global scheduler. Formally, this can be achieved using a function sift defined as:

sift(a) = \{ \begin{matrix}τ & if a ∈ S \\ a & otherwise \end{matrix}

Then, we restrict the power of the global scheduler by forcing it to make the same

Mig: Try to link to dolev-yao decisions on paths he cannot tell apart, as formalized in the next definition.

Definition 5. Given a TPA M, a global scheduler ζ for M is admissible if for all paths σ_{1} and σ_{2} we have

t(σ_{1}) = t(σ_{2}) implies ζ(σ_{1}) = ζ(σ_{2})

where

t (q̂ ⟶^{l_{1}:a_{1}} q_{1} ⟶^{l_{2}:a_{2}} ⋯ ⟶^{l_{n}:a_{n}} q_{n+1}) =^{def} (Enabled(q_{0}), sift(a_{1}), l_{1})
(Enabled(q_{1}), sift(a_{2}), l_{2})
⋮
(Enabled(q_{n}), sift(a_{n}), l_{n})

The idea is that t sifts the information of the path that the scheduler can see. This way, since sift “hides” the secrets to the scheduler, the scheduler cannot take different decisions based on secret information.

5.2 Restricting Local Schedulers

The restriction on the local scheduler is based on the idea that a step of the component i of a system can only be based on the view that i has of the history, i.e. its own history. In order to formalize this restriction, it is convenient to introduce the concept of i-view of a path σ, or projection of σ on i, which we will denote by σ_{↾i}. We define it inductively:

(σ ⟶^{ℓ:a} μ)_{↾i} = \{ \begin{matrix}σ_{↾i} ⟶^{i:b} δ_{q_{i}} & if ℓ = \{i, j\} and μ = δ_{(A) q_{1}∥...∥q_{i}∥...∥q_{j}∥...∥q_{n}} \\ σ_{↾i} ⟶^{i:a} μ & if ℓ = i \\ σ_{↾i} & otherwise \end{matrix}

In the above definition, the first line represents the case of a synchronization step involving the component i, where we assume that the premise for i is of the form q′_{i} ⟶^{b} δ_{q_{i}}. The second line represents an interleaving step in which i is the active component. The

Cat: This is a bit of cheating. In the journal version we need to change the operational semantics so that we can retrieve the form of the premise from the conclusion

third line represents step in which the component i is idle.

The restriction to the local scheduler can now be expressed as follows:

Definition 6. Given a TPA M and a local scheduler ξ for M, we say that ξ is admissible if for all paths σ and σ′, if ξ(σ) = (ℓ, a, μ), and ξ(σ′) = (ℓ′, a′, μ′):

– if ℓ = ℓ′ = i and σ_{↾i} = σ′_{↾i}, then ξ(σ) = ξ(σ′),

– if ℓ = ℓ′ = {i, j}, σ_{↾i} = σ′_{↾i}, and σ_{↾j} = σ′_{↾j} then ξ(σ) = ξ(σ′).

A pair of compatible schedulers (ζ, ξ) for M is called admissible if both ζ and ı are admissible.

6 Safe Nondeterministic Information Hiding

In this section we define the notion of information hiding under the most general hypothesis that the nondeterminism is handled partly in a demonic way and partly in an angelic way. We assume that the demonic part is in the realm of the global scheduler, while the angelic part is controlled by the local scheduler. The motivation is that in a protocol the local components can be thought of as programs running locally in a single machine, and locally predictable and controllable, while the network can be subject to attacks that make the interactions unpredictable.

We recall that, in a purely probabilistic setting, the absence of leakage is expressed as follows (see for instance [?]). Given a purely probabilistic automaton M, and a sequence ã = a_{1}a_{2} … a_{n}, let P_{M}([ã]) represent the probability measure of all complete paths with trace ã in M. Let P be a protocol containing a variable action secr, and let s be secret actions. Let M(s) be the automaton corresponding to P [s/secr]. Define Pr(ã | s) as P_{M(s)}([ã]). Then P is leakage-free if for every observable trace ã , and for every secret s_{1} and s_{2}, we have:

Pr(ã | s_{1}) = Pr(ã | s_{2}).

In a purely nondeterministic setting, on the other hand, the absence of leakage has been characterized in the literature by the following property:

P [s_{1}/secr] ≅ P [s_{2}/secr]

where ≅ is an equivalence relation like trace equivalence, or bisimulation. As we have argued in the introduction, this definition assumes an angelic interpretation of nondeterminism.

We want to combine the above notions so to come with the case in which we have both probability and nondeterminism. Furthermore, we want to extend it to the case in which part of the nondeterminism is interpreted demonically. Let us first introduce some notation.

Let S be a system containing a variable action secr. Let s be a secret action. Let M(s) be the TPA associated to S[s/secr] and let (ζ, ξ) be a compatible pair of global and local schedulers for M(s). The probability of an observable trace ã, given s, is defined as

Pr_{ζ,ξ}(ã | s) = P_{M(s),ζ,ξ}([ã]).

The global nondeterminism is interpret demonically, and therefore we need to ensure that the conditional of an observable, given the two secrets, are calculated with respect to the same global scheduler. However, the scheduler should not be too powerful, i.e. we want to rule out the possibility that the scheduler use the secret information (i.e. be clairvoyant ) to accomplish its demonic goals.

Definition 7. A system S is leakage-free if, for every pair of secrets s_{1} and s_{2}, and every admissible scheduler ζ,

{Pr_{ζ,ξ}(ã | s_{1}) | ξ compatible withζ} = {Pr_{ζ,ξ}(ã | s_{2}) | ξ compatible withζ}.

It turns out that the safe equivalences defined in Section ?? imply the absence of leakage:

Theorem 2. Let S be a system with a variable action secr and assume that S[s_{1}/secr] ≃ S[s_{2}/secr] for every pair of secrets s_{1} and s_{2}. Then S is leakage-free.

From the above theorem and from Propositiion ??, we also have the following corollary (with the same premises as the previous theorem):

Corollary 1. If S[s_{1}/secr] ≃ S[s_{2}/secr] for every pair of secrets s_{1} and s_{2}, then S is leakage-free.

7 Conclusion