Miguel E Andrés

Catuscia Palamidessi

Peter Van Rossum

Ana Sokolova

Information Hiding in Probabilistic Concurrent Systems

Information hiding is a general concept which refers to the goal of preventing an adversary to infer secret information from the observables. Anonymity and Information Flow are examples of this notion. We study the problem of information hiding in systems characterized by the presence of randomization and concurrency. It is well known that the raising of nondeterminism, due to the possible interleavings and interactions of the parallel components, can cause unintended information leaks. One way to solve this problem is to fix the strategy of the scheduler beforehand. In this work, we propose a milder restriction on the schedulers, and we define the notion of strong (probabilistic) information hiding under various notions of observables. Furthermore, we propose a method, based on the notion of automorphism, to verify that a system satisfies the property of strong information hiding, namely strong anonymity or no-interference, depending on the context.

I. INTRODUCTION

The problem of information hiding consists in trying to prevent the adversary to infer confidential information from the observables. Instances of this issue are Anonymity and Information Flow. In both fields there is a growing interest in the quantitative aspects, see for instance [START_REF] Halpern | Anonymity and information hiding in multiagent systems[END_REF], [START_REF] Bhargava | Probabilistic anonymity[END_REF], [START_REF] Clark | Quantified interference for a while language[END_REF], [START_REF] Clarkson | Belief in information flow[END_REF], [START_REF] Chatzikokolakis | Anonymity protocols as noisy channels[END_REF], [START_REF] Smith | On the foundations of quantitative information flow[END_REF]. This is justified by the fact that often we have some a priori knowledge about the likelihood of the various secrets, and by the fact that protocols often use randomized actions to obfuscate the link between secret and observable, like in anonymity protocols such as the DC Nets [START_REF] Chaum | The dining cryptographers problem: Unconditional sender and recipient untraceability[END_REF], Crowds [START_REF] Reiter | Crowds: anonymity for Web transactions[END_REF], Onion Routing [START_REF] Syverson | Anonymous connections and onion routing[END_REF], and Freenet [START_REF] Clarke | Freenet: A distributed anonymous information storage and retrieval system[END_REF].

In a concurrent setting, like in the case of multi-agent systems, there is also another source of uncertainty, which derives from the fact that the various entities may interleave and interact in ways that are usually unpredictable, either because they depend on factors that are too complex to analyze, or because (in the case of specifications) they are implementation-dependent. This uncertainty is commonly modeled as nondeterminism.

The formal analysis of systems which exhibit probabilistic and nondeterministic behavior usually involves the use of schedulers, which are functions that select, for each path, only one possible (probabilistic) transition, thus delivering a purely probabilistic execution tree.

In the area of security, there is the problem that among all possible schedulers there are also those which take different decisions depending on the secret values, and these decisions may induce different observable behaviors, thus leaking the secret. Hence the security properties are usually violated if we consider all possible schedulers: "obviously secure" protocols are not secure anymore. This is a well known problem for which various solutions have already been proposed. We will come back to these in the "Related work" section.

A. Contribution

The main contribution of this work consists in the following:

• We define a class of partial-information schedulers, which we call admissible. These are a restricted version of the standard (full-information) schedulers. The restriction is rather flexible and has strong structural properties, which facilitate the reasoning about security properties. In short, our systems consist of parallel components with certain restrictions on the secret and nondeterministic choices.

The scheduler selects the next component (or components, in case of synchronization) for the subsequent step independently of the secret choices. We then formalize the notion of quantitative information leakage under this restricted notion of scheduler. • We propose alternative definitions to the property of strong anonymity defined in [START_REF] Bhargava | Probabilistic anonymity[END_REF]. The differences of our proposal are: (1) the system should be strongly anonymous for all admissible schedulers instead of all schedulers, and (2) we consider several variants of adversaries, namely (in increasing level of power): external adversaries, internal adversaries, and adversaries in collusion with the scheduler. Additionally, we use admissible schedulers to extend the notions of multiplicative [START_REF] Smith | On the foundations of quantitative information flow[END_REF] and additive leakage [START_REF] Braun | Quantitative notions of leakage for one-try attacks[END_REF] to the case of concurrent system. • We propose a sufficient technique to prove probabilistic strong anonymity, and probabilistic noninterference, based on automorphisms. The idea is the following: In the purely nondeterministic setting, the strong anonymity of a system is often defined and proved as follows: take two users A and B and a trace in which user A is 'the culprit'. Now find a trace that looks the same to the adversary, but in which user B is 'the culprit' [START_REF] Halpern | Anonymity and information hiding in multiagent systems[END_REF], [START_REF] Garcia | Provable anonymity[END_REF], [START_REF] Mauw | A formalization of anonymity and onion routing[END_REF], [START_REF] Hasuo | Probabilistic anonymity via coalgebraic simulations[END_REF]. This new trace is often most easily obtained by switching the behavior of A and B. Non-interference can be proved in the same way (where A and B are high information and the trace is the low information).

In this work, we develop this technique for systems where probability and nondeterminism coexist, and we need to cope with the restrictions on the schedulers. We formalize the notion of switching the behaviors of A and B in terms of the existence of an automorphism between A and B, and then we show that the existence of an automorphism implies strong anonymity. • We use the Dining Cryptographers [START_REF] Chaum | The dining cryptographers problem: Unconditional sender and recipient untraceability[END_REF] to illustrate the problem caused by full-information schedulers, our solution based on admissible schedulers, and our proving technique.

B. Related Work

The problem of the full-information scheduler has already been extensively investigated in literature. The works [START_REF] Canetti | Task-structured probabilistic i/o automata[END_REF] and [START_REF] Canetti | Time-bounded task-PIOAs: A framework for analyzing security protocols[END_REF] consider probabilistic automata and introduce a restriction on the scheduler to the purpose of making them suitable to applications in security. Their approach is based on dividing the actions of each component of the system in equivalence classes (tasks). The order of execution of different tasks is decided in advance by a so-called task scheduler. The remaining nondeterminism within a task is resolved by a second scheduler, which models the standard adversarial scheduler of the cryptographic community. This second entity has limited knowledge about the other components: it sees only the information that they communicate during execution. Their notion of task scheduler is similar to our notion of admissible scheduler, but more restricted since the strategy of the task scheduler is decided entirely before the execution.

The work in [START_REF] Chatzikokolakis | Making random choices invisible to the scheduler[END_REF], [START_REF] Chatzikokolakis | Bisimulation for demonic schedulers[END_REF] is similar to ours in spirit, but in a sense dual from a technical point of view. Instead of defining a restriction on the class of schedulers, they provide a way to specify that a choice is transparent to the scheduler. They achieve this by introducing labels in process terms, used to represent both the states of the execution tree and the next action or step to be scheduled. They make two states indistinguishable to schedulers, and hence the choice between them private, by associating to them the same label. Furthermore, their "equivalence classes" (schedulable actions with the same label) can change dynamically, because the same action can be associated to different labels during the execution.

In [START_REF] Alvim | Safe Equivalences for Security Properties[END_REF] we extend the framework presented here by allowing internal nondeterminism and adding a second type of scheduler to resolve it, to the aim of investigating angelic vs demonic nondeterminism in equivalence-based properties.

The fact that full-information schedulers are unrealistic has also been observed in fields other than security. First attempts used restricted schedulers in order to obtain rules for compositional reasoning [START_REF] De Alfaro | Compositional methods for probabilistic systems[END_REF]. The justification for those restricted schedulers is the same as for ours, namely, that not all information is available to all entities in the system. However that work considers a synchronous parallel composition, so the setting is rather different from ours. Later on, it was shown that model checking is unfeasible in its general form for the restricted schedulers in [START_REF] De Alfaro | Compositional methods for probabilistic systems[END_REF] (see [START_REF] Giro | Quantitative model checking revisited: Neither decidable nor approximable[END_REF] and, more recently, [START_REF] Giro | Undecidability results for distributed probabilistic systems[END_REF]). Despite of undecidability, not all results concerning such schedulers have been negative as, for instance, the technique of partial-order reduction can be improved by assuming that schedulers can only use partial information [START_REF] Giro | Partial order reduction for probabilistic systems: A revision for distributed schedulers[END_REF].

To the best of our knowledge, this is the first work using automorphisms as a sound proof technique to prove strong anonymity and non-interference. The closest line of work we are aware of is in the field of model checking, where isomorphisms have been used to identify symmetries in the system and exploited to alleviate the state space explosion (see for instance [START_REF] Kwiatkowska | Symmetry reduction for probabilistic model checking[END_REF]).

C. Plan of the paper

Looking ahead, after reviewing some preliminaries (Section II) we formalize the notions of systems and components (Section III). In Section IV we present admissible schedulers. We then formalize the notions of internal and external strong anonymity in a probabilistic and nondeterministic setting for admissible schedulers (Section V). Finally, we turn our attention to the verification problem, in Section VI we present a strong-anonymity proving technique based on automorphisms. We conclude and outline some future work in Section VII.

II. PRELIMINARIES

In this section we gather preliminary notions and results related to probabilistic automata [START_REF] Segala | Probabilistic simulations for probabilistic processes[END_REF], [START_REF] Segala | Modeling and Verification of Randomized Distributed Real-Time Systems[END_REF].

A. Probabilistic automata

A function µ : Q → [0, 1] is a discrete probability distri- bution on a set Q if q∈Q µ(q) = 1.
The set of all discrete probability distributions on Q is denoted by D(Q).

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)). Here P(X) is the set of all subsets of X.

If θ(q) = ∅, then q is a terminal state. We write q→µ for µ ∈ θ(q), q ∈ Q. Moreover, we write q a →r for q, r ∈ Q whenever q→µ and µ(a, 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. A path in a probabilistic automaton is a sequence σ = q 0 a1 → q 1 a2 → • • • where q i ∈ Q, a i ∈ Σ and q i ai+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. A cycle is a path σ such that last (σ) = first(σ). Let Paths q (M ) denote the set of all paths, Paths ⋆ q (M ) the set of all finite paths, and 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 Σ ′ .

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 (σ) µ(a, q ′ ), where last (σ) → µ.

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 P q.

A (full-information) scheduler for a probabilistic automaton M is a function ζ : Paths ⋆ (M ) → (D(Σ×Q)∪{⊥}) such that for all finite paths σ, if θ(last (σ)) = ∅ then ζ(σ) ∈ θ(last (σ)), and ζ(σ) = ⊥ otherwise. Hence, a scheduler ζ selects one of the available transitions in each state, and determines therefore a fully probabilistic automaton, obtained by pruning from M the alternatives that are not chosen by ζ. Note that a scheduler is history dependent since it can take different decisions for the same state s according to the past evolution of the system.

B. Noisy Channels

This section briefly recalls the notion of noisy channels from Information Theory [START_REF] Cover | Elements of Information Theory[END_REF].

A noisy channel is a tuple

C def = (X , Y, P (•|•))
where X = {x 1 , x 2 , . . . , x n } is a finite set of input values, modeling the secrets of the channel, and Y = {y 1 , y 2 , . . . , y m } is a finite set of output values, the observables of the channel. For x i ∈ X and y j ∈ Y, P (y j | x i ) is the conditional probability of obtaining the output y j given that the input is x i . These conditional probabilities constitute the so called channel matrix, where P (y j |x i ) is the element at the intersection of the i-th row and the j-th column. For any input distribution P X on X , P X and the channel matrix determine a joint probability P ∧ on X × Y, and the corresponding marginal probability P Y on Y (and hence a random variable Y ). P X is also called a priori distribution and it is often denoted by π. The probability of the input given the output is called a posteriori distribution.

C. Information leakage

We recall here the definitions of multiplicative leakage proposed in [START_REF] Smith | On the foundations of quantitative information flow[END_REF], and of additive leakage proposed in [3]1 . We assume given a noisy channel C = (X , Y, P (•|•)) and a random variable X on X . The a priori vulnerability of the secrets in X is the probability of guessing the right secret, defined as V(X) def = max x∈X P X (x). The rationale behind this definition is that the adversary's best bet is on the secret with highest probability. The a posteriori vulnerability of the secrets in X is the probability of guessing the right secret, after the output has been observed, averaged over the probabilities of the observables. The formal definition is

V(X | Y) def = y∈Y P Y (y) max x∈X P (x | y). Again, this
definition is based on the principle that the adversary will choose the secret with the highest a posteriori probability. Note that, using Bayes theorem, we can write the a posteriori vulnerability in terms of the channel matrix and the a priori distribution, or in terms of the joint probability:

V(X | Y) = y∈Y max x∈X (P (y | x)P X (x)) = y∈Y max x∈X P ∧ (x, y) The multiplicative leakage is L × (C, P X ) def = V(X|Y) V(X) whereas the additive leakage is L + (C, P X ) def = V(X|Y) -V(X).

D. Dining Cryptographers

This problem, described by Chaum in [START_REF] Chaum | The dining cryptographers problem: Unconditional sender and recipient untraceability[END_REF], involves a situation in which three cryptographers are dining together. At the end of the dinner, each of them is secretly informed by a central agency (master) whether he should pay the bill, or not. So, either the master will pay, or one of the cryptographers will be asked to pay. The cryptographers (or some external observer) would like to find out whether the payer is one of them or the master. However, if the payer is one of them, they also wish to maintain anonymity over the identity of the payer.

A possible solution to this problem, described in [START_REF] Chaum | The dining cryptographers problem: Unconditional sender and recipient untraceability[END_REF], is that each cryptographer tosses a coin, which is visible to himself and his neighbor to the left. Each cryptographer observes the two coins that he can see and announces agree or disagree. If a cryptographer is not paying, he will announce agree if the two sides are the same and disagree if they are not. The paying cryptographer will say the opposite. It can be proved that if the number of disagrees is even, then the master is paying; otherwise, one of the cryptographers is paying. Furthermore -for the case of fair coins, if one of the cryptographers is paying, then neither an external observer nor the other two cryptographers can identify, from their individual information, who exactly is paying. The Dining Cryptographers (DC) will be a running example through the paper.

III. 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 purely probabilistic processes, that we call components. They are equipped with a unique identifier, that we call tag, or label, of the component. Note that, because of the restriction that the components are fully deterministic2 , nondeterminism is generated only from the interleaving of the parallel components. Furthermore, because of the uniqueness of the tags, each transition from a node is associated to a different tag / pair of two tags (one in case only one component makes a step, and two in case of a synchronization step among two components).

A. Tagged Probabilistic Automata

We now formalize the notion of TPA.

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, or labels, • Σ is a set of actions, • q ∈ Q is the initial state, • θ : Q → P(L × D(Σ × Q)) is a transition function.
with the additional requirement that for every q ∈ Q and every ℓ ∈ L there is at most one

µ ∈ D(Σ × Q) such that (ℓ, µ) ∈ θ(q).
A path for a TPA is a sequence σ = q 0 l1,a1

-→ q 1 l2,a2 -→ q 2 • • • .
In this way, the process with identifier l i induces the system to move from q i-1 to q i performing the action a i , and it does so with probability µ li (a i , q i ), where µ li is the distribution associated to the choice made by the component l i . Finite paths and complete paths are defined in a similar manner.

In a TPA, the scheduler's choice is determined by the choice of the tag. We will use enab(q) to denote the tags of the components that are enabled to make a transition. Namely,

enab(q) def = {ℓ ∈ L | ∃ µ ∈ D(Σ × Q) : (ℓ, µ) ∈ θ(q)} (1)
We assume that the scheduler is forced to select a component among those which are enabled, i.e., 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 [START_REF] Segala | Probabilistic simulations for probabilistic processes[END_REF]. 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 which are possible from the last state.

Definition 2. A scheduler for a TPA M = (Q, L, Σ, q, θ) is a function ζ : Paths ⋆ (M ) → (L ∪ {⊥}) such that for all finite paths σ, ζ(σ) ∈ enab(last (σ)) if enab(last (σ)) = ∅ and ζ(σ) = ⊥ otherwise.

B. Components

To specify the components we use a sort of probabilistic version of CCS [START_REF] Milner | Communication and Concurrency[END_REF], [START_REF] Milner | Communicating and mobile systems: the π-calculus[END_REF]. We assume a set of secret actions Σ S with elements s, s 1 , s 2 , • • • , and a disjoint set of observable actions Σ O with elements a, a 1 , a 2 , • • • . Furthermore we have communication actions, which are also observable, of the form c(x) (receive x on channel c, where x is a formal parameter), or c v (send v on channel c, where v is a value on some domain V ). Sometimes we need only to synchronize without transmitting any value, in which case we will use simply c and c. We denote the set of channel names by C.

A component q is specified by the following grammar:

Components q ::= 0 termination | a.q observable prefix | i p i : q i blind choice | i p i : s i .q i secret choice | if x = v then q 1 else q 2 conditional | A process call Observables a ::= c | c simple synchronization | c(x) | c v synchronization

and communication

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. When no confusion arises, we use simply + for a binary choice. The process call A is a simple process identifier. For each of them, 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.

We remark once again that each component contains only probabilistic and sequential constructs. In particular, there is no internal parallelism. Hence each component corresponds to a purely probabilistic automaton (apart from the input nondeterminism, which disappears in the definition of a system), as described by the operational semantics below.

Components' semantics:

The operational semantics consists of probabilistic transitions of the form q→µ where q ∈ Q is a process, and µ ∈ D(Σ × Q) is a distribution on actions and processes. They are specified by the following rules:

PRF1 v ∈ V c(x).q → δ(c(v), q[v/x]) PRF2 a.q → δ(a, q) if a = c(x) INT i p i : q i → • i p i • δ(τ, q i ) SECR i p i : s i .q i → • i p i • δ(s i , q i ) CALL q → µ A → µ if A def = q CND1 if v = v then q 1 else q 2 → δ(τ, q 1 ) CND2 v = v ′ if v = v ′ then q 1 else q 2 → δ(τ, q 2 ) • i p i • µ i is the distribution µ such that µ(x) = i p i µ i (x).
We use δ(x) to represent the delta of Dirac, which assigns probability 1 to x. The silent action, τ , is a special action different from all the observable and the secret actions. q[v/x] stands for the process q in which any occurrence of x has been replaced by v. To shorten the notation, in the examples throughout the paper, we omit writing explicit termination, i.e., we omit the symbol 0 at the end of a term.

C. Systems

A system consists of n processes (components) in parallel, and restricted at the top-level on the set of channel names C:

(C) q 1 q 2 • • • q n .
The restriction on C enforces synchronization (and possibly communication) on the channel names belonging to C, in accordance with the CCS spirit. Since C is the set of all channels, all of them are forced to synchronize. This is to eliminate, at the level of systems, the nondeterminism generated by the rule for the receive prefix, PRF1.

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 ℓ → µ where µ ∈ (D(Σ × Q)) and ℓ ∈ L is either the identifier of the component which makes the move, or a two-element set of identifiers representing the two partners of a synchronization. The following two rules (INT) and (SYNC/COMM) provide the operational semantics rules in the case of interleaving and synchronisation/communication, respectively.

(INT) If a j ∈ C q i → • j p j • δ(a j , q ij ) (C) q 1 • • • q i • • • q n i → • j p j • δ(a j , (C) q 1 • • • q ij • • • q n )
where i indicates the tag of the component making the step.

(SYNC/COMM)

q i → δ(c v , q ′ i ) q j → δ(c(v), q ′ j ) (C) q 1 • • • q i • • • q n {i,j} -→ δ(τ, (C) 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. For simplicity we write i,j -→ instead of {i,j} -→. The rule for synchronization without communication is similar, the only difference is that we do not have v and (v) in the actions. Note that c can only be an observable action (neither a secret nor τ ), by the assumption that channel names can only be observable actions.

We note that both interleaving and synchronization rules generate nondeterminism. The only other source of nondeterminism is PRF1, the rule for a receive prefix c(x). However the latter is not real nondeterminism: it is introduced in the semantics of the components but it disappears in the semantics of the systems, given that the channel c is restricted at the toplevel. In fact the restriction enforces communication, and when communication takes place, only the branch corresponding to the actual value v transmitted by the corresponding send action is maintained, all the others disappear.

Proposition 1. The operational semantics of a system is a TPA with the following characteristics:

(a) Every step q ℓ → µ is either a blind choice: µ = • i p i • δ(τ, q i ), or a secret choice: µ = • i p i • δ(s i , q i ), or a delta of Dirac: µ = δ(α, q ′ ) with α ∈ Σ O or α = τ . (b) If q ℓ → µ and q ℓ → µ ′ then µ = µ ′ .
Example 1. We now present the components for the Dining Cryptographers using the introduced syntax. They correspond to Figure 1 and to the automata depicted in Figure 3. As announced before, we omit the symbol 0 for explicit termination at the end of each term. The secret actions s i represent the choice of the payer. The operators ⊕, ⊖ represent the sum modulo 2 and the difference modulo 2, respectively. The test i == n returns 1 (true) if i = n, and 0 otherwise. The set of restricted channel names is The operation pay ⊕ coin 1 ⊕ coin 2 in Figure 2 is syntactic sugar, it can be defined using the if-then-else operator. Note that, in this way, if a cryptographer is not paying (pay = 0), then he announces 0 if the two coins are the same (agree) and 1 if they are not (disagree).

C = {c 0,0 , c 0,1 , c 1,1 , c 1,2 , c 2,0 , c 2,2 , m 0 , m 1 , m 2 }. Master def = p : m 0 0 . m 1 0 . m 2 0 + (1 -p) : 2 i=0 p i : s i . m 0 i == 0 . m 1 i == 1 . m 2 i == 2 Crypt i def = m i (pay ) . c i,i (coin 1 ) . c i,i⊕1 (coin 2 ) . out i pay ⊕ coin 1 ⊕ coin 2 Coin i def = 0.5 : ci,i 0 . ci⊖1,i 0 + 0.5 : ci,i 1 . ci⊖1,i 1 System def = (C ) Master 2 i=0 Crypt i 2 i=0 Coin i

IV. ADMISSIBLE SCHEDULERS

We now introduce the class of admissible schedulers.

Master • 1-p p Ô Ô • p0:s0 × × p1:s1 / / / # # / / / p2:s2 G G 5 5 G G G G G G G G • m 0 0
( ( : : : : : : :

• m0 1 • m0 0 • m0 0 • m1 0 • m1 1 • m1 0 • m2 0 # # / / / / / / • m 2 1
{ { w w w w w w w w w

• Coin i • τ 1 2 1 2 • ci,i 0 • ci,i 1 • ci⊖1,i 0 ' ' • ci⊖1,i 1 Ó Ó • Crypt i • mi(0) Ö Ö mi(1) $ $ • ci,i(0) ci,i(1) 8 8 L L L L L L L L L L L • ci,i(0) ci,i (1)
y y r r r r r r r r r r r

• ci,i⊕1(0) ci,i⊕1(1) 8 8 L L L L L L L L L L L • ci,i⊕1(0) ci,i⊕1 (1)
y y r r r r r r r r r r r

• outi(0) 4 4 • outi(1)
| | • Fig. 3. Dining Cryptographers Automata Standard (full-information) schedulers have access to all the information about the system and its components, and in particular the secret choices. Hence, such schedulers can leak secrets by making their decisions depend on the secret choice of the system. This is the case with the Dining Cryptographers protocol of Section II-D: among all possible schedulers for the protocol, there are several that leak the identity of the payer. In fact the scheduler has the freedom to decide the order of the announcements of the cryptographers (interleaving), so a scheduler could choose to let the payer announce lastly. In this way, the attacker learns the identity of the payer simply by looking at the interleaving of the announcements.

A. The screens intuition

Let us first describe admissible schedulers informally. As mentioned in the introduction, admissible schedulers can base their decisions only on partial information about the evolution of the system, in particular admissible schedulers cannot base their decisions on information concerned with the internal behavior of components (such as secret choices).

We follow the subsequent intuition: admissible schedulers are entities that have access to a screen with buttons, where each button represents one (current) available option. At each point of the execution the scheduler decides the next step among the available options (by pressing the corresponding button). Then (if any) the output of the selected component becomes available to the scheduler and the screen is refreshed with the new available options (the ones corresponding to the system after making the selected step). We impose that the scheduler can base its decisions only on such information, namely: the screens and outputs he has seen up to that point of the execution (and, of course, the decisions he has made). Example 2. Consider S def = ({c 1 , c 2 }) q 1 q 2 q 3 , where

q 1 def = 0.5 : s 1 .c 1 .c 2 + 0.5 : s 2 .c 1 .c 2 , q 2 def = c 1 .(0.5 : a 1 + 0.5 : b 1 ), q 3 def = c 2 .(0.5 : a 2 + 0.5 : b 2 ).
Figure 4 shows the sequence of screens corresponding to a particular sequence of choices taken by the scheduler 3 . Interleaving and communication options are represented by yellow and red buttons, respectively. An arrow between two screens represents the transition from one to the other (produced by the scheduler pressing a button), additionally, the decision taken by the scheduler and corresponding outputs are depicted above each arrow. Note that this system has exactly the same problem as the DC protocol: a full-information scheduler could reveal the secret by basing the interleaving order (q 2 first or q 3 first) on the secret choice of the component q 1 . However, the same does not hold anymore for admissible schedulers (the scheduler cannot deduce the secret choice by just looking at the screens and outputs). This is also the case for the DC protocol, i.e., admissible schedulers cannot leak the secret of the protocol.

B. The formalization

Before formally defining admissible schedulers we need to formalize the ingredients of the screens intuition. The buttons on the screen (available options) are the enabled options given by the function enab (see [START_REF] Alvim | Safe Equivalences for Security Properties[END_REF]), the decision made by the scheduler is the tag of the selected enabled option, observable actions are obtained by sifting the secret actions to the schedulers by means of the following function:

sift (α) def = α if α ∈ Σ O ∪ {τ }, τ if α ∈ Σ S .
The partial information of a certain evolution of the system is given by the map t defined as follows.

Definition 3. Let q ℓ1,α1 -→ • • • ℓn,αn
-→ q n+1 be a finite path of the system, then we define t as:

t q ℓ1,α1 -→ • • • ℓn,αn -→ q n+1 def = (enab(q), ℓ 1 , sift (α 1 ))
. . .

(enab(q n ), ℓ n , sift (α n )).
Finally, we have all the ingredients needed to define admissible schedulers.

Definition 4 (Admissible schedulers). A scheduler ζ is admis

- sible if for all σ, σ ′ ∈ Paths ⋆ t(σ) = t(σ ′ ) implies ζ(σ) = ζ(σ ′ ).
In this way, admissible schedulers are forced to take the same decisions on paths that they cannot tell apart. Note that this is a restriction on the original definition of (fullinformation) schedulers where t is the identity map over finite paths (and consequently the scheduler is free to choose differently).

V. INFORMATION-HIDING PROPERTIES IN PRESENCE OF

NONDETERMINISM

In this section we revise the standard definition of information flow and anonymity in our framework of controlled nondeterminism.

We first consider the notion of adversary. We consider three possible notions of adversaries, increasingly more powerful.

A. Adversaries

External adversaries: Clearly, an adversary should be able, by definition, to see at least the observable actions. For an adversary external to the system S, it is natural to assume that these are also the only actions that he is supposed to see. Therefore, we define the observation domain, for an external adversary, as the set of the (finite) sequences of observable actions, namely:

O e def = Σ * O . Correspondingly, we need a function that extracts the observables from the executions:

t e : Paths ⋆ (S) → O e defined as t e q 0 ℓ1,α1 -→ • • • ℓn,αn -→ q n+1 def = sieve(α 1 ) • • • sieve(α n ) where sieve(α) def = α if α ∈ Σ O , ǫ if α ∈ Σ S ∪ {τ }.
Internal adversaries: An internal adversary may be able to see, besides the observables, also the intearleaving and synchronizations of the various components, i.e. which component(s) are active, at each step of the execution. Hence it is natural to define the observation domain, for an internal adversary, as the sequence of pairs of observable action and tag (i.e. the identifier(s) of the active component(s)), namely:

O i def = (L × (Σ O ∪ {τ })) * .
Correspondingly, we need a function that extracts the observables from the executions:

t i : Paths ⋆ (S) → O i defined as t i q 0 ℓ1,α1 -→ • • • ℓn,αn -→ q n+1 def = (ℓ 1 , sieve(α 1 )) • • • (ℓ n , sieve(α n )).
Note that in this definition we could have equivalently used sift instead than sieve.

Adversaries in collusion with the scheduler: Finally, we consider the case in which the adversary is in collusion with the scheduler, or possibly the adversary is the scheduler, like in the Dolev-Yao model. Here the observation domain coincides with the one of the scheduler:

O s def = (P(L) × L × (Σ O ∪ {τ })) * .
The corresponding function

t s : Paths ⋆ (S) → O s
is defined as the one of the scheduler, i.e. t s = t.

B. Information leakage

In Information Flow and Anonymity there is a converging consensus for formalizing the notion of leakage as the difference or the ratio between the a priori uncertainty that the adversary has about the secret, and the a posteriori uncertainty, that is, the residual uncertainty of the adversary once it has seen the outcome of the computation. The uncertainty can be measured in different ways. One popular approach is the information-theoretic one, according to which the system is seen as a noisy channel between the secret inputs and the observable output, and uncertainty corresponds to the Shannon entropy of the system (see preliminaries, section B). In this approach, the leakage is represented by the so-called mutual information, which expresses the correlation between the input and the output.

The above approach, however, has been recently criticized by Smith [START_REF] Smith | On the foundations of quantitative information flow[END_REF], who has argued that Shannon entropy is not suitable to represent the security threats in the typical case in which the adversary is interested in figuring out the the secret in one-try attempt, and he has proposed to use Rényi's min entropy instead, or equivalently, the average probability of succeeding. This leads to interpret the uncertainty in terms of the notion of vulnerability defined in the preliminaries, section C. The corresponding notion of leakage, in the pure probabilistic case, have been investigated in [START_REF] Smith | On the foundations of quantitative information flow[END_REF] (multiplicative case) and in [START_REF] Braun | Quantitative notions of leakage for one-try attacks[END_REF] (additive case).

Here we adopt the vulnerability-based approach to define the notion of leakage in our probabilistic and nondeterministic context. The Shannon-entropy-based approach could be extended to our context as well, because in both cases we only need to specify how to determine the conditional probabilities which constitute the channel matrix, and the marginal probabilities that constitute the input and the output distribution.

We will denote by S the random variable associated to the set of secrets S = Σ S , and by O x the random variables associated to the set of observables O x , where x ∈ {e, i, s}. So, O x represents the observation domains for the various kinds of adversaries defined above.

Our results require some structural properties for the system: we assume that there is a single component in the system containing a secret choice and this component contains a single secret choice. This hypothesis is general enough to allow expressing protocols like the Dining Cryptographers, Crowds, voting protocols, etc., where the secret is chosen only once. Assumption 1. A system contains exactly one component with a syntactic occurrence of a secret choice, and such a choice does not occur in the scope of any recursive call.

Note that the assumption implies that the choice appears exactly once in the operational semantics of the component. It would be possible to relax the assumption and allow more than one secret choice in a component, as long as there are no observable actions between the secret choices. But for the sake of simplicity in this paper we impose the more restrictive requirement. As a consequence, we have that the operational semantics of systems satisfies the following property: Proposition 2. If q ℓ → µ and q ′ ℓ ′ → µ ′ are both secret choices, then ℓ = ℓ ′ and there exist p i 's, q i 's and q ′ i 's such that:

µ = ⊙ i p i • δ(s i , q i ) and µ ′ = ⊙ i p i • δ(s i , q ′ i )
i.e., µ and µ ′ differ only for the continuation states.

Given a system, each scheduler ζ determines a fully probabilistic automaton, and, as a consequence, the probabilities

P ζ (s, o) def = P ζ      σ | σ ∈ Paths ⋆ (S), t x (σ) = o, secr (σ) = s     
P ζ (s) = P ζ (s,o) P(s) .
Given a scheduler ζ, the multiplicative leakage can be defined as L × (C x ζ , P S ), while the additive leakage can be defined as L + (C x ζ , P S ) where P S is the a priori distribution on the set of secrets (see preliminaries, section C). However, we want a notion of leakage independent from the scheduler, and therefore it is natural to consider the worst case over all possible admissible schedulers. Definition 6 (x-leakage). Let x ∈ {e, i, s}. Given a system, the multiplicative leakage is defined as

ML × (C x ζ , P S ) def = max ζ∈Adm L × (C x ζ , P S ),
while the additive leakage is defined as

ML + (C x ζ , P S ) def = max ζ∈Adm L + (C x ζ , P S ),
where Adm is the class of admissible schedulers defined in the previous section.

We have that the classes of observables e, i, and s determine an increasing degree of leakage:

C. Strong anonymity (revised)

We consider now the situation in which the leakage is the minimum for all possible admissible schedules. In the purely probabilistic case, we know that the minimum possible multiplicative leakage is 1, and the minimum possible additive one is 0. We also know that this is the case for all possible input distributions if and only if the capacity of the channel matrix is 0, which corresponds to the case in which the rows of the matrix are all the same. This corresponds to the notion of strong probabilistic anonymity defined in [START_REF] Bhargava | Probabilistic anonymity[END_REF]. In the framework of information flow, it would correspond to probabilistic noninterference. Still in [START_REF] Bhargava | Probabilistic anonymity[END_REF], the authors considered also the extension of this notion in presence of nondeterminism, and required the condition to hold under all possible schedulers. This is too strong in practice, as we have argued in the introduction: in most cases we can build a scheduler that leaks the secret by changing the interleaving order. We therefore tune this notion by requiring the condition to hold only under the admissible schedulers. Definition 7 (x-strongly anonymous). Let x ∈ {e, i, s}. We say that a system is x-strongly-anonymous if for all admissible schedulers ζ we have

P ζ (o | s 1 ) = P ζ (o | s 2 )
for all s 1 , s 2 ∈ Σ S , and o ∈ O x .

The following corollary is an immediate consequence of previous proposition.

Corollary 8.

1) If a system is s-strongly-anonymous, then it is also istrongly-anonymous. 2) If a system is i-strongly-anonymous, then it is also estrongly-anonymous.

The converse of point (2), in previous the corollary, does not hold, as shown by the following example:

s 2 : c 2 ) Q def = c 1 : o T def = c 2 : o.
It is easy to check that S is e-strongly anonymous but not i-strongly anonymous, showing that (as expected) internal adversaries can "distinguish more" than external adversaries.

On the contrary, for point (1) of Corollary 8, also the other direction holds: Proposition 5. A system is s-strongly-anonymous if and only if it is e-strongly-anonymous.

VI. ON THE VERIFICATION OF STRONG ANONYMITY: A PROVING TECHNIQUE BASED ON AUTOMORPHISMS

As mentioned in the introduction, several problems involving restricted schedulers have been shown undecidable (including computing maximum/minimum probabilities for the case of standard model checking [START_REF] Giro | Quantitative model checking revisited: Neither decidable nor approximable[END_REF], [START_REF] Giro | Undecidability results for distributed probabilistic systems[END_REF]). These results are discouraging in the aim to find algorithms for verifying strong anonymity/non-interference using our notion of admissible schedulers (and most definitions based on restricted schedulers). Despite the fact that the problem seems to be undecidable in general, in this section we present a sufficient (but not necessary) anonymity proving technique: we show that the existence of automorphisms between pair of secrets implies strong anonymity.

A. The proving technique

In practice proving anonymity often happens in the following way. Given a trace in which user A is the 'culprit', we construct an observationally equivalent trace in which user B is the 'culprit' [START_REF] Halpern | Anonymity and information hiding in multiagent systems[END_REF], [START_REF] Garcia | Provable anonymity[END_REF], [START_REF] Mauw | A formalization of anonymity and onion routing[END_REF], [START_REF] Hasuo | Probabilistic anonymity via coalgebraic simulations[END_REF]. This new trace is typically obtained by 'switching' the behavior of users A and B. We formalize this idea by using the notion of automorphism, cf. e.g. [START_REF] Rutten | Universal coalgebra: A theory of systems[END_REF]. Definition 9 (Automorphism). Given a TPA (Q, L, Σ, q, θ) we say that a bijection f : Q → Q is an automorphism if it satisfies f (q) = q and q ℓ → ⊙ i p i • δ(α i , q i ) ⇐⇒ f (q) ℓ → ⊙ i p i • δ(α i , f (q i )).

In order to prove anonymity it is enough (but not necessary) to prove that the behaviors of any two 'culprits' can be exchanged without the adversary noticing. We will express this in the Theorem 1 by means of the existence of automorphisms that exchange a given pair of secret s i and s j .

Our proving technique requires Assumption 1. Before presenting the main theorem of this section we need to introduce one last definition. Let S = (C) q 1 || • • • || q n be a system and M its corresponding TPA. We define M τ as the automaton obtained after "hiding" all the secret actions of M . The idea is to replace every occurrence of a secret s in M by the silent action τ . Note that this can be formalized by replacing the secret choice by a blind choice in the corresponding component q i of the system S.

We can now state the relation between automorphisms and strong anonymity.

Theorem 1. Let S be a system that satisfies Assumption 1 and M its tagged probabilistic automaton. If for every pair of secrets s i , s j ∈ Σ S there exists an automorphism f of M τ such that for any state q we have q ℓ,si -→ M q ′ =⇒ f (q) ℓ,sj -→ M f (q ′ ), then S is s-strongly-anonymous.

Note that, since s-strong anonymity implies i-strong anonymity and e-strong anonymity, the existence of such an automorphism implies all the notions of strong anonymity presented in this work. Proposition 6. The converse does not hold, i.e. strong anonymity does not imply the existence of automorphisms.

We now show that the definition of x-strong-anonymity is independent of the particular distribution over secrets, i.e., if a system is x-strongly-anonymous for a particular distribution over secrets, then it is x-strongly-anonymous for all distributions over secrets.

Theorem 2. Consider a system S = (C) q 1 • • • q i • • • q n . Let q i be the component which contains the secret choice, and assume that it is of the form j p j : s j . q j . Consider now the system S ′ = (C) q 1 • • • q ′ i • • • q n , where q ′ i is identical to q i except for the secret choice, which is replaced by j p ′ j : s j . q j . Then we have that: 1) For every s i , s j there is an automorphism on S satisfying the assumption of Theorem 1 if and only if the same holds for S ′ . 2) S is x-strongly-anonymous if and only if S ′ is x-stronglyanonymous. Note: 1) does not imply 2), because in principle neither S not S ′ may have the automorphism, and still one of the two could be strongly anonymous.

B. An Application: Dining Cryptographers

Now we show how to apply the proving technique presented in this section to the Dining Cryptographers protocol. Concretely, we show that there exists an automorphism f exchanging the behavior of the Crypt 0 and Crypt 1 ; by symmetry, the same holds for the other two combinations.

  The work of Catuscia Palamidessi has been partially supported by the project ANR-09-BLAN-0169-01 PANDA and by the INRIA DRI Equipe Associée PRINTEMPS.

Fig. 1 .

 1 Fig. 1. Chaum's system for the Dining Cryptographers ([9])

Fig. 2 .

 2 Fig. 2. Dining Cryptographers CCS

Fig. 4 .

 4 Fig. 4. Screens intuition

Proposition 4 .

 4 Given a system, for the multiplicative leakage we have ML × (C e ζ , P S ) ≤ ML × (C i ζ , P S ) ≤ ML × (C s ζ , P S ). Similarly for the additive leakage.

Example 3 .

 3 Consider the system S def = ({c 1 , c 2 }) P || Q || T where P def = (0.5 : s 1 : c 1 )+(0.5 :

  for each secret s ∈ S and observable o ∈ O x , where x ∈ {e, i, s}. Here secr is the map from paths to their secret action. From these we can derive, in standard ways, the marginal probabilities P ζ (s), P ζ (o), and the conditional probabilitiesP ζ (o | s).We have that the probabilities of the secrets are actually independent from the scheduler: Given a system, for everypair of schedulers ζ and ζ ′ we have that P ζ (s) = P ζ ′ (s), for every secret s. Because of the previous proposition, we can omit ζ in P ζ . Let x ∈ {e, i, s}. Given a system and a scheduler ζ, the corresponding channel matrix C x ζ has rows indexed by s ∈ S and columns indexed by o ∈ O x . The value in (s, o) is given by P ζ (o | s)

	nel, whose matrix is determined by the conditional probabili-ties as follows: Proposition 3. Every scheduler leads to a (generally different) noisy chan-Definition 5. def = P ζ (s,o)

The notion proposed by Smith in[START_REF] Smith | On the foundations of quantitative information flow[END_REF] was given in a (equivalent) logarithmic form, and called simply leakage. For uniformity sake we use here the terminology and formulation of[START_REF] Braun | Quantitative notions of leakage for one-try attacks[END_REF].

In[START_REF] Alvim | Safe Equivalences for Security Properties[END_REF] we extend our framework by allowing nondeterministic choices in the components, and we use an additional scheduler to handle such "internal" nondeterminism.

The transitions from screens

and

represent 2 steps each (for simplicity we omit the τ -steps generated by blind choices)

Acknowledgement

The authors wish to thank Flavio Garcia, Pedro D'Argenio, Sergio Giro, and Mariëlle Stoelinga for useful comments on an earlier version of this paper, as well as the anonymous reviewers for thoroughly reading the paper and providing thoughtful recommendations.

( ( : : : : : : : Also consider the identity automorphism on Crypt i (for i = 0, 1, 2) and on Coin i (for i = 0, 2). It is easy to check that the product of these seven automorphisms is an automorphism for Crypt 0 and Crypt 1 .

VII. CONCLUSION AND FUTURE WORK

We have defined a class of partial-information schedulers which can only base their decisions on the information they have available. In particular they cannot base their decisions on the internal behavior of the components.

We have used admissible schedulers to resolve nondeterminism in a realistic way, and to tune the definition of strong anonymity proposed in [START_REF] Bhargava | Probabilistic anonymity[END_REF].

We have presented a technique to prove the various definitions of strong anonymity proposed in the paper. This is particularly interesting considering that many problems related to restricted schedulers have been shown to be undecidable. In particular we have shown how to use the technique to prove that the DC protocol is strongly anonymous when considering admissible schedulers, in contrast to the situation when considering full-information schedulers.

We plan to investigate the decidability problem for the various definitions of strong anonymity we have proposed. Another interesting direction for future work is to extend well known isomorphism-checking algorithms and tools (see [START_REF] Foggia | A performance comparison of five algorithms for graph isomorphism[END_REF] for a survey) to our setting in order to verify automatically strong anonymity (in case an automorphism exists -recall that this is not a necessary condition).


Mário S Alvim
email: msalvim@lix.polytechnique.fr

Miguel E Andrés
email: mandres@cs.ru.nl

Catuscia Palamidessi
email: catuscia@lix.polytechnique.fr

Probabilistic Information Flow (Invited Lecture)

In recent years, there has been a growing interest in considering the probabilistic aspects of Information Flow. In this abstract we review some of the main approaches that have been considered to quantify the notion of information leakage, and we focus on some recent developments.

I. INTRODUCTION

One of the concerns in the use of computer systems is to avoid the leakage of secret information through public observables. Ideally we would like systems to be completely secure, but in practice this goal is often impossible to achieve. Therefore it is important to express the amount of leakage in quantitative terms, so to be able to assess whether a system is better than another, although they may both be insecure.

Several works in literature use an Information Theoretic approach to model the problem and define the leakage in a quantitative way, see for example [START_REF] Zhu | Anonymity vs. information leakage in anonymity systems[END_REF], [START_REF] Clark | Quantitative information flow, relations and polymorphic types[END_REF], [START_REF] Malacaria | Assessing security threats of looping constructs[END_REF], [START_REF] Malacaria | Lagrange multipliers and maximum information leakage in different observational models[END_REF], [START_REF] Moskowitz | Quasianonymous channels[END_REF], [START_REF] Moskowitz | Covert channels and anonymizing networks[END_REF], [START_REF] Chatzikokolakis | Anonymity protocols as noisy channels[END_REF]. The idea is that the system is seen as a channel. The input represents the secret, the output represents the observable, and the correlation between the input and output (mutual information) represents the information leakage. The worst case leakage corresponds then to the capacity of the channel, which is by definition the maximum mutual information that can be obtained by varying the input distribution.

In the works mentioned above, the notion of mutual information is based on Shannon entropy, which (because of its mathematical properties) is the most established measure of uncertainty. From the security point of view, this measure corresponds to a particular model of attack and a particular way of estimating the security threat (vulnerability of the secret). Other notions have been considered, and argued to be more appropriate for security in certain scenarios. These include: Rényi min-entropy [START_REF] Rényi | On Measures of Entropy and Information[END_REF], [START_REF] Smith | On the foundations of quantitative information flow[END_REF], Bayes risk [START_REF] Cover | Elements of Information Theory[END_REF], [START_REF] Chatzikokolakis | On the Bayes risk in information-hiding protocols[END_REF], guessing entropy [START_REF] Massey | Guessing and entropy[END_REF], and marginal guesswork [START_REF] Pliam | On the incomparability of entropy and marginal guesswork in brute-force attacks[END_REF].

In Section II we will discuss their meaning and show how they relate (or do not relate) to each other and to Shannon entropy. This work has been partially supported by the project ANR-09-BLAN-0169-01 PANDA and by the INRIA DRI Equipe Associée PRINTEMPS. Whatever definition of uncertainty (i.e. vulnerability) we want to adopt, the notion of leakage is inherent to the system as can be expressed in a uniform way as the difference between the initial uncertainty, i.e. the degree of ignorance about the secret before we run the system, and the remaining uncertainty, i.e. the degree of ignorance about the secret after we run the system and observe its outcome. Following the principle advocated by Smith [START_REF] Smith | On the foundations of quantitative information flow[END_REF], and by many others:

information leakage = initial uncertainty - remaining uncertainty (1)
In [START_REF] Zhu | Anonymity vs. information leakage in anonymity systems[END_REF], the initial uncertainty depends solely on the input distribution, aka a priori distribution. Intuitively, the more uniform this is, the less we know about the secret (in the probabilistic sense). After we run the system, if there is a probabilistic correlation between input and output, then the observation of the output should increase our knowledge of the secret. This is determined by the fact that the distribution on the input changes: in fact we can update the probability of each input with the corresponding conditional probability of the same input, given the output. The new distribution is called a posteriori distribution. In case input and output are independent, then the a priori and the a posteriori distributions coincide and the knowledge should remain the same. In the following, we will use the attributes "a priori" and "a posteriori" to refer to before and after the observation of the output, respectively. The above intuitions should be reflected by any reasonable notion of uncertainty: it should be higher on more uniform distributions, and it should decrease or remain equal with the observation of related events.

If the uncertainty is expressed in terms of Shannon entropy, then the initial uncertainty is the entropy of the input, the remaining uncertainty is the conditional entropy of the input given the output, and (1) matches exactly the definition of mutual information. This justifies the notion of leakage adopted in the works mentioned before ([1], [START_REF] Clark | Quantitative information flow, relations and polymorphic types[END_REF], [START_REF] Malacaria | Assessing security threats of looping constructs[END_REF], [START_REF] Malacaria | Lagrange multipliers and maximum information leakage in different observational models[END_REF], [START_REF] Moskowitz | Quasianonymous channels[END_REF], [START_REF] Moskowitz | Covert channels and anonymizing networks[END_REF], [START_REF] Chatzikokolakis | Anonymity protocols as noisy channels[END_REF]).

The analogy between information flow in a system and a (simple) channel works well when (i) there is no nondeterminism, i.e. either the system is deterministic, or purely probabilistic, and (ii) there is a precise temporal relation between secrets and observables in the computations; namely, the value of the secret is chosen at the beginning of the computation, and, the computation of the system produces an observable outcome, with a probability that depends solely on the chosen input and on the system. Furthermore, each new run of the system is independent from the previous ones.

Restriction (i) implies that for each secret there is exactly one conditional probability distribution on the observables, where the condition is the secret value. Restriction (ii) ensures that this conditional distribution depends uniquely on the system (not on the input distribution). These conditional probabilities constitute the so-called matrix of the channel. Note that in a (basic) information-theoretic channel the matrix must be invariant with respect to the input distribution, which is exactly what condition (ii) guarantees.

If a system is deterministic, then under the same input each run produces always the same output, with probability 1. Therefore the matrix contains only 0's and 1's. The problem of inferring the secret is still interesting though, because the same output may correspond to different inputs. If the system is probabilistic, i.e. it uses some randomized mechanisms, then the matrix usually contains probabilities different from 0 and 1.

Unfortunately, for real-life systems usually conditions (i) and (ii) are too restrictive:

• Specifications typically need to use nondeterminism in order to abstract from implementation details. This is particularly compelling in the case of concurrent and distributed systems: The order in which the various components get executed, and their interactions, depend on scheduling policies that may differ from implementation to implementation. Furthermore, even if the scheduling policy is fixed, there are run time circumstances that may influence the relative speed of the processes. Nondeterminism is an unavoidable aspect of concurrency. • Secrets and observables often alternate and interact during an execution. In particular, the choice of a new secret may depend on previous observables. Furthermore, new execution of the systems may depend on previous ones. This may be due to the way the system works, or to the presence of an active adversary that may use the knowledge derived from previous observations to try to tamper with the mechanisms of the system, with the purpose of increasing the leakage. Examples of such systems, that we call here interactive systems (were interaction refers to the interplay between secrets and observables), can be found in the area of game theory, auction protocols, web servers, GUI applications, etc.

In this paper, we consider the challenges of extending the information-theoretic approach when conditions (i) and (ii) are lifted, and we illustrate two approaches that we have recently proposed in [START_REF] Alvim | Information Flow in Interactive Systems[END_REF] and [START_REF] Alvim | Safe Equivalences for Security Properties[END_REF].

The rest of the paper is organized as follows: in next section we discuss and compare various notions of uncertainty proposed in literature. In Section III we illustate our proposal for modeling interactive systems and defining the notion of leakage. In Section IV we recall briefly the possibilistic approaches proposed in literature to characterize the absence of leakage in nondeterministic systems, we discuss the problems that arise with respect to implementation refinement, and those caused by the presence of omniscent schedulers. We then illustrate our proposal to cope with nondeterminism.

II. UNCERTAINTY AND LEAKAGE

In this section we recall various definitions of uncertainty proposed in literature, and we discuss the relation with security attacks and the way of measuring their success. In general we consider the kind of threats that in the model of [START_REF] Köpf | An information-theoretic model for adaptive side-channel attacks[END_REF] are called brute-force guessing attacks, which can be summarized as follows: The goal of the adversary is to determine the value of a random variable. He can make a series of queries to an oracle. Each query must have a yes/no answer. In general the adversary is adaptive, i.e. he can choose the next query depending on the answer to the previous ones. We assume that the adversary knows the probability distribution.

In the following, A, B denote two discrete random variables with carriers A = {a 1 , . . . , a n }, B = {b 1 , . . . , b m }, and probability distributions p A (•), p B (•), respectively. We will use A ∧ B to represent the random variable with carrier A×B and joint probability distribution p A∧B (a, b) = p A (a) • p(b | A = a), while A • B will denote the random variable with carrier A × B and probability distribution defined as product, i.e.

p A•B (a, b) = p A (a) • p B (b). Clearly, if A and B are independent, we have A ∧ B = A • B.
We shall omit the subscripts on the probabilities when they are clear from the context. In reference to a channel, in general A will denote the input (secret), and B the output (observable).

A. Shannon entropy

The Shannon entropy of A [START_REF] Shannon | A mathematical theory of communication[END_REF] is defined as

H(A) = - a ∈ A p(a) log p(a)
The minimum value H(A) = 0 is obtained when p(•) is concentrated on a single value (i.e. when p(•) is a delta of Dirac). The maximum value H(A) = log |A| is obtained when p(•) is the uniform distribution. Usually the base of the logarithm is set to be 2 and, correspondingly, the entropy is measured in bits.

The conditional entropy of

A given B is H(A | B) = b ∈ B p(b) H(A | B = b) (2)
where

H(A | B = b) = - a ∈ A p(a|b) log p(a|b)
We can prove that 0 ≤ H(A | B) ≤ H(A). The minimum value, 0, is obtained when A is completely determined by B. The maximum value H(A) is obtained when B reveals no information about A, i.e. when A and B are independent. The mutual information between A and B is defined as

I(A; B) = H(A) -H(A | B) (3)
and it measures the amount of information about A that we gain by observing B. It can be shown that I(A; B) = I(B; A) and 0 ≤ I(A; B) ≤ H(A).

Meaning in security:

To explain what H(A) represents from the security point of view, consider a partition {A i } i∈I of A. The adversary is allowed to ask questions of the form "is A ∈ A i ?" according to some strategy. Let n(a) be the number of questions that are needed to determine the value of a, when A = a. Then H(A) represents the lower bound to the expected value of n(•), with respect to all possible partitions and strategies of the adversary [START_REF] Pliam | On the incomparability of entropy and marginal guesswork in brute-force attacks[END_REF], [START_REF] Köpf | An information-theoretic model for adaptive side-channel attacks[END_REF].

B. Rényi min-entropy

In [START_REF] Rényi | On Measures of Entropy and Information[END_REF], Rényi introduced a one-parameter family of entropy measures, intended as a generalization of Shannon entropy. The Rényi entropy of order α (α > 0, α = 1) of a random variable A is defined as

H α (A) = 1 1 -α log a ∈ A p(a) α
Rényi's motivations were of axiomatic nature: Shannon entropy satisfies four axioms, namely symmetry, continuity, value 1 on the Bernoulli uniform distribution, and the chain rule 1 :

H(A ∧ B) = H(A | B) + H(B) (4)
(The entropy of the joint probability, H(A ∧ B), is more commonly denoted by H(A, B). We will use the latter notation in the following.) Shannon entropy is also the only function that satisfies those axioms. However, if we replace (4) with a weaker property representing the additivity of entropy for independent distributions:

H(A • B) = H(A) + H(B) (5)
then there are more functions satisfying the axioms, among which all those of the Rényi's family.

Shannon entropy is obtained by taking the limit of H α as α approaches 1. In fact we can easily prove, using l'Hôpital's rule, that

H 1 (A) def = lim α→1 H α (A) = - a ∈ A p(a) log p(a)
We are particularly interested in the limit of H α as α approaches ∞. This is called min-entropy. It can be proven that

H ∞ (A) def = lim α→∞ H α (A) = -log max a∈A p(a)
Rényi considered also the α-generalization of the Kullback-Liebler divergence, which is defined as (assuming that p and q are distributions on the same set X ):

D KL (p q) = x ∈ X p(x) log p(x) q(x)
Rényi's α-generalization is:

D α (p q) = 1 1 -α log x ∈ X p(x) α q(x) α-1
The standard case, i.e. the Kullback-Liebler divergence, is again obtained by taking the limit of D α as α → 1.

The interest of the above for our purposes lies on the fact that Shannon mutual information can equivalently be defined in terms of the Kullback-Liebler divergence (see for instance [START_REF] Cover | Elements of Information Theory[END_REF]):

I(A; B) = D KL (A ∧ B A • B)
Therefore, it seems natural to define the α-generalization of the mutual information as:

I α (A; B) = D α (A ∧ B A • B) (6)
Other α-generalizations of the mutual information, based on the same idea, are explored in [START_REF] Csiszár | Generalized cutoff rates and Rényi's information measures[END_REF]. As α → ∞, the above definition gives the following minversion of the mutual information:

I ∞ (A; B) def = lim α→∞ I α (A; B) = log max a,b p(a, b) p(a) p(b) (7)
Another natural way to generalize I(A; B) would be to replace H by H α in Definition (3). However, Rényi did not define the α-generalization of the conditional entropy, and there is no agreement on what it should be.

Various researchers, including Cachin [START_REF] Cachin | Entropy measures and unconditional security in cryptography[END_REF], have considered the following definition, based on (2):

H Cachin α (A | B) = b ∈ B p(b) H α (A | B = b) (8)
which, as α → ∞, becomes

H Cachin ∞ (A | B) = - b ∈ B p(b) log max a∈A p(a | b) (9)
An alternative proposal for H ∞ (• | •) came from Smith [START_REF] Smith | On the foundations of quantitative information flow[END_REF]:

H Smith ∞ (A | B) = -log b∈B max a∈A p(a, b) (10)
Using ( 9), [START_REF] Cover | Elements of Information Theory[END_REF], and the analogue of (3) we can define I Cachin ∞ and I Smith ∞ . Meaning in security: Rényi min-entropy can be related to a model of adversary who is allowed to ask exactly one question, which must be of the form "is A = a?" (one-try attacks). More precisely, H ∞ (A) represents the (logarithm of the inverse of the) probability of success for this kind of attacks and with the best strategy, which consists, of course, in choosing the a with the maximum probability.

As for H ∞ (A | B) and I ∞ (A; B), the most interesting versions, in terms of security, seem to be those of Smith: In fact, H Smith 1), but the difference becomes ratio due to the presence of the logarithms.) Note that I Smith ∞ (A; B) ≥ 0, which seems desirable for a good notion of leakage.

The definition of I ∞ in [START_REF] Chatzikokolakis | Anonymity protocols as noisy channels[END_REF] has also an interpretation in security: it represents the maximum gain in the probability of success, i.e. the maximum ratio between the a posteriori and the a priori probability. Note that also I ∞ (A; B) is always non-negative and it is 0 if and only if A and B are independent. Furthermore I ∞ (A; B) coincides with I Smith ∞ if B is uniformly distributed. More in general, D KL (p q) and its α-extension D α (p q) should represent the "inefficiency" of an adversary who bases its strategy on the distribution q, when in fact the real distribution is p. , they have some nice properties. For instance they enjoy weak versions of the chain rule (4). More precisely, the "=" in (4) becomes "≥" for α < 1, and "≤" for α > 1. However, there is no general relation between H Cachin ∞ (A | B) and H ∞ (A), and therefore I Cachin ∞ is not guaranteed to be non-negative.

Hence I α (A; B) defined as D α (A ∧ B A • B)

C. Guessing entropy

The notion of guessing entropy was introduced by Massey in [START_REF] Massey | Guessing and entropy[END_REF]. Let us assume, for simplicity, that the elements of A are ordered by decreasing probabilities, i.e. if 1 ≤ i < j ≤ n then p(a i ) ≥ p(a j ). Then the guessing entropy is defined as follows:

H G (A) = 1≤i≤|A| i p(a i )
Massey did not define the notion of conditional guessing entropy. In some works, like [START_REF] Cachin | Entropy measures and unconditional security in cryptography[END_REF], [START_REF] Köpf | An information-theoretic model for adaptive side-channel attacks[END_REF], it is defined analogously to (2):

H G (A | B) = b ∈ B p(b) H G (A | B = b)
Meaning in security: Guessing entropy represents an adversary who is allowed to ask repeatedly questions of the form "is A = a?". More precisely, H G (A) represents the expected number of questions that the adversary needs to ask to determine the value of A, assuming that he follows the best strategy, which consists, of course, in choosing the a's in order of decreasing probability.

H G (A | B) represents the expected number of questions a posteriori, i.e. after observing the value of B and reordering the queries according to the updated probabilities (i.e. the queries will be chosen in order of decreasing a posteriori probabilities).

Also in this case, H G (A | B) is not necessarily smaller than or equal to H G (A), so the corresponding notion of mutual information is not guaranteed to be non-negative 2 .

D. Marginal guesswork

The marginal guesswork is a variant of guessing entropy that was proposed by Pliam [START_REF] Pliam | On the incomparability of entropy and marginal guesswork in brute-force attacks[END_REF]. It is parametric to a number ε > 0, and is defined as follows. Again, we assume that the elements of A are ordered by decreasing probabilities.

H ε (A) = min{j | 1≤i≤j p(a i ) > ε}
Pliam did not define the conditional version of marginal guesswork, but in [START_REF] Köpf | An information-theoretic model for adaptive side-channel attacks[END_REF] it is defined following (2):

H ε (A | B) = b ∈ B p(b) H ε (A | B = b)
Meaning in security: Consider again an adversary who is allowed to ask repeatedly questions of the form "is A = a?". H (A) represents the minimum number of questions that the adversary needs to ask to determine the value of A with probability at least .

H ε (A | B) represents the same notion, but using the a posteriori probabilities. Again, it is not necessarily the case that H ε (A | B) ≤ H ε (A).

E. Comparison and Discussion

The various notions of entropy discussed in this section have been carefully compared with Shannon entropy, to conclude that in general there is no tight relation. Fano's inequality gives a lower bound to the Bayes risk in terms of (conditional) Shannon entropy, and Rényi [START_REF] Rényi | On Measures of Entropy and Information[END_REF], Hellman-Raviv [START_REF] Hellman | Probability of error, equivocation, and the Chernoff bound[END_REF], and Santhi-Vardi [START_REF] Santhi | On an improvement over Rényi's equivocation bound[END_REF] give upper bounds as well, but all these are rather weak. Smith has shown in [START_REF] Smith | On the foundations of quantitative information flow[END_REF] that the orderings induced on channels by the Bayes risk and by Shannon entropy are in general unrelated.

Massey has shown that the exponential of the Shannon entropy is a lower bound for the guessing entropy, and that, in case of a geometric distribution, the bound is tight. However Massey has also shown that in the general case the Shannon entropy can be arbritrarily close to 0 while the guessing entropy is constant [START_REF] Massey | Guessing and entropy[END_REF].

As for the marginal guesswork. Pliam has shown that it is essentially unrelated with Shannon entropy [START_REF] Pliam | On the incomparability of entropy and marginal guesswork in brute-force attacks[END_REF].

We conclude this section with an observation about the principle (1). As we have seen above this principle prescribes that, given a model of attack (and a measure of success), one should find the corresponding notion of entropy and conditional entropy, which will then be considered as the initial and the residual uncertainty, respectively. The tendency in literature is to define the conditional entropy following the formula [START_REF] Clark | Quantitative information flow, relations and polymorphic types[END_REF].

It is important to realize that the notion of probability enters the definition of entropy in two ways: one corresponds to the use of them made by the adversary to decide its strategy. The other is for averaging purposes. While the distribution used in the first way depends on the knowledge of the adversary, and changes from a priori to a posteriori with the revelation of the observable, the distribution used in the second way should always be the real one, i.e. the a posteriori one. Some of the definitions of entropy given previously do not satisfy this rule, and in fact we obtain the counterintuitive consequence that the a posteriori uncertainty may be higher than the a priori one.

An alternative of the principle (1) would be to define the leakage as information flow directly by using a suitable variant of the Kullback-Liebler divergence, like in [START_REF] Moskowitz | Covert channels and anonymizing networks[END_REF]. As discussed at the end of Section II-B, this divergence represents the "inefficiency" of an adversary who bases its strategy on the distribution q, when in fact the real distribution is p. So, the new principle would be: Leakage = effectiveness of the attack using the a posteriori distribution effectiveness of the attack using the a priori distribution where the computations are done taking into account that the real distribution is the a posteriori one. In the case of Shannon entropy this new principle coincides with (1), but in general they are different. For instance, in the case of the guessing entropy, we should define I G (A; B) as the expected value (averaged using the a posteriori probabilities) of the divergence between the number of queries when the a's are ordered using the a priori distribution on A, and the number of queries when the a's are ordered using the a posteriori distribution on A.

I G (A; B) = b∈B p(b) 1≤i≤|A| i (p(a i | b) -p(a ki | b)) (11)
where k i is a permutation which reorders the elements of A so that their a posteriori probabilities are decreasing, namely if 1 ≤ i ≤ j ≤ n, then p(a ki ) ≥ p(a kj ).

Note that, if we applied (3) with the definitions of guessing entropy given above, we would obtain, instead:

I G (A; B) = b∈B p(b) 1≤i≤|A| i (p(a i ) -p(a ki | b))
It is possible to prove that, if defined as in [START_REF] Chatzikokolakis | On the Bayes risk in information-hiding protocols[END_REF], then I G (A; B) is always non-negative.

III. INTERACTIVE INFORMATION FLOW

In this section we consider the applicability of the information-theoretic approach to interactive systems, i.e. those systems in which there can be an alternation of secrets and observables during the computation, and they influence each other. The conditional probabilities p(b | a) can be computed as the ratio between the probability that a computation has trace (a, b), given that it has secret trace a [START_REF] Desharnais | The metric analogue of weak bisimulation for probabilistic processes[END_REF]. This is natural and correct, as it follows the definition of conditional probability in terms of joint and marginal probability. However, as shown by the example below, it does not help to define an information-theoretic channel because by definition a channel should be invariant with respect to the input distribution, and such construction is not.

Example: Consider the protocol represented in Figure 1. This protocol is used in a website with one seller and two possible buyers (one of them is poor and the other rich). The sale starts with the seller offering a product, which can be either cheap (with probability r) or expensive (with probability 1 -r). In case the offered product is cheap, the poor buyer aquires the product with probability s whereas the rich buyer does it with probability 1 -s. Similarly (with probabilities t and 1 -t) for the case on which the offered product is expensive. We assume that the offered product is observable, since it is visible to everyone in the website, while the identity of the buyer is secret. In the following, we use the notation r to represent 1 -r.

If we want to build the channel matrix, one could think of using the standard formula for conditional probability p(b | a) = p(a,b) p(a) to fill each entry of the matrix. That is what is

Table I CHANNEL MATRIX

indeed proposed in [START_REF] Desharnais | The metric analogue of weak bisimulation for probabilistic processes[END_REF]. Proceeding this way we obtain the matrix on Table I.

However, the entries of the matrix are not invariant with respect to the input distribution. If we fix the parameters r = r = 0.5 and make two different assignments to the values of s, s, t, t we induce two different input distributions, with the associated matrices, as shown in Table II.

Table II TWO DIFFERENT CHANNEL MATRICES DEPENDING ON THE INPUT

DISTRIBUTION

As shown by this example, when secrets occur after observables the conditional probabilities depend on the distribution on secrets and, thus, so it does the matrix making it unsound to analyze such systems using informationtheoretical approaches.

In [START_REF] Alvim | Information Flow in Interactive Systems[END_REF], we investigate an extension of the theory of simple channels so to make the information-theoretic approach applicable also the case of interactive systems. It turns out that a richer notion of channels, known in Information Theory as channels with memory and feedback, serves our purposes. Indeed the dependence of inputs on past outputs corresponds exactly to feedback, and the dependence of the output on all previous inputs and outputs corresponds to memory.

A. Applications

Interactive systems can be found in a variety of disparate areas such as game theory, auction protocols, and zeroknowledge proofs. We now present two examples of interactive systems.

• In the area of auction protocols, consider the cocaine auction protocol [START_REF] Stajano | The cocaine auction protocol: On the power of anonymous broadcast[END_REF]. The auction is organized as a succession of rounds of bidding. Round i starts with the seller announcing the bid price b i for that round. Buyers have t seconds to make an offer (i.e. to say yes, meaning "I am willing to buy at the current bid price b i "). As soon as one buyer says yes, he becomes the winner w i of that round and a new round begins. If nobody says anything for t seconds, round i is concluded by timeout and the auction is won by the winner w i-1 of the previous round.

The identities of the buyers in each round constitute the input of the channel, whereas the bid prices constitute the output of the channel. Note that inputs and outputs alternate so the system is interactive. It is also easy to see that inputs depend on past outputs (feedback): the identity of the winner of each round depends on the previous bid prices. Furthermore, outputs depend on the previous inputs (memory): (in some scenarios) the bid price of round i may depend on the identity of previous winners. For more details on the modeling of this protocol using channels with memory and feedback see [START_REF] Alvim | Information Flow in Interactive Systems[END_REF]. • In the area of game theory, consider the classic prisoner's dilemma (the present formulation is due to Albert W. Tucker [START_REF] Poundstone | Prisoners Dilemma[END_REF], but it was originally devised by Merrill Flood and Melvin Dresher in 1950). Two suspects are arrested by the police. The police have insufficient evidence for a conviction, and, having separated both prisoners, visit each of them to offer the same deal. If one testifies (defects from the other) for the prosecution against the other and the other remains silent (cooperates with the other), the betrayer goes free and the silent accomplice receives the full 10year sentence. If both remain silent, both prisoners are sentenced to only six months in jail for a minor charge. If each betrays the other, each receives a fiveyear sentence. Each prisoner must choose to betray the other or to remain silent. Each one is assured that the other would not know about the betrayal before the end of the investigation.

In the iterated prisoner's dilemma, the game is played repeatedly. Thus each player has an opportunity to punish the other player for previous non-cooperative play. In this case the strategy (cooperate or defect) of each player is the input of the channel and the sentence is the output. Once again, it is easy to see that the system is interactive: inputs and outputs alternate.

Furthermore, inputs depend on previous outputs (the strategy depend on the past sentences) and outputs depend on previous inputs (the sentence of the suspects depend on their declarations -cooperate or defect).

IV. NONDETERMINISM AND INFORMATION FLOW

As seen in previous Section II, the noise of the channel, namely the similarity between the rows of the channel matrix, helps preventing the inference of the secret from the observables. In practice noise is created by using randomization, see for instance the DCNet [START_REF] Chaum | The dining cryptographers problem: Unconditional sender and recipient untraceability[END_REF] and the Crowds [START_REF] Reiter | Crowds: anonymity for Web transactions[END_REF] protocols.

In the literature about the foundations of Computer Security, however, the quantitative aspects are often abstracted away, and probabilistic behavior is replaced by nondeterministic behavior. Correspondingly, there have been various approaches in which information-hiding properties are expressed in terms of equivalences based on nondeterminism, especially in a concurrent setting. For instance, [START_REF] Schneider | CSP and anonymity[END_REF] defines anonymity as follows3 : A protocol S is anonymous if, for every pair of culprits a and b, S[ a / x ] and S[ b / x ] produce the same observable traces. A similar definition is given in [START_REF] Abadi | A calculus for cryptographic protocols: The spi calculus[END_REF] for secrecy, with the difference that S[ a / x ] and S[ b / x ] are required to be bisimilar. In [START_REF] Delaune | Verifying privacytype properties of electronic voting protocols[END_REF], an electoral system S preserves the confidentiality of the vote if for any voters v and w, the observable behavior of S is the same if we swap the votes of v and w.

Namely, S[ a / v | b / w ] ∼ S[ b / v | a / w ],
where ∼ represents bisimilarity.

These proposals are based on the implicit assumption that all the nondeterministic executions present in the specification of S will always be possible under every implementation of S. Or at least, that the adversary will believe so. In concurrency, however, as argued in [START_REF] Chatzikokolakis | Bisimulation for demonic schedulers[END_REF], nondeterminism has a rather different meaning: if a specification S contains some nondeterministic alternatives, typically it is because we want to abstract from specific implementations, such as the scheduling policy. A specification is considered correct, with respect to some property, if every alternative satisfies the property. Correspondingly, an implementation is considered correct if all executions are among those possible in the specification, i.e. if the implementation is a refinement of the specification. There is no expectation that the implementation will actually make possible all the alternatives indicated by the specification.

We argue that the use of nondeterminism in concurrency corresponds to a demonic view: the scheduler, i.e. the entity that will decide which alternative to select, may try to choose the worst alternative. Hence we need to make sure that "all alternatives are good", i.e. satisfy the intended property. In the above mentioned approaches to the formalization of security properties, on the contrary, the interpretation of nondeterminism is angelic: the scheduler is expected to actually help the protocol to confuse the adversary and thus protect the secret information.

There is another issue, orthogonal to the angelic/demonic dichotomy, but relevant for the achievement of security properties: the scheduler should not be able to make its choices dependent on the secret, or else nearly every protocol would be insecure, i.e. the scheduler would always be able to leak the secret to an external observer (for instance by producing different interleavings of the observables, depending on the secret). This remark has been made several times already, and several approaches have been proposed to cope with the problem of the "almighty" scheduler (aka omniscient, clairvoyant, etc.), see for example [START_REF] Canetti | Task-structured probabilistic i/o automata[END_REF], [START_REF] Chatzikokolakis | Making random choices invisible to the scheduler[END_REF], [START_REF] Chatzikokolakis | Bisimulation for demonic schedulers[END_REF], [START_REF] Andrés | Information hiding in probabilistic concurrent systems[END_REF].

The risk of a naive use of nondeterminism to specify a security property, is not only that it may rely on an implicit assumption that the scheduler behaves angelically, but also that it is clairvoyant, i.e. that it peeks at the secrets (that it is not supposed to be able to see) to achieve its angelic strategy.

Consider the following system, in a CCS-like syntax: where is the parallel operator, c sec is a process that sends sec on channel c, c(s).P is a process that receives s on channel c and then continues as P , and (c, out) is the restriction operator, enforcing synchronization on c and out.

S def = (c, out)(A Corr
In this example, sec represents a secret information.

It is easy to see that we have S [ a / sec ] ∼ S b / sec . Note that, in order to simulate the third branch in S [ a / sec ], the process S b / sec needs to select its first branch. Viceversa, in order to simulate the third branch in S b / sec , the process S [ a / sec ] needs to select its second branch. This means that, in order to achieve bisimulation, the scheduler needs to know the secret, and change its choice accordingly.

This example shows a system that intuitively is not secure, because the third component, Corr , reveals whatever secret it receives. However, according to the equivalence-based notions of security discussed above, it is secure. But it is secure thanks to a scheduler that angelically helps the system to protect the secret, and it does so by making its choices dependent on the secret! In our opinion these assumptions on the scheduler are excessively strong.

In a recent work [START_REF] Alvim | Safe Equivalences for Security Properties[END_REF] we address the above issue by defining a framework in which it is possible to combine both angelic and demonic nondeterminism in a setting in which also probabilistic behavior may be present, and in a context in which the scheduler is restricted (i.e. not clairvoyant). We propose safe versions of typical equivalence relations (traces and bisimulation), and we show how to use them to characterize information-hiding properties.

∞

  (A | B) represents the inverse of the (expected value of the) probability that the same kind of adversary succeeds in guessing the value of A a posteriori, i.e. after observing the result of B. The complement of this probability is also known as probability of error or Bayes risk. Since in general B and A are correlated, observing B increases the probability of success. In fact we can prove formally thatH Smith ∞ (A | B) ≤ H Smith∞ (A), with equality if and only if A and B are independent. I Smith ∞ (A; B) corresponds to the ratio between the probabilities of success a priori and a posteriori, which is a natural notion of leakage. (I Smith ∞ (A; B) is in the format of (

  should represent the gain of the adversary in revising his strategy according to the knowledge of the correlation between A and B. Concerning H Cachin α and I Cachin α

  Figure 1. Interactive System

The original axiom, called the grouping axiom, does not mention the conditional entropy. However it corresponds to the chain rule if the conditional entropy is defined as in[START_REF] Clark | Quantitative information flow, relations and polymorphic types[END_REF].

This problem is inherent to the probabilistic case, and therefore it does not occur in[START_REF] Köpf | An information-theoretic model for adaptive side-channel attacks[END_REF], since that work considers only deterministic systems.

The actual definition of[START_REF] Schneider | CSP and anonymity[END_REF] is more complicated, but the spirit is the same.