Sardaouna Hamadou

Catuscia Palamidessi

Vladimiro Sassone

Ehab Elsalamouny

Probable innocence in the presence of independent knowledge

We analyse the Crowds anonymity protocol under the novel assumption that the attacker has independent knowledge on behavioural patterns of individual users. Under such conditions we study, reformulate and extend Reiter and Rubin's notion of probable innocence, and provide a new formalisation for it based on the concept of protocol vulnerability. Accordingly, we establish new formal relationships between protocol parameters and attackers' knowledge expressing necessary and sufficient conditions to ensure probable innocence.

Introduction

Anonymity protocols often use random mechanisms. It is therefore natural to think of anonymity in probabilistic terms. Various notions of such probabilistic anonymity have been proposed and a recent trend of work in formalizing these notions is directed at exploring the application of information-theoretic concepts (e.g. [18, 4-6, 1, 15]). In our opinion, however, except a recent paper by Franz, Meyer, and Pashalidis [START_REF] Franz | Attacking unlinkability: The importance of context[END_REF] which addresses the advantage that an adversary could take of hints from the context in which the protocol operates, such approaches fail to account for the fact that in the real world, the adversary often have some extra information about the correlation between anonymous users and observables. Consider for example the following simple anonymous voting process. In a parliament composed by Labourists and Conservatives, one member voted against a proposal banning minimum wages. Without any additional knowledge it is reasonable to assume that the person is more likely to be in the most liberal political group. If however we know in addition that one Conservative voted against, then it is more reasonable to suspect the liberally-inclined Conservatives. Similarly, suppose that in a classroom of n students the teacher asks to tick one of two boxes on a piece of paper to indicate whether or not they are satisfied by her teaching. If n is small and the teacher noticed that the pupils use pens of different colours, then she can use these colours to partition the class so as to make the vote of some students more easily identifiable. Extra knowledge of this kind, independent of the logic of the protocol used, can affect dramatically its security. The extra knowledge can either arise from an independent source, as in the first example, or simply from the context in which the anonymity protocol is run, as in the second example.

The work of Catuscia Palamidessi has been partially supported by the project ANR-09-BLAN-0169-01 PANDA: PArallel aNd Distributed Analysis.

A relevant point in case is Reiter and Rubin's Crowds protocol [START_REF] Reiter | Crowds: Anonymity for web transactions[END_REF], which allows Internet users to perform anonymous web transactions. The idea is to send the message through a chain of users participating in the protocol. Each user in the 'crowd' must establish a path between her and a set of servers by selecting randomly some users to act as routers. The random selection process is performed in such a way that when a user in the path relays a message, she does not know whether or not the sender is the initiator of the message, or simply a forwarder like herself. Each user only has access to messages routed through her, and some participants may be corrupted, i.e., they may work together in order to uncover the identity of the initiator. It is well known that Crowds cannot ensure strong anonymity [START_REF] Reiter | Crowds: Anonymity for web transactions[END_REF][START_REF] Chatzikokolakis | Probable innocence revisited[END_REF] in presence of corrupted participants, but when the number of corrupted users is sufficiently small, it provides a weaker notion of anonymity known as probable innocence. Informally, a sender is probably innocent if to an attacker she is no more likely to be the originator than not to be.

Although Crowds has been widely analysed in the literature (e.g. [START_REF] Chatzikokolakis | Probable innocence revisited[END_REF][START_REF] Malacaria | Lagrange multipliers and maximum information leakage in different observational models[END_REF]), the fact that independent information may be available to the attacker has been so far ignored. We maintain that this is ultimately incompatible with achieving a comprehensive and reliable analysis of the protocol, as attackers' extra knowledge is inherent to Crowds. In particular, as any request routed through an attacker reveals the identity of the target server, a team of attackers will soon build up a host of observations suitable to classify the behaviour of honest participants.

This paper is to the best of our knowledge the first to investigate the impact of the attacker's independent knowledge on the anonymity in the Crowds protocol.

Related work.

Quantitative approach to the foundations of information-hiding has became a very active and mature research field. Several various formal definitions and frameworks have been proposed for reasoning about secure information flow analysis (e.g. [START_REF] Smith | On the foundations of quantitative information flow[END_REF][START_REF] Chen | Quantitative analysis of leakage for multi-threaded programs[END_REF][START_REF] Clark | A static analysis for quantifying information flow in a simple imperative language[END_REF][START_REF] Michael | Belief in information flow[END_REF]), side-channel analysis (e.g [START_REF] Köpf | An information-theoretic model for adaptive side-channel attacks[END_REF]) and anonymity. Our work follows a recent trend in the analysis of anonymity protocols directed to the application of information-theoretic notions (e.g. [17, 18, 4-6, 1, 15, 10, 2]).

The most related work to ours is the one of Reiter and Ruben [START_REF] Reiter | Crowds: Anonymity for web transactions[END_REF], the one of Halpen and O'Neill [START_REF] Halpern | Anonymity and information hiding in multiagent systems[END_REF], and the recent paper of Chatzikokolakis, and Palamidessi [START_REF] Chatzikokolakis | Probable innocence revisited[END_REF]. In [START_REF] Reiter | Crowds: Anonymity for web transactions[END_REF] the authors propose a formal definition of probable innocence that considers the probability of observable events induced by actions of an anonymous user participating in the protocol. They require that the probability of an anonymous user producing any observable to be less than one half. In [START_REF] Halpern | Anonymity and information hiding in multiagent systems[END_REF] the authors formalize probable innocence in terms of the adversary's confidence that a particular anonymous event happened, after performing an observation. Their definition requires that the probability of an anonymous events should be at most one half, under any observation. In [START_REF] Chatzikokolakis | Probable innocence revisited[END_REF] the authors argue that the definition of [START_REF] Reiter | Crowds: Anonymity for web transactions[END_REF] makes sense only for systems satisfying certain properties while the definition of [START_REF] Halpern | Anonymity and information hiding in multiagent systems[END_REF] depends on the probabilities of anonymous events which are not part of the protocol. They propose a definition of probable innocence that tries to combine the two previous ones by considering both the probability of producing some observable and the adversary's confidence after the observation.

Another recent work closely related to ours is the one of Smith's [START_REF] Smith | On the foundations of quantitative information flow[END_REF] which proposes a new metric for quantitative information flow based on the concept of vulnerability as an alternative to previous metrics based on Shannon entropy and mutual infor-mation. Informally, the idea is that the adversary knows the a priori distributions of the hidden (anonymous) events and always 'bets' on the most likely culprit. The a priori vulnerability then is the probability that the adversary guesses the true culprit based only on the a priori distribution. The a posteriori vulnerability is the average probability that the adversary guesses the true culprit based on the a posteriori probability distribution on the agents after the observation.

The main difference between these approaches and ours is that they do not take into account the very likely additional knowledge of the adversary about the correlation between the anonymous events and some observables independent from the behaviour of the protocol. In this paper we first generalize the concepts of probable innocence and vulnerability. Instead than just comparing the probability of being innocent with the probability of being guilty, we consider the degree of the probability of being innocent. Informally a protocol is α-probable innocent if for any anonymous user the probability of being innocent is less than or equal to α. Similarly a protocol is α-vulnerable if the a posteriori vulnerability of the anonymous users is less than or equal to α. We prove that these two notions are related. In particular (α-)probable innocence implies (α-)vulnerability and in the specific case when the a priori distribution of the anonymous events is uniform, they are equivalent. We furthermore extend these definitions in order to cope with the extra independent knowledge of the adversary by computing the a posteriori probability and the a posteriori vulnerability w.r.t to both the protocol observables and the independent observables. We show that the presence of extra knowledge makes probable innocence (resp. vulnerability) more difficult to be achieved.

Finally, it should be acknowledged that our observations about the importance of additional knowledge of the adversary are not entirely new. Indeed, as already noticed above, Franz, Meyer, and Pashalidis [START_REF] Franz | Attacking unlinkability: The importance of context[END_REF] considered the fact that an adversary could take advantage of hints from the context in which a protocol operates. However, though that their approach is closely related to ours in spirit, it is not general in the sense that it assumes a deterministic correlation between the anonymous events and the observable hints and a uniform distribution on the anonymous events. Moreover, their metric is associated to Shannon entropy which is recently proven by Smith [START_REF] Smith | On the foundations of quantitative information flow[END_REF] of being less accurate than vulnerability-based metric.

Structure of the paper. The paper is organised as follows: in §2 we fix some basic notations and recall the fundamental ideas of the Crowds protocol and its properties, including the notion of probable innocence. In §3 we reformulate and extend probable innocence using the idea of protocol vulnerability; §4 and §5 deliver our core technical contribution by respectively extending probable innocence and vulnerability to the case of attacker's independent knowledge.

Preliminaries

This section describes our conceptual framework and briefly revises the Crowds protocol and the notion of probable innocence. We use capital letters A, B to denote discrete random variables and the corresponding small letters a, b and calligraphic letters A, B for their values and set of values respectively. We denote by p(a), p(b) the probabilities of a and b respectively and by p(a ∧ b) their joint probability. The conditional probability of a given b is defined as

p(a | b) = p(a ∧ b) p(b)
The Bayes theorem relates the conditional probabilities p(a | b) and p(b | a) as follows

p(a | b) = p(b | a) p(a) p(b)

The framework

In this paper we consider a framework similar to the probabilistic approaches to anonymity and information flow used in (for instance) [START_REF] Halpern | Anonymity and information hiding in multiagent systems[END_REF], [START_REF] Chatzikokolakis | Anonymity protocols as noisy channels[END_REF], [START_REF] Malacaria | Lagrange multipliers and maximum information leakage in different observational models[END_REF], and [START_REF] Smith | On the foundations of quantitative information flow[END_REF]. We restrict ourselves to total protocols and programs with one high level (or anonymous) input A, a random variable over a finite set A, and one low level output (observable) O, a random variable over a finite set O. We represent a protocol/program by the matrix of the conditional probabilities p(o j | a i ), where p(o j | a i ) is the probability that the low output is o j given that the high input is a i . We assume that the high input is generated according to an a priori publicly-known probabilistic distribution. An adversary or eavesdropper can see the output of a protocol, but not the input, and he is interested in deriving the value of the input from the observed output in one single try.

In this paper we will also assume that the attacker has access to the value of a random variable S distributed over S that summarizes his additional knowledge (information) about A independent from the behavior of the protocol, as explained in the introduction. The matrix of the conditional probabilities p(s k | a i ) expresses the correlation between the anonymous events and the additional knowledge of the adversary.

When | S | = 1 the adversary's additional information about A is a trivial one and cannot help his effort in determining the value of A. For example knowing the length of a password in a fixed-length password system is a trivial information since all passwords have the same length. Trivial information allows us to model the absence of additional information. The standard framework can therefore be seen as an instance of our framework.

The Crowds Protocol and the definition of probable innocence

The protocol. Crowds is a protocol proposed by Reiter and Rubin in [START_REF] Reiter | Crowds: Anonymity for web transactions[END_REF] to allow Internet users performing anonymous web transactions by protecting their identity as originators of messages. The central idea to ensure anonymity is that the originator forwards the message to another, randomly-selected user, which in turn forwards the message to another user, and so on until the message reaches its destination (the end server). This routing process ensures that, even when a user is detected sending a message, there is a substantial probability that she is simply forwarding it on behalf of somebody else.

More specifically, a crowd is a fixed number of users participating in the protocol. Some members (users) in the crowd may be corrupted (the attackers), and they can collaborate in order to discover the originator's identity. The purpose of the protocol is to protect the identity of the message originator from the attackers. When an originator -also known as initiator-wants to communicate with a server, she creates a random path between herself and the server through the crowd by the following process.

-Initial step: the initiator selects uniformly at random a member of the crowd (possibly herself) and forwards the request to her. We refer to the latter user as the forwarder.

-Forwarding steps: a forwarder, upon receiving a request, flips a biased coin. With probability 1p f she delivers the request to the end server. With probability p f she selects uniformly at random a new forwarder (possibly herself) and forwards the request to her. The new forwarder repeats the same forwarding process.

The response from the server to the originator follows the same path in the opposite direction. Each user (including corrupted users) is assumed to have only access to messages routed through her, so that she only knows the identities of her immediate predecessor and successor in a path, and the end server.

Informal definition of Probable Innocence. In [START_REF] Reiter | Crowds: Anonymity for web transactions[END_REF] Reiter and Rubin have proposed a hierarchy of anonymity notions in the context of Crowds. These range from 'absolute privacy,' where the attacker cannot perceive the presence of communication, to 'provably exposed,' where the attacker can prove the sender and receiver relationship. Clearly, as most protocols used in practice, Crowds cannot ensure absolute privacy in presence of attackers or corrupted users, but can only provide weaker notions of anonymity. In particular, in [START_REF] Reiter | Crowds: Anonymity for web transactions[END_REF] the authors propose an anonymity notion called probable innocence and prove that, under some conditions on the protocol parameters, Crowds ensures the probable innocence property to the originator. Informally, they define it as follows:

A sender is probably innocent if, from the attacker's point of view, the sender appears no more likely to be the originator than to not be the originator.

In other words, the attacker may have reason to suspect the sender of being more likely than any other potential sender to be the originator, but it still appears at least as likely that she is not.

The formal property proved by Reiter and Rubin. Let m be the number of users participating in the protocol and let c and n be the number of the corrupted and honest users, respectively, with m = n + c. Since anonymity makes only sense for honest users, we define the set of anonymous events as A = {a 1 , a 2 , . . . , a n }, where a i indicates that user i is the initiator of the message. We define the set of observable events as O = {o 1 , o 2 , . . . , o n }, where o i indicates that user i forwarded a message to a corrupted user. We also say that user i is detected by the attacker.

As it is usually the case in the analysis of Crowds, we assume that attackers will always deliver a request to forward immediately to the end server, since forwarding it any further cannot help them learn anything more about the identity of the originator.

In [START_REF] Reiter | Crowds: Anonymity for web transactions[END_REF] Reiter and Rubin formalise their notion of probable innocence via the conditional probability p(I | H) that the initiator is detected given that any user is detected at all. Here I denotes the event that it is precisely the initiator to forward the message to the attacker on the path, and H that there is an attacker in the path. Precisely, probable innocence holds if p(I | H) ≤ 1 2 . In our setting the probability that user j is detected given that user i is the initiator, can be written simply as p(o j | a i ). As we are only interested in the case in which a user is detected, for simplicity we do not write such condition explicitly. Therefore, the property proved in [START_REF] Reiter | Crowds: Anonymity for web transactions[END_REF] (i.e. p(I | H) ≤ 1 2 ) translates in our setting as:

∀i. p(o i | a i ) ≤ 1/2 (2)
Reiter and Rubin proved in [START_REF] Reiter | Crowds: Anonymity for web transactions[END_REF] that, in Crowds, the following holds:

p(o j | a i ) =          1 -n-1 m p f i = j 1 m p f i j
Therefore, probable innocence (2) holds if and only if

m ≥ c + 1 p f -1 2 p f
3 Probable innocence revisited and extended

In our opinion there is a mismatch between the idea of probable innocence expressed informally in (1) and the property actually proved by Reiter and Rubin, cf. [START_REF] Braun | Compositional methods for information-hiding[END_REF]. The former, indeed, seems to correspond to the following:

∀i. p(a i | o i ) ≤ 1/2 (3)
It is worth noting that this is also the interpretation given by Halpern and O'Neill [START_REF] Halpern | Anonymity and information hiding in multiagent systems[END_REF].

The properties (2) and (3) however coincide under the assumption that the a priori distribution is uniform, i.e. that each honest user has equal probability of being the initiator. This is a standard asumption in Crowds. Proposition 1. If the a priori distribution is uniform, then ∀i, j. p(a i | o j ) = p(o j | a i ).

Proof. If the a priori distribution is uniform, then for every i we have p(a i ) = 1/n where n is the number of honest users. The probability of user j being detected is also uniform, and hence equal to 1/n. In fact, every initiator forwards the message to each other user with the same probability, and each forwarder does the same, hence each user has the same probability of being detected when she is the initiator, and the same probability of being detected when she is not the initiator. Therefore we have:

p(o j | a j ) = p(o k | a k ) and p(o j | a i ) = p(o k | a i )
for every j, k and i j, k, and hence:

p(o j ) = p(o j ∧ a j ) + i j p(o j ∧ a i ) = p(o j | a j )p(a j ) + i j p(o j | a i )p(a i ) = p(o k | a k )p(a k ) + i k p(o k | a i )p(a i ) by symmetry = p(o k )
Finally, by using the Bayes theorem, we have:

p(a i | o j ) = p(o j | a i ) p(a i ) p(o j ) = p(o j | a i ) • 1/n 1/n = p(o j | a i ) Corollary 1.
If the a priori distribution is uniform, then (2) and ( 3) are equivalent.

The following proposition points out that in presence of uniform a priori distribution, the matrix associated to the protocol, i.e. the array of the conditional probabilities p(o j |a i ), has equal elements everywhere except on the diagonal: Proposition 2. If the a priori distribution is uniform, then there exists a p such that

p(o j | a i ) =          p i = j 1-p n-1 i j
Proof. As already noted in the proof of Proposition 1, for symmetry reasons we have

p(o j | a j ) = p(o k | a k ) and p(o j | a i ) = p(o k | a i ) for every j, k and i j, k.
It is generally the case, in Crowds, that p is (much) greater than (1p)/(n -1), which means that the user which is detected is also the most likely culprit. This allows us to reformulate the property of probable innocence in terms of the (a posteriori) vulnerability [START_REF] Smith | On the foundations of quantitative information flow[END_REF] of a protocol, which coincides with the converse of the Bayes risk [START_REF] Chatzikokolakis | On the Bayes risk in information-hiding protocols[END_REF].

Let us briefly recall the definition of vulnerability. The idea is that the adversary knows the a priori distributions and always 'bets' on the most likely culprit. The a priori vulnerability then is the probability that the adversary guesses the true culprit based only on the a priori distribution p(a). The a posteriori vulnerability is the average probability that the adversary guesses the true culprit based on the a posteriori probability distribution on the agents after the observation, i.e., p(a | o). Formally:

Definition 1 ([19]). -The a priori vulnerability is V(A) = max i p(a i ) -The a posteriori vulnerability is V(A | O) = j p(o j ) max i (p(a i |, o j ))
Using the Bayes theorem, we can reformulate V(A | O) as follows:

V(A | O) = j max i (p(o j |a i ) p(a i )) (4)
It is easy to see that probable innocence implies that the a posteriori vulnerability is smaller than 1/2. The converse also holds, if the a priori distribution is uniform.

Proposition 3. -If either (2) or (3) holds, then V(A | O) ≤ 1/2. -If V(A | O) ≤ 1/2 and
the a priori distribution is uniform, then (2) and (3) hold.

We now generalize the concept of probable innocence. Instead than just comparing the probability of being innocent with the probability of being guilty, we consider the degree of the probability of being innocent. Similarly for the vulnerability.

Definition 2. Given a real number α ∈ [0, 1], we say that a protocol satisfies

-α-probable innocence if and only if ∀i. p(a i | o i ) ≤ α -α-vulnerability if and only if V(A | O) ≤ α.
Clearly α-probable innocence coincides with the standard probable innocence for α = 1/2. It is also to be remarked that the minimum possible value of α is 1/n, i.e., it is not possible for a protocol to satisfy α-probable innocence or α-vulnerability if α is smaller than this value.

Probable innocence in presence of extra information

We now consider the notion of probable innocence when we assume that the adversary has some extra information about the correlation between the culprit and the observable.

We express this extra information in terms of a random variable S , whose values s 1 . . . s we assume to be observable, and the conditional probabilities p(s k | a i ). We assume that, the original observables O and the additional observables S are independent, for every originator.

Example 1. Consider an instance of the Crowds protocol in which there are two servers, and assume that the users are divided in two parts, A 1 and A 2 . Assume that each user in A 1 , when he is the initiator, has probability p 1 to address his message to the first server (as the final destination of the message). Conversely, assume that each user in A 2 has probability p 2 to address the second server. The address of the server appears in the message, and it is therefore observed by the adversary when he intercepts the message. It is clear that (because of the way Crowds works) the event that the message is intercepted is independent from the server to which the message is addressed.

If we indicate by s 1 the fact that the message is addressed to the first server, and by s 2 the fact that the message is addressed to the second server, the matrix of the conditional probabilities corresponding to this example is as follows:

p(s | a) =                          p 1 a ∈ A 1 , s = s 1 1 -p 1 a ∈ A 1 , s = s 2 1 -p 2 a ∈ A 2 , s = s 1 p 2 a ∈ A 2 , s = s 2
We are interested in exploring how the extra information provided by S and the conditional probabilities of S given A affects the notion of probable innocence.

We take the point of view that the invariant property should be the one expressed by (3), generalized by Definition 2. We reformulate this definition to accommodate the presence of extra information in the observables. Definition 3 (α-probable innocence in presence of extra information). Given a real number α ∈ [0, 1], we say that a protocol satisfies α-probable innocence if and only if

∀i, k. p(a i | o i ∧ s k ) ≤ α
The following lemma expresses the relation between the conditional probabilities with respect to the new observables and the original ones

Lemma 1. ∀i, j, k. p(a i | o j ∧ s k ) = p(a i | o j ) p(s k | a i ) p(s k | o j )
Proof. By Bayes theorem we have, for every i, j, k

p(a i | o j ∧ s k ) = p(o j ∧ s k | a i ) p(a i ) p(o j ∧ s k )
Since we are assuming that, given any originator a i , O and S are independent, we have

p(o j ∧ s k | a i ) = p(o j | a i ) p(s k | a i ), and therefore p(a i | o j ∧ s k ) = p(o j | a i ) p(s k | a i ) p(a i ) p(o j ∧ s k )
We can rewrite p(o j ∧ s k ) as p(s k | o j ) p(o j ). Hence:

p(a i | o j ∧ s k ) = p(o j | a i ) p(s k | a i ) p(a i ) p(s k |o j ) p(o j )
Finally, using Bayes theorem again, we conclude.

We can now prove the presence of extra information reduces the degree α of probable innocence by a factor q = min i,k p(

s k | o i )/p(s k | a i ) : Proposition 4.
-In presence of extra information, a protocol satisfies α-probable innocence if

∀i. p(a i | o i ) ≤ q α -If ∀i, j. p(a i | o i ) = p(a j | o j ),
then the above condition is also necessary, i.e. the protocol satisfies α-probable innocence only if

∀i. p(a i | o i ) ≤ q α
Proof. Immediate from previous lemma, with j = i.

In general the factor q in the above proposition is strictly greater than 0 and strictly smaller than 1. Note also that, in the case of Crowds, the protocol satisfies the required symmetry, i.e. the elements in the principal diagonal of the matrix of the conditional probabilities are all the same (cf. Prop. 2) and therefore the above factor q is strict.

Example 2. Consider an instance of the Crowds protocol where there are 6 members (m = 6). One of these members is an attacker (c = 1), and the others are honest (n = 5). Assume that p f = 3/4 then we have

p(o i | a i ) = 1 - n -1 m p f = 1 - 4 6 • 3 4 = 1 2
and, for i j,

p(o j | a i ) = 1 m p f = 1 6 • 3 4 = 1 8
Now suppose that, as in Example 1, there are two servers and the honest members are divided into two groups A 1 and A 2 , where A 1 = {1, 2} (resp. A 2 = {3, 4, 5}) are the users which prefer the server 1 (resp. the server 2). Assume that the preference probabilities p 1 = p 2 = 3/4, i.e. that the conditional probabilities p(s | a) are given by

p(s k | a i ) =          3 4 a i ∈ A k 1 4 a i A k
Because of the independence assumption, the conditional probabilities p(o ∧ s | a) can be computed as the product p(o | a) p(s | a) (see Fig. 1). From these we can compute the joint probabilities p(o ∧ s) by using the formula

p(o j ∧ s k ) = i p(o j ∧ s k | a i ) p(a i )
Assuming that the a priori distribution is uniform (p(a i ) = 1 5 ), we obtain the probabilities shown in Fig. 1. From these we can then calculate p(s | o) using the definition

p(s k | o j ) = p(s k ∧ o j ) p(o j )
and the fact that if A is uniformly distributed then also O is uniformly distributed (p(o j ) =

i ) ≤ q α. In fact p(a i | o i ) = 1/2 and max i,k p(a i | o i ∧ s k ) = 2/3.
We note that in some cases the extra information may contradict the original observable. For instance it could be the case that user 1, when she is the originator, has a strong preference for the server 1. So if the attacker receives a message from user 1 addressed to the server 2, it may be better for him to assume that the originator is one (arbitrary) user from the group that favors the server 2, rather than user 1.

We argue, therefore, that the presence of extra information makes the property of probable innocence more difficult to satisfy, because the attacker can use the extra information to improve his guess about the culprit, and he may guess a user which is not necessarily the one who sent the message to him. Therefore it seems reasonable to consider the following definition: -In presence of extra information, a protocol satisfies the safe version of α-probable innocence if ∀i, j. p(a i | o j ) ≤ q α -If ∀i, j. p(a i | o i ) = p(a j | o j ), then the above condition is also necessary, i.e. the protocol satisfies the safe version of α-probable innocence only if ∀i. p(a i | o i ) ≤ q α where q = min i, j,k p(s k |o j )/p(s k |a i ) .

p(o, s) o 1 , s 1 o 2 , s 1 o 3 , s 1 o 4 , s 1 o 5 , s 1 o 1 , s 2 o 2 , s 2 o 3 , s 2 o 4 , s 2 o 5 , s 2
Example 3. Consider again the instance of Crowds like in Example 2, but assume now that the preference probabilities are much higher than before, namely

p(s k | a i ) =          9 10 a i ∈ A k 1 10 a i A k
We can compute the probabilities p(o∧ s | a), p(o∧ s), p(s | o) and p(a | o∧ s) like before.

The results are shown in Fig. 2. We note that in certain cases the extra knowledge dominates over the original observables. For instance, if the adversary receives a message from user 3 addressed to server 1, it is better for him to bet that a sender of group 1 is the originator, rather than user 3. In fact the a posteriori probability of the latter is p(a 3 | o 3 ∧ s 1 ) = 1/6 while the a posteriori probability of (say) user 1 is p(a

1 | o 3 ∧ s 1 ) = 3/8.
Using the values of p(s k | o i ) and p(s k | a i ), the factor q = min i,k p(s k | o i )/p(s k | a i ) in Proposition 4 is evaluated to 2/3, and we can see that Proposition 5 holds for this instance of Crowds, i.e. ∀i, k. p(a i | o i ∧ s k ) ≤ α if and only if ∀i. p(a i | o i ) ≤ q α. In fact p(a i | o i ) = 1/2 and max i, j,k p(a i | o j ∧ s k ) = 3/4.

Vulnerability in presence of extra information

In this section we explore how the definition of α-vulnerability is affected by the presence of extra information. Let us start with the definition of α-vulnerability in presence of the new observables. It is natural to extend the notion of α-vulnerability by considering the (a posteriori) vulnerability when the observables are constituted by the joint random variables O, S , which is given by For the next proposition, we consider the specific case in which the protocol satisfies the symmetry of Crowds. with information about the correlation between a set of observables s 1 , . . . , s and the event that user i is the originator of a message, as formalised by the conditional probability p(s k | a i ). We formalised the idea of probable innocence for such systems, both in standard terms and via the notion of protocol vulnerability, and identified a simple and neat measure of the impact of independent knowledge. Namely, it makes probable innocence (resp. vulnerability) more difficult to achieve by a factor q (resp. q) which depends on the ratio between the probability of the observables conditional to the originator and conditional to the user detected (and, in the case of vulnerability, also from the cardinality of the random variable that represents the extra knowledge).

V(A | O, S ) =
In conclusion, we remark that although the scenario in which attackers possess or can acquire extra knowledge is highly likely, it has so far been ignored. In the near future, we plan to work on the even more interesting scenario in which the attackers use their 'beliefs' about users behaviour to raise the vulnerability of anonymity protocols such as Crowds.

  p(o | a) o 1 o 2 o 3 o 4 o 5 , s | a) o 1 , s 1 o 2 , s 1 o 3 , s 1 o 4 , s 1 o 5 , s 1 o 1 , s 2 o 2 , s 2 o 3 , s 2 o 4 , s 2 o 5 , s 2

Fig. 1 .

 1 Fig. 1. The matrices of the conditional probabilities of Example 2. We use here the notation o, s to represent o ∧ s.

  j ∧ s k ) max i p(a i | o j ∧ s k )Hence we extend α-vulnerability as follows:Definition 5 (α-vulnerability in presence of extra information). Given a real number α ∈ [0, 1], a protocol satisfies α-vulnerability if and only if V(A | O, S ) ≤ α.

  p(o | a) o 1 o 2 o 3 o 4 o 5

  1 5 ). Finally, using Bayes theorem, we can calculate the probabilities p(a| o ∧ s) from p(o ∧ s | a), p(o ∧ s),and p(a). Using the values of p(s k | o i ) and p(s k | a i ), the factor q = min i,k p(s k | o i )/p(s k | a i ) in Proposition 4 is evaluated to 3/4. It is easy to see that Proposition 4 holds for this instance of Crowds, i.e. ∀i, k. p(a i | o i ∧ s k ) ≤ α if and only if ∀i. p(a i | o

2. If the a priori distribution is uniform and

Proof. By definition we have:

Using Bayes theorem we derive:

Because of the independence of O and S for any given originator, we deduce:

1. Since q = max i,k p(s k | a i ), from (5) we derive:

Since the input distribution is uniform:

It is interesting to note that, in the part (2) of Proposition 6, the extra knowledge does not make the protocol more vulnerable. This is because the additional knowledge is sometimes in accordance with the best guess based on the original observable, and sometimes in conflict, but the original observable always dominates, and therefore the additional knowledge is either redundant or disregarded. In any case, it is not used to make the guess. In the general case (represented by the first part of the proposition), however, the additional knowledge may dominate the original observable, and induce the adversary to change his bet, thus increasing his chances. For this reason, the vulnerability increases in general of a factor q.

Conclusion

In this paper we focussed on the Crowds anonymity protocol and asked the question of how its existing analyses are affected by taking into account that attackers may have independent knowledge about users' behaviours. This amounts to providing the attackers


Miguel E Andrés

Catuscia Palamidessi

Peter Van Rossum

Geoffrey Smith

Computing the Leakage of Information-Hiding Systems

Keywords: Specification and verification techniques for finite state systems, Software verification, Model-checking, Information theory, Anonymity, probabilistic automata

We address the problem of computing the information leakage of a system in an efficient way. We propose two methods: one based on reducing the problem to reachability, and the other based on techniques from quantitative counterexample generation. The second approach can be used either for exact or approximate computation, and provides feedback for debugging. These methods can be applied also in the case in which the input distribution is unknown. We then consider the interactive case and we point out that the definition of associated channel proposed in literature is not sound. We show however that the leakage can still be defined consistently, and that our methods extend smoothly.

Introduction

By information hiding, we refer generally to the problem of constructing protocols or programs that protect sensitive information from being deduced by some adversary. In anonymity protocols [START_REF] Chatzikokolakis | Anonymity protocols as noisy channels[END_REF], for example, the concern is to design mechanisms to prevent an observer of network traffic from deducing who is communicating. In secure information flow [START_REF] Sabelfeld | Language-based information flow security[END_REF], the concern is to prevent programs from leaking their secret input to an observer of their public output. Such leakage could be accidental or malicious.

Recently, there has been particular interest in approaching these issues quantitatively, using concepts of information theory. See for example [START_REF] Moskowitz | Covert channels and anonymizing networks[END_REF][START_REF] Clark | Quantitative information flow, relations and polymorphic types[END_REF][START_REF] Deng | Measuring anonymity with relative entropy[END_REF][START_REF] Clarkson | Belief in information flow[END_REF][START_REF] Chatzikokolakis | Anonymity protocols as noisy channels[END_REF]. The secret input S and the observable output O of an information-hiding system are modeled as random variables related by a channel matrix, whose (s, o) entry specifies P (o|s), the conditional probability of observing output o given input s. If we define the vulnerability of S as the probability that the adversary could correctly guess the value of S in one try, then it is natural to measure the information leakage by comparing the a priori vulnerability of S with the a posteriori vulnerability of S after observing O. We consider two measures of leakage: additive, which is the difference between the a posteriori and a priori vulnerabilities; and multiplicative, which is their quotient [START_REF] Smith | On the foundations of quantitative information flow[END_REF][START_REF] Braun | Quantitative notions of leakage for onetry attacks[END_REF].

We thus view a protocol or program as a noisy channel, and we calculate the leakage from the channel matrix and the a priori distribution on S. But, given an operational specification of a protocol or program, how do we calculate the parameters of the noisy channel: the sets of inputs and outputs, the a priori distribution, the channel matrix, and the associated leakage? These are the main questions we address in this paper. We focus on probabilistic automata, whose transitions are labeled with probabilities and actions, each of which is classified as secret, observable, or internal.

We first consider the simple case in which the secret inputs take place at the beginning of runs, and their probability is fixed. The interpretation in terms of noisy channel of this kind of systems is well understood in literature. The framework of probabilistic automata, however, allows to represent more general situations. Thanks to the nondeterministic choice, indeed, we can model the case in which the input distribution is unknown, or variable. We show that the definition of channel matrix extends smoothly also to this case. Finally, we turn our attention to the interactive scenario in which inputs can occur again after outputs. This case has also been considered in literature, and there has been an attempt to define the channel matrix in terms of the probabilities of traces [START_REF] Desharnais | The metric analogue of weak bisimulation for probabilistic processes[END_REF]. However it turns out that the notion of channel is unsound. Fortunately the leakage is still well defined, and it can be obtained in the same way as the simple case.

We consider two different approaches to computing the channel matrix. One uses a system of linear equations as in reachability computations. With this system of equations one can compute the joint matrix, the matrix of probabilities of observing both s and o; the channel matrix is trivially derived from this joint matrix. The other approach starts with a 0 channel matrix, which we call a partial matrix at this point. We iteratively add the contributions in conditional probabilities of complete paths to this partial matrix, obtaining, in the limit, the channel matrix itself. We then group paths with the same secret and the same observable together using ideas from quantitative counterexample generation, namely by using regular expressions and strongly connected component analysis. In this way, we can add the contribution of (infinitely) many paths at the same time to the partial matrices. This second approach also makes it possible to identify which parts of a protocol contribute most to the leakage, which is useful for debugging.

Looking ahead, after reviewing some preliminaries (Section 2) we present restrictions on probabilistic automata to ensure that they have well-defined, finite channel matrices (Section 3). This is followed by the techniques to calculate the channel matrix efficiently (Section 4 and Section 5). We then turn our attention to extensions of our information-hiding system model. We use nondeterministic choice to model the situation where the a priori distribution on the secret is unknown (Section 6). Finally, we consider interactive systems, in which secret actions and observable actions can be interleaved arbitrarily (Section 7).

Preliminaries

Probabilistic automata

This section recalls some basic notions on probabilistic automata. More details can be found in [START_REF] Segala | Modeling and Verification of Randomized Distributed Real-Time Systems[END_REF]. 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).

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

• Q is a finite set of states,
• Σ a finite set of actions,

• q the initial state, and

• α a transition function α : Q → ℘ f (D(Σ × Q)).
Here ℘ f (X) is the set of all finite 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) = ∅ 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(σ). We denote the set of actions occurring in a cycle as CyclesA(M ). 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 σ 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 (σ) µ(a, q ), where last(σ) → µ.

Let Ω q CPaths q (M ) be the sample space, and let F q be the smallest σ-algebra generated by the cones. Then P 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 .

Given a probability space (Ω, F, P ) and two events A, B ∈ F with P (B) > 0, the conditional probability of A given B, P (A | B), is defined as P (A ∩ B)/P (B). We extend by continuity the case P (B) = 0.

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 (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.

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 additive leakage proposed in [START_REF] Braun | Quantitative notions of leakage for onetry attacks[END_REF] 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) 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) 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). (1)
The multiplicative leakage is defined as L × (C, P X ) V(X|Y) V(X) and the additive leakage as L + (C, P X ) V(X|Y) -V(X).

Information Hiding Systems

To formally analyze the information-hiding properties of protocols and programs, we propose to model them as a particular kind of probabilistic automata, which we call Information-Hiding Systems (IHS). Intuitively, an IHS is a probabilistic automaton in which the actions are divided in three (disjoint) categories: those which are supposed to remain secret (to an external observer), those which are visible, and those which are internal to the protocol.

First we consider only the case in which the choice of the secret takes place entirely at the beginning, and is based on a known distribution. Furthermore we focus on fully probabilistic automata. Later in the paper we will relax these constraints. Definition 3.1 (Information-Hiding System). An information-hiding system (IHS) is a quadruple I = (M, Σ S , Σ O , Σ τ ) where M = (Q, Σ, q, α) is a fully probabilistic automaton, Σ = Σ S ∪ Σ O ∪ Σ τ where Σ S , Σ O , and Σ τ are pairwise disjoint sets of secret, observable, and internal actions, and α satisfies the following restrictions:

1. α(q) ∈ D(Σ S × Q), 2. ∀s ∈ Σ S ∃!q . α(q)(s, q) = 0, 3. α(q) ∈ D(Σ O ∪ Σ τ × Q) for q = q, 4. ∀a ∈ (Σ S ∪ Σ O ) . a ∈ CyclesA(M ), 5. P(CPaths(M ) ∩ Paths (M )) = 1.
The first two restrictions are on the initial state and mean that only secret actions can happen there (1) and each of those actions must have non null probability and occur only once (2), Restriction 3 forbids secret actions to happen in the rest of the automaton, and Restriction 4 ensures that the channel associated to the IHS has finitely many inputs and outputs. Finally, Restriction 5 means that infinite computations have probability 0 and therefore we can ignore them. It is easy to check whether a systems satisfies restriction 5 by using backwards DBS techniques backwards from qf .

We now show how to interpret an IHS as a noisy channel. We call trace Σ S (σ) and trace Σ O (σ) the secret and observable traces of σ, respectively. For s ∈ Σ * S , we define

[s] {σ ∈ CPaths(M ) | trace Σ S (σ) = s}; similarly for o ∈ Σ * O , we define [o] {σ ∈ CPaths(M ) | trace Σ O (σ) = o}. Definition 3.2. Given an IHS I = (M, Σ S , Σ O , Σ τ ), its noisy channel is (S, O, P ), where S Σ S , O trace Σ O (CPaths(M )), and P (o | s) P([o] | [s]
). The a priori distribution π ∈ D(S) of I is defined by π(s) α(q)(s, •). If C is the noisy channel of I, the multiplicative and additive leakage of I are naturally defined as

L × (I) L × (C, π) and L + (I) L + (C, π). Example 3.3. Crowds [16] is a well-known anonymity protocol, in which a user init q a q b corr S a b U U A B p 3 p 3 1 3 2 3 1 1-p 1-p p 3 p 3 p 3
Fig. 1: Crowds Protocol (called the initiator) wants to send a message to a web server without revealing his identity. To achieve this, he routes the message through a crowd of users participating in the protocol. Routing is as follows. In the beginning, the initiator randomly selects a user (called a forwarder), possibly himself, and forwards the request to him. A forwarder performs a probabilistic choice. With probability p (a parameter of the protocol) he selects a new user and again forwards the message. With probability 1-p he sends the message directly to the server. One or more users can be corrupted and collaborate with each other to try to find the identity of the initiator. We now show how to model Crowds as an IHS for 2 honest and 1 corrupted user. We assume that the corrupted user immediately forwards messages to the server, as there is no further information to be gained for him by bouncing the message back.

Figure 1 shows the automaton2 . Actions a and b are secret and represent who initiates the protocol; actions A, B, and U are observable; A and B represent who forwards the message to the corrupted user; U represents the fact that the message arrives at the server undetected by the corrupted user. We assume U to be observable to represent the possibility that the message is made publically available at the server's site.

The channel associated to this IHS has S = {a, b}, O = {A, B, U }, and a priori distribution π(a) = 1 3 , π(b) = 2 3 . Its channel matrix is computed in the next section.

Reachability analysis approach

This section presents a method to compute the matrix of joint probabilities P ∧ associated to an IHS, defined as

P ∧ (s, o) P([s] ∩ [o]) for all s ∈ S and o ∈ O.
We omit the subscript ∧ when no confusion arises. From P ∧ we can derive the channel matrix by dividing P ∧ (s, o) by π(s). The leakage can be computed directly from P ∧ , using the second form of the a posteriori vulnerability in (1). We write x λ q for the probability of the set of paths with trace λ ∈ (Σ S ∪ Σ O ) starting from the state q of M :

x

λ q P q ([λ] q ),
where

[λ] q {σ ∈ CPaths q (M ) | trace Σ S ∪Σ O (σ) = λ}.
The following key lemma shows the linear relation between the x λ q 's. We assume, w.l.o.g., that the IHS has a unique final state q f (since it is possible to add an internal transition with probability 1 from every final state to qf ).

Lemma 4.1. Let I = (M, Σ S , Σ O , Σ τ ) be an IHS. For all λ ∈ (Σ S ∪ Σ O ) and q ∈ Q we have x q f = 1,
x λ q f = 0 for λ = , x q = h∈Στ q ∈succ(q) α(q)(h, q ) • x q for q = q f , x λ q = q ∈succ(q) α(q)(first(λ), q ) • x tail(λ) q + h∈Στ α(q)(h, q ) • x λ q for λ = and q = q f . Furthermore, for s ∈ S and o ∈ O we have

P([s] ∩ [o]) = x so q .
Using this lemma, one can compute joint probabilities by solving the system of linear equations in the variables x λ q 's. We note that the system has a solution and such a solution is unique.

Example 4.2. Continuing with the Crowds example, we show how to compute joint probabilities. Note that q f = S. The linear equations from Lemma 4.1 are

x aA init = 1 3 • x A q a , x A q a = p 3 • x A q a + p 3 • x A q b + p 3 • x corr , x A corr = x A S , x bA init = 2 3 • x A q b , x A q b = p 3 • x A q a + p 3 • x A q b + p 3 • x A corr , x A S = 0, x aB init = 1 3 • x B q a , x B q a = p 3 • x B q a + p 3 • x B q b + p 3 • x B corr , x B corr = x B S , x bB init = 2 3 • x B q b , x B q b = p 3 • x B q a + p 3 • x B q b + p 3 • x corr , x B S = 0, x aU init = 1 3 • x U q a , x U q a = p 3 • x U q a + p 3 • x U q b + (1-p) • x S , x corr = x S , x bU init = 2 3 • x U q b , x U q b = p 3 • x U q a + p 3 • x U q b + (1-p) • x S , x S = 1.
Let us fix p = 0.9. By solving the system of linear equations we obtain Fig. 2: CM of Crowds

x aA init = 7 40 , x aB init = 3 40 , x aU init = 1 12 , x bA init = 3 20 , x bB init = 7 20 , x bU init = 1 6 .
We can now compute the channel matrix by dividing each x so init by π(s). The result is shown in Figure 2.

Complexity Analysis

We now analyze the computational complexity for the computation of the channel matrix of a simple IHS. Note that the only variables (from the system of equations in Lemma 4.1) that are relevant for the computation of the channel matrix are those x λ q for which it is possible to get the trace λ starting from state q. As a rough overestimate, for each state q, there are at most |S| • |O| λ's possible: in the initial state one can have every secret and every observable, in the other states no secret is possible and only a suffix of an observable can occur. This gives at most |Q| • |S| • |O| variables. Therefore, we can straightforwardly obtain the desired set of values in O((|Q| • |S| • |O|) 3 ) time (using Gaussian Elimination). Note that using Strassen's methods the exponent reduces to 2.807, this consideration applies to similar results in the rest of the paper as well.

Because secret actions can happen only at the beginning, the system of equations has a special form. The variables of the form x so q only depend on variables of the form x o q (with varying o and q = q) and not on each other. Hence, we can first solve for all variables of the form x o q and then compute the remaining few of the form x so q . Required time for the first step is O((|O| • |Q|) 3 ) and the time for the second step can be ignored.

Finally, in some cases not only do the secret actions happen only at the beginning of the protocol, but the observable actions happen only at the end of the protocol, i.e., after taking a transition with an observable action, the protocol only performs internal actions (this is, for instance, the case for our model of Crowds). In this case, one might as well enter a unique terminal state q f after an observable action happens. Then the only relevant variables are of the form x so q , x o q , and x q f ; the x so q only depends on the x o q , the x o q only depend on x o q (with the same o, but varying q's) and on x q f and x q f = 1. Again ignoring the variables x so q for complexity purposes, the system of equations has a block form with |O| blocks of (at most) |Q| variables each. Hence the complexity in this case decreases to O(|O| • |Q| 3 ).

The Iterative Approach

We now propose a different approach to compute channel matrices and leakage. The idea is to iteratively construct the channel matrix of a system by adding probabilities of sets of paths containing paths with the same observable trace o and secret trace s to the (o|s) entry of the matrix.

One reason for this approach is that it allows us to borrow techniques from quantitative counterexample generation. This includes the possibility of using or extending counterexample generation tools to compute channel matrices or leakage. Another reason for this approach is the relationship with debugging. If a (specification of a) system has a high leakage, the iterative approach allows us to determine which parts of the system contribute most to the high leakage, possibly pointing out flaws of the protocol.

Finally, if the system under consideration is very large, the iterative approach allows us to only approximate the leakage (by not considering all paths, but only the most relevant ones) under strict guarantees about the accuracy of the approximation. We will focus on the multiplicative leakage; similar results can be obtained for the additive case.

Partial matrices

We start by defining a sequence of matrices converging to the channel matrix by adding the probability of complete paths one by one. We also define partial version of the a posteriori vulnerability and the leakage. Later, we show how to use techniques from quantitative counterexample generation to add probabilities of many (maybe infinitely many) complete paths all at once. Definition 5.1. Let I = (M, Σ S , Σ O , Σ τ ) be an IHS, π its a priori distribution, and σ 1 , σ 2 , . . . an enumeration of the set of complete paths of M . We define the partial matrices P k : S × O → [0, 1] as follows P 0 (o|s) 0, P k+1 (o|s)

     P k (o|s) + P( σ k+1 ) π(s) if trace Σ O (σ k+1 ) = o and trace Σ S (σ k+1 ) = s, P k (o|s)
otherwise.

We define the partial vulnerability V k S,O as o max s P k (o|s) • π(s), and the partial multiplicative leakage

L k × (I) as V k S,O /max s π(s).
The following lemma states that partial matrices, a posteriori vulnerability, and leakage converge to the correct values. Lemma 5.2. Let I = (M, Σ S , Σ O , Σ τ ) be an IHS. Then 1. P k (o|s) ≤ P k+1 (o|s), and lim k→∞ P k (o|s) = P (o|s),

2. V k S,O ≤ V k+1 S,O , and lim k→∞ V k S,O = V(S|O), 3. L k × (I) ≤ L k+1 × (I), and lim k→∞ L k × (I) = L × (I).
Since rows must sum up to 1, this technique allow us to compute matrices up to given error . We now show how to estimate the error in the approximation of the multiplicative leakage.

Proposition 5.3. Let (M, Σ S , Σ O , Σ τ ) be an IHS. Then we have

L k × (I) ≤ L × (I) ≤ L k × (I) + |S| i=1 (1 -p k i ),
where p k i denotes the mass probability of the i-th row of P k , i.e. p k i o P k (o|s i ).

On the computation of partial matrices.

After showing how partial matrices can be used to approximate channel matrices and leakage we now turn our attention to accelerating the convergence. Adding most likely paths first is an obvious way to increase the convergence rate. However, since automata with cycles have infinitely many paths, this (still) gives an infinite amount of path to process. Processing many paths at once (all having the same observable and secret trace) tackles both issues at the same time: it increases the rate of convergence and can deal with infinitely many paths at the same time, Interestingly enough, these issues also appear in quantitative counterexample generation. In that area, several techniques have already been provided to meet the challenges; we show how to apply those techniques in the current context. We consider two techniques: one is to group paths together using regular expressions, the other is to group paths together using strongly connected component analysis.

Regular expressions. In [START_REF] Daws | Symbolic and parametric model checking of discrete-time markov chains[END_REF], regular expressions containing probability values are used to reason about traces in Markov Chains. This idea is used in [START_REF] Damman | Regular expressions for PCTL counterexamples[END_REF] in the context of counterexample generation to group together paths with the same observable behaviour. The regular expressions are over pairs p, q with p a probability value and q a state, to be able to track both probabilities and observables. We now use the same idea to group together paths with the same secret action and the same observable actions.

We consider regular expressions over triples of the form a, p, q with p ∈ [0, 1] a probability value, a ∈ Σ an action label and q ∈ Q a state. Regular expressions represent sets of paths as in [START_REF] Damman | Regular expressions for PCTL counterexamples[END_REF]. We also take the probability value of such a regular expression from that paper. Definition 5.4. The function val : R(Σ) → R evaluates regular expressions:

val ( ) 1, val (r • r ) val (r) × val (r ), val ( a, p, q ) p, val (r * ) 1 if val (r) = 1, val (r + r ) val (r) + val (r ), val (r * ) 1 1-val(r) if val (r) = 1.
The idea is to obtain regular expressions representing sets of paths of M , each regular expression will contribute in the approximation of the channel matrix and leakage. Several algorithms to translate automata into regular expressions have been proposed (see [START_REF] Neumann | Converting deterministic finite automata to regular expressions[END_REF]). Finally, each term of the regular expression obtained can be processed separately by adding the corresponding probabilities [START_REF] Daws | Symbolic and parametric model checking of discrete-time markov chains[END_REF] to the partial matrix.

As mentioned before, all paths represented by the regular expression should have the same observable and secret trace in order to be able to add its probability to a single element of the matrix. To ensure that condition we request the regular expression to be normal, i.e., of the form r 1 + • • • + r n with the r i containing no +'s.

For space reasons, instead of showing technical details we only show an example.

Example 5.5. We used JFLAP 7.0 [START_REF]Jflap website[END_REF] to obtain the regular expression r r 1 + r 2 + • • • + r 10 equivalent to the automaton in Figure 1.

r 1 b, 2 3 , q b • r • B, 0.3, corr • τ, 1, S , r 2 b, 2 3 , q b • r • τ, 0.3, q a • τ, 0.3, q a • A, 0.3, corr • τ, 1, S , r 3 a, 1 3 , q a • τ, 0.3, q a • A, 0.3, corr • τ, 1, S , r 4 b, 2 3 , q b • r • U, 0.1, S , r 5 a, 1 3 , q a • τ, 0.3, q a • τ, 0.3, q b • r • B, 0.3, corr • τ, 1, S , r 6 b, 2 3 , q b • r • τ, 0.3, q a • τ, 0.3, q a • U, 0.1, S , r 7 a, 1 3 , q a • τ, 0.3, q a • U, 0.1, S , r 8 a, 1 3 , q a • τ, 0.3, q a • τ, 0.3, q b • r • τ, 0.3, q a • τ, 0.3, q a • A, 0.3, corr • τ, 1, S , r 9 a, 1 3 , q a • τ, 0.3, q a • τ, 0.3, q b • r • U, 0.1, S , r 10 a, 1 3 , q a • τ, 0.3, q a • τ, 0.3, q b • r • τ, 0.3, q a • τ, 0.3, q a • U, 0.1, S ,
where r ( τ, 0.3, q b • ( τ, 0.3, q a • τ, 0.3, q a • τ, 0.3, q b ) ). We also note

val (r 1 ) = 7 20 (b, B), val (r 2 ) = 3 20 (b, A), val (r 3 ) = 1 7 (a, A), val (r 4 ) = 7 60 (b, U ), val (r 5 ) = 3 40 (a, B), val (r 6 ) = 1 20 (b, U ), val (r 7 ) = 1 21 (a, U ), val (r 8 ) = 9 280 (a, A), val (r 9 ) = 1 40 (a, U ), val (r 10 ) = 3 280 (a, U )
, where the symbols between brackets denote the secret and observable traces of each regular expression. Now we have all the ingredients needed to define partial matrices using regular expressions.

Definition 5.6. Let I = (M, Σ S , Σ O , Σ τ ) be an IHS, π its a priori distribution, and r = r 1 + r 2 + • • • + r n a regular expression equivalent to M in normal form. We define for k = 0, 1, . . . , n the matrices P k : S × O → [0, 1] as follows

P k (o|s) =          0 if k = 0, P k-1 (o|s) + val(r k ) π(s) if k = 0 and trace Σ O (r k ) = o and trace Σ S (r k ) = s, P k-1 (o|s)
otherwise.

Note that in the context of Definition 5.6, we have P n = P .

SCC analysis approach. In [START_REF] Andrés | Significant diagnostic counterexamples in probabilistic model checking[END_REF], paths that only differ in the way they traverse strongly connected components (SCC's) are grouped together. Note that in our case, such paths have the same secret and observable trace since secret and observable actions cannot occur on cycles. Following [START_REF] Andrés | Significant diagnostic counterexamples in probabilistic model checking[END_REF], we first abstract away the SCC's, leaving only probabilistic transitions that go immediately from an entry point of the SCC to an exit point (called input and output states in [START_REF] Andrés | Significant diagnostic counterexamples in probabilistic model checking[END_REF]). This abstraction happens in such a way that the observable behaviour of the automaton does not change.

Again, instead of going into technical details (which also involves translating the work [START_REF] Andrés | Significant diagnostic counterexamples in probabilistic model checking[END_REF] from Markov chains to fully probabilistic automata), we show an example. Figure 3 shows the automaton obtained after abstracting SCC. In the following we show the set of complete paths of the automaton, together with their corresponding probabilities and traces

σ 1 init a -→ q a A -→ corr τ -→ S, P(σ 1 ) = 7 40 , (a, A), σ 2 init b -→ q b B -→ corr τ -→ S, P(σ 2 ) = 7 20 , (b, B), σ 3 init a -→ q a U -→ S, P(σ 3 ) = 1 12 , (a, U ), σ 4 init b -→ q b U -→ S, P(σ 4 ) = 1 6 , (b, U ), σ 5 init a -→ q a B -→ corr τ -→ S, P(σ 5 ) = 3 40 , (a, B), σ 6 init b -→ q b A -→ corr τ -→ S, P(σ 6 ) = 3 20 , (b, A).
Note that the SCC analysis approach groups more paths together (for instance σ 1 group together the same paths than the regular expressions r 3 and r 8 in the examples of this section), as a result channel matrix and leakage are obtained faster. On the other hand, regular expressions are more informative providing more precise feedback.

Identifying high-leakage sources

We now describe how to use the techniques presented in this section to identify sources of high leakage of the system. Remember that the a posteriori vulnerability can be expressed in terms of joint probabilities

V(S | O) = o max s P([s] ∩ [o]).
This suggests that, in case we want to identify parts of the system generating high leakage, we should look at the sets of paths

[o 1 ] ∩ [s 1 ], . . . , [o n ] ∩ [s n ] where {o 1 , . . . o n } = O and s i ∈ arg (max s P([o i ] ∩ [s])).
In fact, the multiplicative leakage is given dividing V(S | O) by V(S), but since V(S) is a constant value (i.e., it does not depend on the row) it does not play a role here. Similarly for the additive case.

The techniques presented in this section allow us to obtain such sets and, furthermore, to partition them in a convenient way with the purpose of identifying states/parts of the system that contribute the most to its high probability. Indeed, this is the aim of the counterexamples generation techniques previously presented. For further details on how to debug sets of paths and why these techniques meet that purpose we refer to [START_REF] Aljazzar | Debugging of dependability models using interactive visualization of counterexamples[END_REF][START_REF] Damman | Regular expressions for PCTL counterexamples[END_REF][START_REF] Andrés | Significant diagnostic counterexamples in probabilistic model checking[END_REF].

Example 5.8. To illustrate these ideas, consider the path σ 1 of the previous example; this path has maximum probability for the observable A. By inspecting the path we find the transition with high probability q a A → corr. This suggests to the debugger that the corrupted user has an excessively high probability of intercepting a message from user a in case he is the initiator.

In case the debugger requires further information on how corrupted users can intercept messages, the regular expression approach provides further/more-detailed information. For instance, we obtain further information by looking at regular expressions r 3 and r 8 instead of path σ 1 (in particular it is possible to visualize the different ways the corrupted user can intercept the message of user a when he is the generator of the message).

Information Hiding Systems with Variable a Priori

In Section 3 we introduced a notion of IHS in which the distribution over secrets is fixed. However, when reasoning about security protocols this is often not the case. In general we may assume that an adversary knows the distribution over secrets in each particular instance, but the protocol should not depend on it. In such scenario we want the protocol to be secure, i.e. ensuring low enough leakage, for every possible distribution over secrets. This leads to the definition of maximum leakage. Definition 6.1 ( [START_REF] Smith | On the foundations of quantitative information flow[END_REF][START_REF] Braun | Quantitative notions of leakage for onetry attacks[END_REF]). Given a noisy channel C = (S, O, P ), we define the maximum multiplicative and additive leakage (respectively) as

ML × (C) max π∈D(S)
L × (C, π), and

ML + (C) max π∈D(S) L + (C, π).
In order to model this new scenario where the distribution over secrets may change, the selection of the secret is modeled as nondeterministic choice. In this way such a distribution remains undefined in the protocol/automaton. We still assume that the choice of the secret happens at the beginning, and that we have only one secret per run. We call such automaton an IHS with variable a priori. Definition 6.2. An IHS with variable a priori is a quadruple

I = (M, Σ S , Σ O , Σ τ ) where M = (Q, Σ, q, α) is a probabilistic automaton, Σ = Σ S ∪ Σ O ∪ Σ τ where Σ S ,
Σ O , and Σ τ are pairwise disjoint sets of secret, observable, and internal actions, and α satisfies the following restrictions:

1. α(q) ⊆ D(Σ S × Q), 2. |α(q)| = |S| ∧ ∀s ∈ Σ S . ∃ q . π(s, q) = 1, for some π ∈ α(q), 3. α(q) ⊆ D(Σ O ∪ Σ τ × Q) and |α(q)| ≤ 1, for all q = q, 4. ∀a ∈ (Σ S ∪ Σ O ) . a ∈ CyclesA(M ), 5.
∀q, s ∀π ∈ α(q) . (π(s, q) = 1 ⇒ P(CPaths q (M ) ∩ Paths * q (M )) = 1). Restrictions 1, 2 and 3 imply that the secret choice is non deterministic and happens only at the beginning. Additionally, 3 means that all the other choices are probabilistic. Restriction 4 ensures that the channel associated to the IHS has finitely many inputs and outputs. Finally, 5 implies that, after we have chosen a secret, every computation terminates except for a set with null probability.

Given an IHS with variable a priori, by fixing the a priori distribution we can obtain a standard IHS in the obvious way: Definition 6.3. Let I = ((Q, Σ, q, α), Σ S , Σ O , Σ τ ) be an IHS with variable a priori and π a distribution over S. We define the IHS associated to (I, π) as I π = ((Q, Σ, q, α ), Σ S , Σ O , Σ τ ) with α (q) = α(q) for all q = q and α (q)(s, •) = π(s).

The following result says that the conditional probabilities associated to an IHS with variable a priori are invariant with respect to the a priori distribution. This is fundamental in order to interpret the IHS as a channel. Proposition 6.4. Let I be an IHS with variable a priori. Then for all π, π ∈ D(S) such that π(s) = 0 and π (s) = 0 for all s ∈ S we have that P Iπ = P I π .

Proof. The secret s appears only once in the tree and only at the beginning of paths, hence

P([s] ∩ [o]) = α (q)(s, •) P qs ([o]) and P([s]) = α (q)(s, •). Therefore P([o] | [s]) = P qs ([o]
), where q s is the state after performing s. While α (q)(s, •) is different in I π and I π , P qs ([o]) is the same, because it only depends on the parts of the paths after the choice of the secret.

Note that, although in the previous proposition we exclude input distributions with zeros, the concepts of vulnerability and leakage also make sense for these distributions 3 .

This result implies that we can define the channel matrix of an IHS I with variable a priori as the channel matrix of I π for any π, and we can compute it, or approximate it, using the same techniques of previous sectionsSimilarly we can compute or approximate the leakage for any given π.

We now turn the attention to the computation of the maximum leakage. The following result from the literature is crucial for our purposes. Proposition 6.5 ([3]). Given a channel C, arg max π∈D(S) L × (C, π) is the uniform distribution, and arg max π∈D(S) L + (C, π) is a corner point distribution, i.e. a distribution π such that π(s) = 1 κ on κ elements of S, and π(s) = 0 on all the other elements. As an obvious consequence, we obtain: Corollary 6.6. Given an IHS I with variable a priori, we have ML × (I) = L × (I π ), where π is the uniform distribution, and ML + (I) = L + (I π ), where π is a corner point distribution. Corollary 6.6 gives us a method to compute the maxima leakages of I. In the multiplicative case the complexity is the same as for computing the leakage 4 . In the additive case we need to find the right corner point, which can be done by computing the leakages for all corner points and then comparing them. This method has exponential complexity (in |S|) as the size of the set of corner points is 2 |S| -1. We conjecture that this complexity is intrinsic, i.e. that the problem is NP-hard5 .

Interactive Information Hiding Systems

We now consider extending the framework to interactive systems, namely to IHS's in which the secrets and the observables can alternate in an arbitrary way. The secret part of a run is then an element of Σ * S , like the observable part is an element of Σ * O . The idea is that such a system models an interactive play between a source of secret information, and a protocol or program that may produce, each time, some observable in response.

Since each choice is associated to one player of this "game", it seems natural to impose that in a choice the actions are either secret or observable/hidden, but not both.

The main novelty and challenge of this extension is that part of the secrets come after observable events, and may depend on them. Definition 7.1. Interactive IHS's are defined as IHS's (Definition 3.1), except that Restrictions 1 to 3 are replaced by α(q

) ∈ D(Σ S × Q) ∪ D(Σ -Σ S × Q).
Example 7.2. Consider an Ebay-like auction protocol with one seller and two possible buyers, one rich and one poor. The seller first publishes the item he wants to sell, which can be either cheap or expensive. Then the two buyers start bidding. At the end, the seller looks at the profile of the bid winner and decides whether to sell the item or cancel the transaction. Figure 7 illustrates the automaton representing the protocol, for certain given probability distributions.

Fig. 4: Ebay Protocol

We assume that the identities of the buyers are secret, while the price of the item and the seller's decision are observable. We ignore for simplicity the internal actions which are performed during the bidding phase. Hence Σ O = {cheap, expensive, sell, cancel}, Σ τ = ∅, S = Σ S = {poor, rich}, and O = {cheap, expensive} × {sell, cancel}. The distributions on S and O are defined as usual. For instance we have P([cheap sell]) = P({q

0 cheap -→ q 1 poor -→ q 3 sell -→ q 7 , q 0 cheap -→ q 1 rich -→ q 3 sell -→ q 7 }) = 2 3 • 3 5 • 4 5 + 2 3 • 2 5 • 3 4 = 13 25 .
Let us now consider how to model the protocol in terms of a noisy channel. It would seem natural to define the channel associated to the protocol as the triple (S, O, P ) where

P (o | s) = P([o] | [s]) = P([s]∩[o]) P([s]
) . This is, indeed, the approach taken in [START_REF] Desharnais | The metric analogue of weak bisimulation for probabilistic processes[END_REF]. For instance, with the protocol of Example 7.2, we would have:

P([cheap sell] | [poor]) = P([poor] ∩ [cheap sell]) P([poor]) = 2 3 • 3 5 • 4 5 2 3 • 3 5 + 1 3 • 1 5 = 24 35 . (2)
However, it turns out that in the interactive case (in particular when the secrets are not in the initial phase), it does not make sense to model the protocol in terms of a channel. At least, not a channel with input S. In fact, the matrix of a channel is supposed to be invariant with respect to the input distribution (like in the case of the IHS's with variable a priori considered in previous section), and this is not the case here. The following is a counterexample.

Example 7.3. Consider the same protocol as in Example 7.2, but assume now that the distribution over the choice of the buyer is uniform, i.e. α(q 1 )(poor, q 3 ) = α(q 1 )(rich, q 4 ) = α(q 2 )(poor, q 5 ) = α(q 2 )(rich, q 6 ) = 1 2 . Then the conditional probabilities are dif-ferent than those for Example 7.2. In particular, in contrast to (2), we have

P([cheap sell] | [poor]) = P([poor] ∩ [cheap sell]) P([poor]) = 2 3 • 1 2 • 4 5 2 3 • 1 2 + 1 3 • 1 2 = 8 15 .
The above observation, i.e. the fact that the conditional probabilities depend on the input distribution, makes it unsound to reason about certain information-theoretic concepts in the standard way. For instance, the capacity is defined as the maximum mutual information over all possible input distributions, and the traditional algorithms to compute it are based on the assumption that the channel matrix remains the same while the input distribution variates. This does not make sense anymore in the interactive setting.

However, when the input distribution is fixed, the matrix of the joint probabilities is well defined as P ∧ (s, o) = P([s] ∩ [o]), and can be computed or approximated using the same methods as for simple IHS's. The a priori probability and the channel matrix can then be derived in the standard way:

π(s) = o P ∧ (s, o), P (o | s) = P ∧ (s, o) π(s) .
Thanks to the formulation (1) of the a posteriori vulnerability, the leakage can be computed directly using the joint probabilities. 75 . We note that our techniques to compute channel matrices and leakage extend smoothly to the case where secrets are not required to happen at the beginning. However, no assumptions can be made about the occurrences of secrets (they do not need to occur at the beginning anymore). This increases the complexity of the reachability technique to O((|S| • |O| • |Q|) 3 ). On the other hand, complexity bounds for the iterative approach remain the same.

Related Work

To the best of our knowledge, this is the first work dealing with the efficient computation of channel matrices and leakage. However, for the simple scenario, channel matrices can be computed using standard model checking techniques. Chatzikokolakis et al. [START_REF] Chatzikokolakis | Anonymity protocols as noisy channels[END_REF] have used Prism [START_REF]Prism website[END_REF] to model Crowds as a Markov Chain and compute its channel matrix. Each conditional probability P (o|s) is computed as the probability of reaching a state where o holds starting from the state where s holds. Since for the simple version of IHS's secrets occur only once and before observables (as in Crowds), such a reachability probability equals P (o|s). This procedure leads to O(|S| • |O| • |Q| 3 ) time complexity to compute the channel matrix, where Q is the space state of the Markov Chain.

Note that the complexity is expressed in terms of the space state of a Markov Chain instead of automaton. Since Markov Chains do not carry information in transitions With respect to the interactive scenario, standard model checking techniques do not extend because multiple occurrences of the same secret are allowed (for instance in our Ebay example, P (cheap sell|rich) cannot be derived from reachability probabilities from the two different states of the automaton where rich holds).

Conclusion and Future Work

In this paper we have addressed the problem of computing the information leakage of a system in an efficient way. We have proposed two methods: one based on reachability techniques; the other based on quantitative counterexample generation.

We plan to use tools developed for counterexamples generation (in particular the Prism implementation of both techniques presented in Section 5) in order to compute/approximate leakage of large scale protocols. We also intend to investigate in more depth how the results obtained from those tools can be used to identify flaws of the protocol causing high leakage.

In Section 7 we have shown that when the automaton is interactive we cannot define its channel in the standard way. An intriguing problem is how to extend the notion of channel so to capture the dynamic nature of interaction. One idea is to use channels with history and/or feedback. Another idea is to lift the inputs from secrets to schedulers on secrets, i.e. to functions from paths to distributions over secrets.

1 Fig. 3 :

 13 Fig. 3: Crowds after the SCC analysis

Example 7 . 4 .

 74 Consider the Ebay protocol I presented in Example 7.2. The matrix of the joint probabilities P ∧ (s, o) is: cheap sell cheap cancel expensive sell expensive cancel poor Furthermore π(poor) = 7 15 and π(rich) = 8 15 . Hence we have L × (I) = 51 40 and L + (I) = 11

Fig. 5 :

 5 Fig.5: Automaton vs Markov Chain they have a larger state space than an equivalent automaton. Figure8illustrates this: to model the automaton (left hand side) we need to encode the information in its transitions into states of the Markov Chain (right hand side). Therefore, the probability of seeing observation a and then c in the automaton can be computed as the probability of reaching the state ac. The Markov Chain used for modeling Crowds (in our two honest and one corrupted user configuration) has 27 states.For this reason we conjecture that our complexityO(|O| • |Q| 3 ) is a considerable improvement over the one on Markov Chains O(|S| • |O| • |Q| 3 ).With respect to the interactive scenario, standard model checking techniques do not extend because multiple occurrences of the same secret are allowed (for instance in our Ebay example, P (cheap sell|rich) cannot be derived from reachability probabilities from the two different states of the automaton where rich holds).

Figure 8

 8 illustrates this: to model the automaton (left hand side) we need to encode the information in its transitions into states of the Markov Chain (right hand side). Therefore, the probability of seeing observation a and then c in the automaton can be computed as the probability of reaching the state ac. The Markov Chain used for modeling Crowds (in our two honest and one corrupted user configuration) has 27 states.For this reason we conjecture that our complexity O(|O| • |Q| 3 ) is a considerable improvement over the one on Markov Chains O(|S| • |O| • |Q| 3 ).

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's sake we use here the terminology and formulation of[START_REF] Braun | Quantitative notions of leakage for onetry attacks[END_REF].

For the sake of simplicity, we allow the initiator of the protocol to send the message to the server also in the first step of the protocol.

We assume that conditional probabilities are extended by continuity on such distributions.

Actually we can compute it even faster using an observation from[START_REF] Smith | On the foundations of quantitative information flow[END_REF] which says that the leakage on the uniform distribution can be obtained simply by summing up the maximum elements of each column of the channel matrix.

Since submitting this paper, we have proved that our conjecture is true.

The work of Catuscia Palamidessi has been partially supported by the project ANR-09-BLAN-0169-01 PANDA: PArallel aNd Distributed Analysis.