Konstantinos Chatzikokolakis

Catuscia Palamidessi
email: catuscia@lix.polytechnique.fr

Christelle Braun
email: braun@lix.polytechnique.fr

Under consideration for publication in Math. Struct. in Comp. Science

published or not. The documents may come

Introduction

During the last decade, internet activities have become an important part of many people's lives. As the number of these activities increases, there is a growing amount of personal information about the users that is stored in electronic form and that is usually transferred using public electronic means. This makes it feasible and often easy to collect, transfer and process a huge amount of information about a person. As a consequence, the need for mechanisms to protect such information is compelling.

A recent example of such privacy concerns are the so-called "biometric" passports. These passports, used by many countries and required by all visa waiver travelers to the United States, include an RFID chip containing information about the passport's owner. These chips can be read wirelessly without any contact with the passport and without the owner even knowing that his passport is being read. It is clear that such devices need protection mechanisms to ensure that the contained information will not be revealed to any non-authorized person.

In general, privacy can be defined as the ability of users to prevent information about themselves from becoming known to people other than those they choose to give the information to. We can further categorize privacy properties based on the nature of the hidden information. Data protection usually refers to confidential data like the credit card number. Anonymity, on the other hand, concerns the identity of the user who performed a certain action. Unlinkability refers to the link between the information and the user, and unobservability regards the actions of a user. Information-hiding protocols aim at ensuring a privacy property during an electronic transaction. For example, the voting protocol Foo 92 [START_REF] Fujioka | A practical secret voting scheme for large scale elections[END_REF] allows a user to cast a vote without revealing the link between the voter and the vote. The anonymity protocol Crowds [START_REF] Reiter | Crowds: anonymity for Web transactions[END_REF] allows a user to send a message on a public network without revealing the identity of the sender. These kinds of protocols often use randomization to introduce noise, thus limiting the inference power of a malicious observer.

Information theory

At an abstract level information-hiding protocols can be viewed as information-theoretic channels. A channel consists of a set of input values S, a set of output values O (the observables) and a transition matrix which gives the conditional probability p(o|s) of producing o as the output when s is the input. In the case of privacy preserving protocols, S contains the secret information that we want to protect and O the facts that the attacker can observe. This framework allows us to apply concepts from information theory to reason about the knowledge that the attacker can gain about the input by observing the output of the protocol (information leakage). This leakage is usually expressed in terms of mutual information, that is the difference between the a priori entropy (the initial uncertainty of the attacker) and the a posteriori entropy (the uncertainty of the attacker after the observation). The channel capacity, that is defined as the maximum mutual information under all possible a priori distributions, represents the worst case of leakage.

Hypothesis testing

Information theory is parametric on the notion of entropy. The most popular one is Shannon entropy, because of its relation with the channel's transmission rate. With respect to the problem of information-hiding, however, one of the most natural notion is arguably the Rényi min entropy [START_REF] Rényi | On Measures of Entropy and Information[END_REF]. As discussed by Smith [START_REF] Smith | On the foundations of quantitative information flow[END_REF], this notion represents well the one-try attacks, and it is strictly related to the problem of hypothesis testing and to the Bayes risk.

In information-hiding systems the attacker finds himself in the following scenario: he cannot directly detect the information of interest, namely the actual value of the random variable S ∈ S, but he can discover the value of another random variable O ∈ O which depends on S according to a known conditional distribution. This kind of situation is quite common also in other disciplines, like medicine, biology, and experimental physics, to mention a few. The attempt to infer S from O is called hypothesis testing (the "hy-pothesis" to be validated is the actual value of S), and it has been widely investigated in statistics.

One of the most used approaches to this problem is the Bayesian method, which consists in assuming as known the a priori probability of the distribution of the hypotheses, and in deriving from that (and from the matrix of the conditional probabilities) the a posteriori distribution after a certain fact has been observed. It is well known that the best strategy for the adversary is to apply the MAP (Maximum Aposteriori Probability) criterion, which, as the name says, dictates that one should choose the hypothesis with the maximum a posteriori probability for the given observation. "Best" means that this strategy induces the smallest probability of error in the guess of the hypothesis. The probability of error, in this case, is called Bayes risk. The a posteriori Rényi min entropy is the logarithm of the converse of the Bayes risk † . In [START_REF] Chatzikokolakis | On the Bayes risk in information-hiding protocols[END_REF], we proposed to define the degree of protection provided by a protocol as the Bayes risk associated to the matrix. [START_REF] Mciver | Compositional closure for bayes risk in probabilistic noninterference[END_REF] have shown that the Bayes risk is the maximally discriminating among various notions of entropy, when compositionality is taken into account.

A major problem with the Bayesian method is that the a priori distribution is not always known. This is particularly true in security applications. In some cases, it may be possible to approximate the a priori distribution by statistical inference, but in most cases, especially when the input information changes over time, it may not. Thus other methods need to be considered, which do not depend on the a priori distribution. One such method is the one based on the so-called Maximum Likelihood criterion.

Contribution

In this paper we consider the Bayesian hypothesis-testing approach to the one-try attacks, under the assumption that the input distribution is known. We consider as degree of protection the Bayes risk, i.e. the probability of error of an adversary trying to discover the secret using the MAP rule.

Next, we consider a probabilistic process algebra for the specification of informationhiding protocols, and we investigate which constructs in the language can be used safely in the sense that by applying them to a term, the degree of protection provided by the term does not decrease. This provides a criterion to build specifications in a compositional way, while preserving the degree of protection.

We apply these compositional methods to the example of the Dining Cryptographers, and we are able to strengthen the strong anonymity result by Chaum. Namely we show that we can have strong anonymity even if some coins are unfair, provided that there is a spanning tree of fair ones. This result is obtained by adding processes representing coins to the specification and using the fact that this can be done with a safe construct.

Plan of the paper

In the next section we recall some basic notions. Section 3 introduces the language CCS p . Section 4 shows how to model protocols and process terms as channels. Section 5 discusses hypothesis testing and presents some properties of the probability of error. Section 6 characterizes the constructs of CCS p which are safe. Section 7 applies previous results to find a new property of the Dining Cryptographers. Section 8 discusses related work. Section 9 concludes.

Preliminaries

In this section we give a brief overview of the technical concepts from the literature that will be used through the paper. More precisely, we recall some basic notions of metric spaces (see for instance [START_REF] Munkres | Topology: A First Course[END_REF]), probability theory (see for instance [START_REF] Chung | A Course in Probability Theory[END_REF]) and probabilistic automata [START_REF] Segala | Modeling and Verification of Randomized Distributed Real-Time Systems[END_REF][START_REF] Segala | Probabilistic simulations for probabilistic processes[END_REF].

Metric spaces

A metric space is a pair (X, d) where X is a set and d : X × X → [0, ∞) is a function (called distance or metric) which satisfies the following properties:

for all x, y ∈ X, d(x, y) = 0 if and only if x = y, -for all x, y ∈ X, d(x, y) = d(y, x), -for all x, y, z ∈ X, d(x, y) ≤ d(y, z) + d(z, y).

Let (X, d) be a metric space. A sequence of elements in X is converging if it has a limit in X with respect to the distance d. The metric space (X, d) is called compact if every sequence of elements in X has a converging subsequence.

Probability spaces

Let Ω be a set. A σ-field over Ω is a collection F of subsets of Ω closed under complement and countable union and such that Ω ∈ F. If B is a collection of subsets of Ω then the σ-field generated by B is defined as the smallest σ-field containing U (its existence is ensured by the fact that the intersection of an arbitrary set of σ-fields containing B is still a σ-field containing B).

A measure on F is a function µ :

F → [0, ∞] such that 1 µ(∅) = 0 and 2 µ( i C i ) = i µ(C i ) if {C i } i is a countable collection of pairwise disjoint elements of F.
A probability measure on F is a measure µ on F such that µ(Ω) = 1. A probability space is a tuple (Ω, F, µ) where Ω is a set, called the sample space, F is a σ-field on Ω and µ is a probability measure on F. The elements of a σ-field F are also called events.

We will denote by δ(x) (called the Dirac measure on x) the probability measure s.t. δ(x)({y}) = 1 if y = x, and δ(x)({y}) = 0 otherwise. If {c i } i are convex coefficients, and {µ i } i are probability measures, we will denote by i c i µ i the probability measure defined as

( i c i µ i )(A) = i c i µ i (A).
If A, B are events then A ∩ B is also an event. If µ(A) > 0 then we can define the conditional probability p(B|A), meaning "the probability of B given that A holds", as

p(B|A) = µ(A ∩ B) µ(A)
Note that p(•|A) is a new probability measure on F. In continuous probability spaces, where many events have zero probability, it is possible to generalize the concept of conditional probability to allow conditioning on such events. However, this is not necessary for the needs of this paper. Thus we will use the above "traditional" definition of conditional probability and make sure that we never condition on events of zero probability.

A probability space and the corresponding probability measure are called discrete if Ω is countable and F = 2 Ω . In this case, we can construct µ from a function p : Ω → [0, 1] satisfying x∈Ω p(x) = 1 by assigning µ({x}) = p(x). The set of all discrete probability measures with sample space Ω will be denoted by Disc(Ω).

Probabilistic automata

A probabilistic automaton M is a tuple (St, T init , Act, T ) where St is a set of states, T init ∈ St is the initial state, Act is a set of actions and T ⊆ St × Act × Disc(St) is a transition relation. Intuitively, if (T, a, µ) ∈ T then there is a transition from the state T performing the action a and leading to a distribution µ over the states of the automaton. (We use T for states instead of s because later in the paper states will be (process) terms, and s will be used for sequences of actions.) We also write T a -→ µ if (T, a, µ) ∈ T . The idea is that the choice of transition among the available ones in T is performed nondeterministically, and the choice of the target state among the ones allowed by µ (i.e., those states T ′ such that µ(T ′ ) > 0) is performed probabilistically. A probabilistic automaton M is fully probabilistic if from each state of M there is at most one transition available.

An execution fragment α of a probabilistic automaton is a (possibly infinite) sequence T 0 a 1 T 1 a 2 T 2 . . . of alternating states and actions, such that for each i there is a transition (T i , a i+1 , µ i ) ∈ T and µ i (T i+1 ) > 0. We will use fst(α), lst(α) to denote the first and last state of a finite execution fragment α respectively. An execution (or history) is an execution fragment such that fst(α) = T init . An execution α is maximal if it is infinite or there is no transition from lst(α) in T . We denote by exec * (M), exec ⊥ (M), and exec(M) the set of all the finite, all the non-maximal, and all executions of M, respectively.

A scheduler of a probabilistic automaton M = (St, T init , Act, T ) is a function

ζ : exec ⊥ (M) → T such that ζ(α) = (T, a, µ) ∈ T implies that T = lst(α).
The idea is that a scheduler selects a transition among the ones available in T and it can base his decision on the history of the execution. The execution tree of M relative to the scheduler ζ, denoted by etree(M, ζ), is a fully probabilistic automaton M ′ = (St ′ , T init , Act, T ′ ) such that St ′ ⊆ exec * (M), and (α, a, µ ′ ) ∈ T ′ if and only if ζ(α) = (lst(α), a, µ) for some µ, and µ ′ (αaT ) = µ(T ). Intuitively, etree(M, ζ) is produced by unfolding the executions of M and resolving the nondeterminism using ζ.

In the following, given two executions α, α ′ , we write α ≤ α ′ to indicate that α is a prefix of α ′ . Given a fully probabilistic automaton M = (St, T init , Act, T ) we can define a probability space (Ω M , F M , p M ) on the space of executions of M as follows:

-Ω M ⊆ exec(M) is the set of maximal executions of M.

-If α is a finite execution of M we define the cone with prefix α as

C α = {α ′ ∈ Ω M |α ≤ α ′ }.
Let C M be the collection of all cones of M. Then F is the σ-field generated by C M (by closing under complement and countable union).

-We define the probability of a cone C α where α = T 0 a 1 T 1 . . . a n T n as

p(C α ) = n i=1 µ i (T i )
where µ i is the (unique because the automaton is fully probabilistic) measure such that (T i-1 , a i , µ i ) ∈ T . We define p M as the measure extending p to F (see [START_REF] Segala | Modeling and Verification of Randomized Distributed Real-Time Systems[END_REF] for more details about this construction).

CCS with internal probabilistic choice

We consider an extension of standard CCS ( [START_REF] Milner | Communication and Concurrency[END_REF])) obtained by adding internal probabilistic choice. The resulting calculus CCS p can be seen as a simplified version of the probabilistic π-calculus presented in [START_REF] Herescu | Probabilistic asynchronous π-calculus[END_REF][START_REF] Palamidessi | A randomized encoding of the π-calculus with mixed choice[END_REF] and it is similar to the one considered in [START_REF] Deng | Compositional reasoning for probabilistic finitestate behaviors[END_REF]. Like in those calculi, computations have both a probabilistic and a nondeterministic nature.

The main conceptual novelty is a distinction between observable and secret actions, introduced for the purpose of specifying information-hiding protocols.

We assume a countable set Act of actions a, and we assume that it is partitioned into a set Sec of secret actions s, a set Obs of observable actions o, and the silent action τ . For each s ∈ Sec we assume a complementary action s ∈ Sec such that s = s, and the same for Obs. The silent action τ does not have a complementary action, so the notation a will imply that a ∈ Sec or a ∈ Obs.

The syntax of CCS p is the following:

PROB • i p i T i τ -→ i p i δ(T i ) ACT j ∈ I I a i .T i a j -→ δ(T j ) PAR1 T 1 a -→ µ T 1 || T 2 a -→ µ || T 2 PAR2 T 2 a -→ µ T 1 || T 2 a -→ T 1 || µ REP T || ! T a -→ µ ! T a -→ µ || ! T COM T 1 a -→ δ(T ′ 1 ) T 2 a -→ δ(T ′ 2 ) T 1 || T 2 τ -→ δ(T ′ 1 || T ′ 2 ) RES T b -→ µ α = a, a (νa)T b -→ (νa)µ
Table 1. The semantics of CCS p .

T ::= process term

• i p i T i probabilistic choice | i s i .T i secret choice (s i ∈ Sec) | i r i .T i nondeterministic choice (r i ∈ Obs ∪ {τ }) | T || T parallel composition | (νa) T restriction | ! T replication
All the summations in the syntax are finite. We will use the notation T 1 ⊕ p T 2 to represent a binary probabilistic choice • i p i T i with p 1 = p and p 2 = 1p. Similarly we will use a 1 .T 1 a 2 .T 2 to represent a binary secret or nondeterministic choice. For the parallel operator we use the symbol " || " instead than the more standard " | " to avoid confusion with the notation for conditional probability.

The semantics of a given CCS p term is a probabilistic automaton whose states are process terms, whose initial state is the given term, and whose transitions T are those derivable from the rules in Table 1. We recall that we use the notation T a -→ µ stands for (T, a, µ) ∈ T . We denote by µ || T the measure µ ′ such that µ ′ (T ′ || T ) = µ(T ′ ) for all processes T ′ and µ ′ (T ′′ ) = 0 if T ′′ is not of the form T ′ || T , and similarly for T || µ. Furthermore we denote by (νa)µ the measure µ ′ such that µ ′ ((νa)T ) = µ(T ), and

µ ′ (T ′ ) = 0 if T ′ is not of the form (νa)T .
Note that in the produced probabilistic automaton, all transitions to non-Dirac measures are silent. Note also that a probabilistic term generates exactly one (probabilistic) transition.

A transition of the form T a -→ δ(T ′ ), i.e., a transition having for target a Dirac measure, corresponds to a transition of a non-probabilistic automaton (a standard labeled transition system). Thus, all the rules of CCS p specialize to the ones of CCS except from PROB. The latter models the internal probabilistic choice: a silent τ transition is available from the sum to a measure containing all of its operands, with the corresponding probabilities.

A secret choice i s i .T i produces the same transitions as the nondeterministic term i r i .T i , except for the labels. The distinction between the two kind of labels influences the notion of scheduler for CCS p : the secret actions are assumed to be inputs of the system. Namely we assume that the process receives in input a sequence of secret actions, and a secret action in the process can only be performed if it matches the next secret action in the input (this match "consumes" the input). Hence some choices are determined, or influenced, by the input. In particular, a secret choice with different guards is entirely decided by the input. The scheduler has to resolve only the residual nondeterminism which derives from the nondeterministic choices and from the interleavings.

In the following, we use the notation X ⇀ Y to represent the partial functions from X to Y , and α |Sec represents the projection of α on Sec.

Definition 3.1. Let T be a process in CCS p and M be the probabilistic automaton generated by T . A scheduler is a function

ζ : Sec * → exec * (M) ⇀ T such that: if (i) s = s 1 s 2 . . . s n and α |Sec = s 1 s 2 . . . s m with m ≤ n,

and

(ii) there exists a transition (lst(α), a, µ) such that either a ∈ Sec, or (a ∈ Sec and a = s m+1 ), then ζ(s)(α) is defined, and it is one of the transitions that satisfy (ii).

We will write ζ s (α) for ζ(s)(α).

Note that this definition of scheduler is different from the one used in probabilistic automaton, where the scheduler can decide to stop, even if a transition is allowed. Here the scheduler must proceed whenever a transition is allowed (provided that if it is labeled by a secret, that secret is the next one in the input string s). This view is in line with the standard operational semantics of CCS, where all enabled transitions are possible.

We now adapt the definition of execution tree from the notion found in probabilistic automata. In our case, the execution tree depends not only on the scheduler, but also on the input. Definition 3.2. Let M = (St, T, Act, T ) be the probabilistic automaton generated by a CCS p process T , where St is the set of processes reachable from T . Given an input s and a scheduler ζ, the execution tree of T for s and ζ, denoted by etree(T, s, ζ), is a fully probabilistic automaton M ′ = (St ′ , T, Act, T ′ ) such that St ′ ⊆ exec(M), and (α, a, µ ′ ) ∈ T ′ if and only if ζ s (α) = (lst(α), a, µ) for some µ, and µ ′ (αaT ) = µ(T ).

Note that we do not require the input s to be completely consumed during the execution. Typically, the execution consumes only the prefix of s which is to proceed at each step in which a secret action is involved.

Modeling protocols for information-hiding

In this section we propose an abstract model for information-hiding protocols, and we show how to represent this model in CCS p . An extended example is presented in Section 7.

Protocols as channels

We view protocols as channels in the information-theoretic sense [START_REF] Cover | Elements of Information Theory[END_REF]. The secret information that the protocol is trying to conceal constitutes the input of the channel, and the observables constitute the outputs. The set of the possible inputs and that of the possible outputs will be denoted by S and O respectively. We assume that S and O are of finite cardinality m and n respectively. We also assume a discrete probability distribution over the inputs, which we will denote by π = (π 1 , π 2 , . . . , π m ), where π i is the probability of the i-th element of S.

During the run, the protocol may use randomized operations to increase the level of uncertainty about the secrets and obfuscate the link with the observables. It may also have internal interactions between internal components, or other forms of nondeterministic behavior, but let us rule out this possibility for the moment, and consider a purely probabilistic protocol. We also assume there is exactly one output from each run of the protocol, and again, this is not a restrictive assumption because the elements of O can be structured data.

Given an input s, a run of the protocol will produce each o ∈ O with a certain probability p(o|s) which depends on s and on the randomized operations performed by the protocol. Note that p(o|s) depends only on the probability distributions on the mechanisms of the protocol, and not on the input distribution. The probabilities p(o|s), for s ∈ S and o ∈ O, constitute a m × n array M which is called the matrix of the channel, where the rows are indexed by the elements of S and the columns are indexed by the elements of O. We will use the notation (S, O, M ) to represent the channel.

Note that the input distribution π and the probabilities p(o|s) determine a distribution on the output. We will represent by p(o) the probability of o ∈ O. Thus both the input and the output can be considered random variables. We will denote these random variables by S and O.

If the protocol contains some form of nondeterminism, like internal components giving rise to different interleaving and interactions, then the behavior of the protocol, and in particular the output, will depend on the scheduling policy. We can reduce this case to previous (purely probabilistic) scenario by assuming a scheduler ζ which resolves the nondeterminism entirely. Of course, the conditional probabilities, and therefore the matrix, will depend on ζ, too. We will express this dependency by using the notation M ζ .

Process terms as channels

A given CCS p term T can be regarded as a protocol in which the input is constituted by sequences of secret actions, and the output by sequences of observable actions. We consider sequences as inputs instead than single actions, in order to be more general, and to account for the interactive nature of a process. Furthermore when the operational semantics of a process calculus is expressed in terms of a labeled transition system (and this is necessary in our context in order to achieve the compositionally results), it is customary to use sequences of labels to represent the input/output behavior. On the other hand, the standard notion of information-theoretic channel has only one input and one output, hence we need to regard the whole sequence of secret actions as one secret (the input of the channel), and analogously for the output.

We assume that only a finite set of finite sequences is relevant. This is certainly true if the term is terminating, which is usually the case in security protocols, as each session is supposed to terminate in finite time. For the sake of generality, we allow the element of S The following remark may be useful to understand the nature of the above definition: Remark 4.2. Given a sequence s = s 1 s 2 . . . s h , consider the term

T ′ = (νSec)(s 1 .s 2 . . . . .s h .0 || T ) Given a
(U ′ ))) if ζ s chooses (U, s j , δ(U ′ )).
Note that ζ ′ is a "standard" scheduler, i.e., it does not depend on an input sequence.

We have that each element p(o|s) in M ζ (T ) is equal to the probability of the set of all the maximal executions of T ′ , under ζ ′ , whose projection on Obs gives o.

Inferring the secrets from the observables

In this section we discuss possible methods by which an adversary can try to infer the secrets from the observables, and consider the corresponding probability of error, that is, the probability that the adversary draws the wrong conclusion. We regard the probability of error as a representative of the degree of protection provided by the protocol, and we study its properties with respect to the associated matrix.

We start by defining the notion of decision function, which represents the guess the adversary makes about the secrets, for each observable. This is a well-known concept, particularly in the field of hypothesis testing, where the purpose is to try to discover the valid hypothesis from the observed facts, knowing the probabilistic relation between the possible hypotheses and their consequences. In our scenario, the hypotheses are the secrets.

Definition 5.1. A decision function for a channel (S, O, M ) is any function f : O → S.

Given a channel (S, O, M ), an input distribution π, and a decision function f , the probability of error P(f, M, π) is the average probability of guessing the wrong hypothesis by using f , weighted on the probability of the observable (see for instance [START_REF] Cover | Elements of Information Theory[END_REF]). The probability that, given o, s is the wrong hypothesis is 1p(s|o) (with a slight abuse of notation, we use p(•|•) to represent also the probability of the input given the output). Hence we have: Definition 5.2. [START_REF] Cover | Elements of Information Theory[END_REF] The probability of error with respect to a decision function f is defined by

P(f, M, π) = 1 - O p(o)p(f (o)|o)
Given a channel (S, O, M ), the best decision function that the adversary can use, namely the one that minimizes the probability of error, is the one associated with the so-called MAP rule, which prescribes choosing the hypothesis s which has Maximum Aposteriori Probability (for a given o ∈ O), namely the s for which p(s|o) is maximum. The fact that the MAP rule represent the 'best bet' of the adversary is rather intuitive, and well known in the literature. We refer to [START_REF] Cover | Elements of Information Theory[END_REF] for a formal proof.

The MAP rule is used in the so-called Bayesian approach to hypothesis testing, and the corresponding probability of error is also known as Bayes risk. We will denote it by P MAP (M, π). The following characterization is an immediate consequence of Definition 5.2 and of the Bayes theorem p(s|o) = p(o|s)π s /p(o).

P MAP (M, π) = 1 - O max s (p(o|s)π s )
It is natural then to define the degree of protection associated with a process term as the infimum probability of error that we can obtain from this term under every compatible scheduler (in a given class).

In the following, we assume the class of schedulers A to be the set of all the schedulers compatible with the given input S.

It turns out that the infimum probability of error on A is achievable, i.e., it is actually a minimum. In order to prove this fact, let us first define a suitable metric on A.

Definition 5.3. Consider a CCS p process T , and let M be the probabilistic automaton generated by T . We define a distance d between schedulers in A as follows:

d(ζ, ζ ′ ) =    2 -m if m = min{|α| | α ∈ exec * (M) and ζ(α) = ζ ′ (α)} 0 if ζ(α) = ζ ′ (α) for all α ∈ exec * (M)
where |α| represents the length of α.

Note that M is finitely branching, both in the nondeterministic and in the probabilistic choices, in the sense that from every node T ′ there is only a finite number of transitions (T ′ , a, µ) and µ is a finite summation of the form µ = i p i δ(T i ). Hence we have the following (standard) result:

Proposition 5.4. (A, d) is a compact metric space, i.e., every sequence has a convergent subsequence (namely a subsequence with a limit in A).

We are now ready to show that there exists a scheduler that gives the minimum probability of error: Proposition 5.5. For every CCS p process T we have that there exists a minimizing

ζ m ∈ A such that inf ζ∈A P MAP (M ζ (T ), π) = P MAP (M ζm (T ), π) = min ζ∈A P MAP (M ζ (T ), π) Proof. By Proposition 5.4, (A, d) is compact. Furthermore, P MAP (M ζ (T ), π) is a con- tinuous function from (A, d) to ([0, 1], d ′ )
, where d ′ is the standard distance on real numbers. In fact, since S and O are finite sets of finite sequences, we have that for every T there exists a δ such that

d(ζ, ζ ′ ) < δ implies M ζ (T ) = M ζ ′ (T ). Consequently, ({P MAP (M ζ (T ), π) | ζ ∈ A}, d ′
) is also compact, and, since it represents a set of probabilities, it is bounded, too. The rest follows from the fact that compact and bounded subsets of reals are closed, and hence they contain their infima.

Thanks to previous proposition, we can define the degree of protection provided by a protocols in terms of the minimum probability of error.

Definition 5.6. Given a CCS p process T , the protection Pt MAP (T ) provided by T , in the Bayesian approach, is given by

Pt MAP (T, π) = min ζ∈A P MAP (M ζ (T ), π)
We conclude this section with some properties of P MAP . The next proposition shows that the probabilities of error are concave functions with respect to the space of matrices. Proposition 5.7. Consider a family of channels {(S, O, M i )} i∈I , and a family {c i } i∈I of convex coefficients, namely 0 ≤ c i ≤ 1 for all i ∈ I, and i∈I c i = 1. Then:

P MAP ( i∈I c i M i , π) ≥ i∈I c i P MAP (M i , π)
Proof. Consider ∀i ∈ I, M i = (p i (o|s)) s∈S,o∈O . Then:

P MAP ( i c i M i , π) = 1 -o max s ( i c i p i (o|s)π s ) ≥ 1 -o i c i max s (p i (o|s)π s ) = 1 -i o c i max s (p i (o|s)π s ) (since the summands are positive) = 1 -i c i o max s (p i (o|s)π s ) = i∈I c i -i∈I c i o∈O max s (p i (o|s)π s ) (since i∈I c i = 1) = i∈I c i (1 -o∈O max s (p i (o|s)π s )) = i∈I c i P MAP (M i , π)
Corollary 5.8. Consider a family of channels {(S, O, M i )} i∈I , and a family {c i } i∈I of convex coefficients. Then:

P MAP ( i∈I c i M i , π) ≥ min i∈I P MAP (M i , π)
The next proposition shows that if we transform the observables, and collapse the columns corresponding to observables which have become the same after the transformation, the probability of error does not decrease. Proposition 5.9. Consider a channel (S, O, M ), where M has conditional probabilities p(o|s), and a transformation of the observables f : O → O ′ . Let M ′ be the matrix whose conditional probabilities are p ′ (o ′ |s) = f (o)=o ′ p(o|s) and consider the new channel (S, O ′ , M ′ ). Then:

P MAP (M ′ , π) ≥ P MAP (M, π)
Proof. The result derives from:

o ′ ∈O ′ max s (p ′ (o ′ |s)π s ) = o ′ ∈O ′ max s ( f (o)=o ′ p(o|s)π s ) ≤ o ′ ∈O ′ f (o)=o ′ max s (p(o|s)π s ) = o∈O max s (p(o|s)π s )
The following propositions are from the literature. The condition p(s|o) = π s means that the observation does not give any additional information concerning the hypothesis. In other words, the a posteriori probability of s coincides with its a priori probability. The property p(s|o) = π s for all s ∈ S and o ∈ O was used as a definition of (strong) anonymity by Chaum [START_REF] Chaum | The dining cryptographers problem: Unconditional sender and recipient untraceability[END_REF]) and was called conditional anonymity by Halpern and O'Neill [START_REF] Halpern | Anonymity and information hiding in multiagent systems[END_REF].

Safe constructs

In this section we investigate constructs of the language CCS p which are safe with respect to the protection of the secrets.

We start by giving some conditions that will allow us to ensure the safety of the parallel and the restriction operators. The following theorem states our main results for Pt MAP . Note that they are also valid for Pt ML , because Pt ML (T ) = Pt MAP (T, π u ). In the following, given a function f : X → R for which an element x m exists such that f (x m ) = min x∈X f (x), we will denote such x m by minarg x∈X f (x) or alternatively by minarg X f (x).

Theorem 6.2. The probabilistic choice, the nondeterministic choice, and a restricted form of parallel composition are safe constructs, namely, for every input probability π, and any terms T 1 , T 2 , . . . , T h , we have

(1) Pt MAP ( ⊙ i p i T i , π) ≥ i p i Pt MAP (T i , π) ≥ min i Pt MAP (T i , π) (2) Pt MAP ( i o i .T i , π) = min i Pt MAP (T i , π) (3) Pt MAP ((ν o 1 , o 2 , . . . , o k ) (T 1 || T 2 )) ≥ Pt MAP (T 2 , π) if T 1 is safe outside o 1 , o 2 , . . . , o k . Proof. 1 By definition Pt MAP ( • i p i T i , π) = min ζ∈A P MAP (M ζ ( • i p i T i ), π). Let ζ m = minarg A P MAP (M ζ ( • i p i T i ), π). Hence Pt MAP ( ⊙ i p i T i , π) = P MAP (M ζm ( ⊙ i p i T i ), π)
Consider, for each i, the scheduler ζ mi defined as ζ m on the i-th branch, except for the removal of the first state and the first τ -step from the execution fragments in the domain. It's easy to see that

M ζm ( ⊙ i p i T i ) = i p i M ζmi (T i )
From Proposition 5.7 we derive

P MAP (M ζm ( ⊙ i p i T i ), π) ≥ i p i P MAP (M ζmi (T i ), π)
Finally, observe that ζ mi is still compatible with S, hence we have

P MAP (M ζmi (T i ), π) ≥ Pt MAP (T i , π) for all i which concludes the proof in this case. 2 Let ζ m = minarg A P MAP (M ζ ( i o i .T i ), π).
Let A i be the class of schedulers that choose the i-th branch at the beginning of the execution, and define

ζ ni = minarg Ai P MAP (M ζ ( i o i .T i ), π)
Obviously we have

Pt MAP ( i o i .T i , π) = min i P MAP (M ζni ( i o i .T i ), π)
P MAP (M ζni ( i o i .T i ), π) = P MAP (M ζmi (T i ), π) = Pt MAP (T i , π)
which concludes the proof of this case.

3 Let ζ m = minarg A P MAP (M ζ ((νo 1 , o 2 , . . . , o k ) (T 1 || T 2 )), π). Hence Pt MAP ((νo 1 , o 2 , . . . , o k ) (T 1 || T 2 ), π) = P MAP (M ζm ((νo 1 , o 2 , . . . , o k ) (T 1 || T 2 )), π)
The proof proceeds by constructing a set of series of schedulers whose limit with respect to the metric d in Definition 5.3 correspond to schedulers on the execution tree of T 2 . Consider a generic node in the execution tree of (νo

1 , o 2 , . . . , o k ) (T 1 || T 2 ) under ζ m , and let (νo 1 , o 2 , . . . , o k ) (T ′ 1 || T ′
2 ) be the new term in that node. Assume α to be the execution history up to that node. Let us consider separately the three possible kinds of transitions derivable from the operational semantics:

(a) (νo 1 , o 2 , . . . , o k ) (T ′ 1 || T ′ 2 ) a -→ (νo 1 , o 2 , . . . , o k ) (µ || T ′ 2 ) due to a transition T ′ 1 a -→ µ.
In this case a must be τ because of the assumption that T 1 does not contain secret actions and all its observable actions are included in {o 1 , o 2 , . . . , o k }. Assume that µ = i p i δ(T ′ 1i ). Then we have

(νo 1 , o 2 , . . . , o k ) (µ || T ′ 2 ) = i p i δ((νo 1 , o 2 , . . . , o k ) (T ′ 1i || T ′ 2 )).
Let us now consider the tree obtained by replacing the above distribution by δ((νo

1 , o 2 , . . . , o k ) (T ′ 1i || T ′ 2
)) (i.e., the tree obtained by pruning all alternatives except (νo

1 , o 2 , . . . , o k ) (T ′ 1i || T ′ 2 )
, and assigning to it probability 1). Let ζ mi be the projection of ζ m on the new tree (i.e., ζ mi is defined as the projection of ζ m on the histories

α ′ such that if α is a proper prefix of α ′ then ατ (νo 1 , o 2 , . . . , o k ) (T ′ 1i || T ′
2 ) is a prefix of α ′ ). We have

P MAP (M ζm ((νo 1 , o 2 , . . . , o k ) (T 1 || T 2 )), π) = P MAP ( i p i M ζmi ((νo 1 , o 2 , . . . , o k ) (T 1 || T 2 )), π)

≥

(by Proposition 5.7)

i p i P MAP (M ζmi ((νo 1 , o 2 , . . . , o k ) (T 1 || T 2 )), π)
In the execution tree of T 2 the above transition does not have a correspondent, but it obliges us to consider all different schedulers that are associated to the various ζ mi 's for different i's.

(b) (νo 1 , o 2 , . . . , o k ) (T ′ 1 || T ′ 2 ) a -→ (νo 1 , o 2 , . . . , o k ) (T ′ 1 || µ) due to a transition T ′ 2 a
-→ µ, with a not included in {o 1 , o 2 , . . . , o k }. In this case, the corresponding scheduler for T 2 must choose the same transition, i.e., T ′ 2 a -→ µ.

(c) (νo 1 , o 2 , . . . , o k ) (T ′ 1 || T ′ 2 ) τ -→ (νo 1 , o 2 , . . . , o k ) δ(T ′′ 1 || T ′′ 2 ) due to the transitions T ′ 1 a -→ δ(T ′′ 1 ) and T ′ 2 ā -→ δ(T ′′ 2 ).
In this case a must be an observable o because of the assumption that T 1 does not contain secret actions. The corresponding scheduler for T 2 must choose the transition

T ′ 2 ā -→ δ(T ′′ 2 ).
By considering the inequalities given by the transitions of type (a), we obtain sequences of schedulers of the form

{ζ m , ζ mi , ζ mij , ζ mijh , . . .}, which behave like ζ m until the node (νo 1 , o 2 , . . . , o k ) (T ′ 1 || T ′ 2 )
, and correspond to paths of increasing depth in the subtree of that node. Let p i , q j , r h . . . the probabilities of the branches selected by ζ mi , ζ mij , ζ mijh , . . . at each next choice point (which corresponds to a choice point with the same probability in the execution of T 2 ). We have:

P MAP (M ζm ((νo 1 , o 2 , . . . , o k ) (T 1 || T 2 )), π) ≥ i p i P MAP (M ζmi ((νo 1 , o 2 , . . . , o k ) (T 1 || T 2 )), π) ≥ i p i j q j P MAP (M ζmij ((νo 1 , o 2 , . . . , o k ) (T 1 || T 2 )), π) ≥ i p i j q j h r h P MAP (M ζ mijh ((νo 1 , o 2 , . . . , o k ) (T 1 || T 2 )), π) ≥ . . .
Observe now that for every i, j, h, . . . {ζ m , ζ mi , ζ mij , ζ mijh , . . .} is a converging series of schedulers whose limit ζ mijh... is isomorphic to a scheduler for T 2 , except that some of the observable transitions in T 2 may be removed due to the restriction on o 1 , o 2 , . . . , o k . This removal determines a (usually non injective) mapping f on the observables. Hence Proposition 5.9 applies, and we have:

P MAP (M ζm ((νo 1 , o 2 , . . . , o k ) (T 1 || T 2 )), π) ≥ i p i j q j h r h . . . P MAP (M ζ mijh... ((νo 1 , o 2 , . . . , o k ) (T 1 || T 2 )), π) ≥
(by Proposition 5.9)

i p i j q j h r h . . . P MAP (M ζ mijh... (T 2 ), π) ≥ i p i j q j h r h . . . min ζ∈A P MAP (M ζ (T 2 ), π)
Finally, observe that i p i = j q j = h r h = . . . = 1, hence

P MAP (M ζm ((νo 1 , o 2 , . . . , o k ) (T 1 || T 2 )), π) ≥ min ζ∈A P MAP (M ζ (T 2 ), π)
which concludes the proof.

Unfortunately the safety property does not hold for the secret choice. The following is a counterexample. Consider now T ′ = s 1 .T s 2 .T . Let us define a scheduler that, if the secret starts with s 1 selects o 1 , and if the secret starts with s 2 selects o 2 . We note that, under this scheduler, p(o

1 |s 1 s) = p(o 2 |s 2 s) = 1 while p(o 1 |s 2 s) = p(o 2 |s 1 s) = 0. Therefore Pt MAP (T ′ , π) = 1 -p 1 -p 2
where p 1 and p 2 are the maximum probabilities of the secrets of the form s 1 s and s 2 s, respectively. Note now that either max s π s = p 1 or max s π s = p 2 because of the assumption that S does not contain the empty sequence. Let π be such that both p 1 and p 2 are positive. Then 1

-p 1 -p 2 < 1 -max s π s , hence Pt MAP (T ′ , π) < Pt MAP (T, π).
The reason why we need the condition (i) in Definition 6.1 for the parallel operator is analogous to the case of secret choice. The following is a counterexample. Example 6.4. Let Sec and S be as in Example 6.3. Define T 1 = s 1 .0 s 2 .0 and

T 2 = o 1 .0 o 2 .0. Again, we have Pt MAP (T 2 , π) = 1 -max s π s .
Consider now the term T 1 || T 2 and define a scheduler that first executes an action s in T 1 and then, if s is s 1 , it selects o 1 , while if s is s 2 , it selects o 2 . The rest proceeds like in Example 6.3, where

T ′ = T 1 || T 2 and T = T 2.
The reason why we need the condition (ii) in Definition 6.1 is that without it the parallel operator may create different interleavings, thus increasing the possibility of an adversary discovering the secrets. The following is a counterexample. Example 6.5. Let Sec and S be as in Example 6.3. Define T 1 = o.0 and

T 2 = s 1 .(o 1 .0 ⊕ .5 o 2 .0) s 2 .(o 1 .0 ⊕ .5 o 2 .0). It is easy to see that Pt MAP (T 2 , π) = 1 -max s π s .
Consider the term T 1 || T 2 and define a scheduler that first executes an action s in T 2 and then, if s is s 1 , it selects first T 1 and then the continuation of T 2 , while if s is s 2 , it selects first the continuation of T 2 and then T 1 . Hence, under this scheduler, p(oo 1 |s 1 s) = p(oo 2 |s 1 s) = .5 and also p(o 1 o|s 2 s) = p(o 2 o|s 2 s) = .5 while p(oo 1 |s 2 s) = p(oo 2 |s 2 s) = 0 and p(o 1 o|s 1 s) = p(o 2 o|s 1 s) = 0. Therefore Pt MAP (T, π) = 1p 1p 2 where p 1 and p 2 are the maximum probabilities of the secrets of the form s 1 s and s 2 s, respectively. Following the same reasoning as in Example 6.3, we have that Pt MAP (T ′ , π) < Pt MAP (T, π).

A case study: the Dining Cryptographers

In this section we consider the Dining Cryptographers (DC) protocol proposed by Chaum [START_REF] Chaum | The dining cryptographers problem: Unconditional sender and recipient untraceability[END_REF], we show how to describe it in CCS p , and we apply the results of the previous section to obtain a generalization of Chaum's strong anonymity result.

In its most general formulation, the DC consists of a multigraph where one of the nodes (cryptographers) may be secretly designated to pay for the dinner. The cryptographers would like to find out whether there is a payer or not, but without either discovering the identity of the payer, nor revealing it to an external observer. The problem can be solved as follows: we put on each edge a probabilistic coin, with two possible, mutually exclusive results, 0 or 1. The coins are tossed, and each cryptographer computes the binary sum of all (the results of) the adjacent coins. Furthermore, it adds 1 if it is designated to be the payer. Finally, all the cryptographers declare their result.

It is easy to see that this protocol solves the problem of figuring out the existence of a

Crypt i = c i,i 1 (x 1 ) . . . . . c i,i k (x k ) . pay i (x) . di x 1 + . . . + x k + x Coin h = cℓ,h 0 . cr,h 0 .0 ⊕p h cℓ,h 1 . cr,h 1 .0 Collect = d 1 (y 1 ) . d 2 (y 2 ) . . . . . dn(yn) . out y 1 , y 2 , . . . , yn DC = (ν c)(ν d)( i Crypt i || h Coin h || Collect)
Table 2. The dining cryptographers protocol expressed in CCS p .

payer: the binary sum of all declarations is 1 if and only if there is a payer, because all the coins are counted twice, so their contribution to the total sum is 0.

The property we are interested in, however, is the anonymity of the system. Chaum proved that the DC is strongly anonymous if all the coins are fair, i.e., they give 0 and 1 with equal probability, and the multigraph is connected, namely there is a path between each pair of nodes. To state formally the property, let us denote by s the secret identity of the payer, and by o the collection of the declarations of the cryptographers.

Theorem 7.1. [START_REF] Chaum | The dining cryptographers problem: Unconditional sender and recipient untraceability[END_REF]) If the multigraph is connected, and the coins are fair, then DC is strongly anonymous, namely for every s and o, p(s|o) = p(s) holds.

We are now going to show how to express the DC in CCS p . We start by introducing a notation for value-passing in CCS p , following standard lines. The new notation is just syntactic sugar, in the sense that it is expressed in terms of the constructs of CCS p .

Input c(x).T

= v c v .T [v/x] Output c v = cv
The protocol, represented in Table 2, is defined as the parallel composition of the cryptographers processes Crypt i , of the coin processes Coin h , and of a process Collect whose purpose is to collect all the declarations of the cryptographers, and output them in the form of a tuple. The reason for using this process Collect is that in the original Chaum protocol all cryptographers are supposed to make their declaration at the same time. This is important because otherwise the schedule could reveal the identity of the payer by scheduling his declaration first, for example. However in CCS p concurrency is resolved by interleaving, and it is not possible to enforce the simultaneity of a set of actions (with he exception of a pair of complementary actions in a synchronisation step). Hence we need to simulate the simultaneous declarations by means of a single process (Collect) that collects the results into a tuple and then declares the tuple in a single step, and by internalizing the interleavings corresponding to the possible orders in which the results are transmitted by the cryptographers to Collect. Since these interleavings are internalized (i.e. they do not produce any observable action), their order does not matter: they are all equivalent (namely, invisible) from the point of view of the observer. In this protocol, the secret actions are pay i . All the others are observable actions.

Each coin communicates with two cryptographers. c i,h represents the communication channel between Coin h and Crypt i if h is indeed the index of a coin, otherwise it represents a communication channel "with the environment". We will call the latter external.

In the original definition of the DC there are no external channels, we have added them to prove a generalization of Chaum's result. They could be interpreted as a way for the environment to influence the computation of the cryptographers and hence test the system, for the purpose of discovering the secret.

We are now ready to state our generalization of Chaum's result:

Theorem 7.2. A DC is strongly anonymous if it has a spanning tree consisting of fair coins only.

Proof. Consider the term DC in Table 2. Remove all the coins that do not belong to the spanning tree, and the corresponding restriction operators. Let T be the process term obtained this way. Let A be the class of schedulers which select the value 0 for all the external channels. Since all the remaining coins are fair, this situation corresponds to the original formulation of Chaum and so we can apply Chaum's result (Theorem 7.1) and Proposition 5.11 to conclude that all the rows of the matrix M are the same and hence, by Proposition 5.10, P MAP (M, π) = 1max i π i .

Consider now one of the removed coins, h, and assume, without loss of generality, that c ℓ,h (x), c r,h (x) are the first actions in the definitions of Crypt ℓ and Crypt r . Consider the class of schedulers B that selects value 1 for x in these channels. The matrix M ′ that we obtain is isomorphic to M : the only difference is that each column o is now mapped to a column o + w, where w is a tuple that has 1 in the ℓ and r positions, and 0 in all other positions, and + represents the componentwise binary sum. Since this map is a bijection, we can apply Proposition 5.9 in both directions and derive that P MAP (M ′ , π) = 1max i π i .

By repeating the same reasoning on each of the removed coins, we can conclude that Pt MAP (T, π) = 1max i π i for any scheduler ζ of T .

Consider now the term T ′ obtained from T by adding back the coin h:

T ′ = (νc ℓ,h c r,h )(Coin h || T )
By applying Theorem 6.2 we can deduce that

Pt MAP (T ′ , π) ≥ Pt MAP (T, π)
By repeating this reasoning, we can add back all the coins, one by one, and obtain the original DC . Hence we can conclude that

Pt MAP (DC , π) ≥ Pt MAP (T, π) = 1 -max i π i
and, since 1max i π i is the maximum probability of error,

Pt MAP (DC , π) = 1 -max i π i
which concludes the proof.

Interestingly, also the other direction of Theorem 7.2 holds. We report this result for completeness, however we have proved it by using traditional methods, not by applying the compositional methods of Section 6.

Theorem 7.3. A DC is strongly anonymous only if it has a spanning tree consisting of fair coins only.

Proof. By contradiction. Let G be the multigraph associated to the DC and let n be the number of vertices in G. Assume that G does not have a spanning tree consisting only of fair coins. Then it is possible to split G in two non-empty subgraphs, G 1 and G 2 , such that all the edges between G 1 and G 2 are unfair. Let (c 1 , c 2 , . . . , c m ) be the vector of coins corresponding to these edges. Since G is connected, we have that m ≥ 1.

Let a 1 be a vertex in G 1 and a 2 be a vertex in G 2 . By our assumption of strong anonymity, for every observable o (which, we recall, is a vector of bits representing the declarations of the cryptographers) we have

p(o | a 1 ) = p(o | a 2 ) (1)
Here a 1 , resp. a 2 , represents the event that the cryptographer a 1 , resp. a 2 , is the payer. Observe now that, if w is a binary vector of dimension n containing 1 exactly twice, in correspondence of a 1 and a 2 , then p(o | a 1 ) = p(o + w | a 2 ), where o + w is the vector resulting from the component wise binary sum of o and w. This is because by adding 1 to their declarations, we invert the payer/non payer behavior of a 1 and a 2 . Thus by adding w to the declarations in the case in which a 2 is the payer (and a 1 is a non-payer) we obtain the same result as the case in which a 1 is the payer (and a 2 is a non-payer). Hence (1) becomes

p(o + w | a 2 ) = p(o | a 2 ) (2)
Let d be the binary sum of all the elements of o in G 1 , and d ′ be the binary sum of all the elements of o + w in G 1 . Since in G 1 w contains 1 exactly once, we have d ′ = d + 1. Hence (2), being valid for all o's, implies

p(d + 1 | a 2 ) = p(d | a 2 ) (3)
Because of the way o, and hence d, are calculated, and since the contribution of the edges internal to G 1 is 0, and a 2 (the payer) is not in G 1 , we have that

d = m i=1 c i
from which, together with (3), and the fact that the coins are independent from the choice of the payer, we derive

p( m i=1 c i = 0) = p( m i=1 c i = 1) = 1/2 (4)
The last step is to prove that p( m i=1 c i = 0) = 1/2 implies that one of the c i 's is fair, which will give us a contradiction. We prove this by induction on m. The property obviously holds for m = 1. Let us now assume that we have proved it for the vector (c 1 , c 2 , . . . , c m-1 ). Observe that p(

m i=1 c i = 0) = p( m-1 i=1 c i = 0)p(c m = 0) + p( m-1 i=1 c i = 1)p(c m = 1). From (4) we derive p( m-1 i=1 c i = 0)p(c m = 0) + p( m-1 i=1 c i = 1)p(c m = 1) = 1/2 (5)
Now, it is easy to see that (5) has only two solutions: one in which p(c m = 0) = 1/2, and one in which p( m-1 i=1 c i = 1) = 1/2. In the first case we are done, in the second case we apply the induction hypothesis.

Related work

In the field of information flow there have been various works [START_REF] Mclean | Security models and information flow[END_REF][START_REF] Gray | Toward a mathematical foundation for information flow security[END_REF][START_REF] Lowe | Quantifying information flow[END_REF][START_REF] Clark | Quantitative analysis of the leakage of confidential data[END_REF][START_REF] Clark | Quantified interference for a while language[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] Heusser | Applied quantitative information flow and statistical databases[END_REF][START_REF] Smith | On the foundations of quantitative information flow[END_REF], Andrés, Palamidessi, van Rossum & Smith 2010a[START_REF] Alvim | Information Flow in Interactive Systems[END_REF][START_REF] Boreale | Asymptotic information leakage under onetry attacks[END_REF] in which the high information and the low information are seen as the input and output respectively of a (noisy) channel. Information leakage is formalized in this setting as the channel mutual information or the channel capacity. The idea is that the leakage represents the difference between the a priori uncertainty about the (secret) high information, and the a posteriori uncertainty, after the low information has become pubblically known. The uncertainty is expressed in terms of entropy, and there are various alternative notions depending on the notion of attack that one wishes to model, as discussed in [START_REF] Köpf | An information-theoretic model for adaptive side-channel attacks[END_REF]. Most of the above approaches are based either on Shannon entropy or on the Rényi min entropy.

Channel capacity has been also used in relation to anonymity in (Moskowitz, Newman, Crepeau & Miller 2003b, Moskowitz, Newman & Syverson 2003a). These works propose a method to create covert communication by means of non-perfect anonymity.

A related line of work is [START_REF] Serjantov | Towards an information theoretic metric for anonymity[END_REF][START_REF] Díaz | Towards measuring anonymity[END_REF], where the main idea is to express the lack of (probabilistic) information in terms of entropy.

A different information-theoretic approach is taken in [START_REF] Clarkson | Belief in information flow[END_REF]. In this paper, the authors define information leakage as the difference between the a priori accuracy of the guess of the attacker, and the a posteriori one, after the attacker has made his observation. The accuracy of the guess is defined as the Kullback-Leibler distance between the belief (which is a weight attributed by the attacker to each input hypothesis) and the true distribution on the hypotheses. This approach, that was Shannon-based in [START_REF] Clarkson | Belief in information flow[END_REF], was later applied by Hamadou et al. [START_REF] Hamadou | Reconciling belief and vulnerability in information flow[END_REF]) also to the case of the Rényi min entropy.

The problem of preservation of information protection under program composition was considered also by [START_REF] Mciver | Compositional closure for bayes risk in probabilistic noninterference[END_REF]. In that paper, the author define an order on specifications based on Bayes Risk, and they identify a compositional subset of it: a refinement order ⊑ such that S ⊑ I implies C[S] C[I] for all contexts C. They also show that ⊑ is the compositional closure of , in the sense that S ⊑ I only when C[S] C[I] for some C. Finally, they prove that ⊑ is sound for other three, competing notions of elementary test and that therefore Bayes-Risk testing, with context, is maximally discriminating among them.

Desharnais et al. [START_REF] Desharnais | The metric analogue of weak bisimulation for probabilistic processes[END_REF]) defined a notion of metric between probabilistic processes and proved that the Shannon capacity associated to a protocol associated to a process is continuous with respect to this metric.

Deng et al. [START_REF] Deng | Measuring anonymity with relative entropy[END_REF]) consider a probabilistic calculus similar to CCS p , and define a relation between traces based on the Kullback-Leibler divergence. They show that certain constructs of their calculus preserve the relation, in the sense that they do not increase the divergence.

The analysis of quantitative information flow in concurrent programs has also been investigated in purely probabilistic (i.e. non information-theoretic) frameworks. For instance, [START_REF] Garcia | Probabilistic anonymity and admissible schedulers[END_REF] proposed to verify strong probabilistic anonymity by checking the sufficient condition that if two states differ only for the choice of the secret value, then the probabilistic automata rooted in those two states are isomorphic. This idea was further developed by [START_REF] Andrés | Information hiding in probabilistic concurrent systems[END_REF].

Conclusion, discussion, and future work

In this paper we have proposed to use the notion of Bayes risk to measure the degree of protection offered by an information-hiding protocol. We have investigated CCS p constructs that are safe, i.e., that are guaranteed not to decrease the protection. Then we have applied these results to strengthen a result of Chaum: the dining cryptographers are strongly anonymous if and only if they have a spanning tree of fair coins.

We recall that the Bayes risk represents the probability of error of an adversary who knows the exact prior probability distribution, and therefore he applies the MAP rule exactly. In case the adversary does not know the exact prior, he can still apply (an approximation of) the MAP rule of course, using for instance the uniform distribution, or his best bet, as the prior. Since the MAP rule is optimal, the probability of error in the approximate case is always greater than or equal to the Bayes risk. Hence the compositional method developed in this paper is still useful to compute a lower bound on the degree of protection.

One natural question is whether we could obtain a better (more precise) bound in the case we know for sure that the adversary is going to use a certain distribution as prior. Typically, if the adversary does not know anything about the prior distribution, he will use the uniform prior. This is equivalent to applying the so-called ML rule, which prescribes the choice of the s which has Maximum Likelihood (for a given o ∈ O), namely the s for which p(o|s) is maximum ‡ The corresponding probability of error P ML (M, π) can be characterised as follows (as an immediate consequence of Definition 5.2 and od the Bayes theorem). ‡ The name comes from the fact that p(o|s) is called the likelihood of s given o. However, the methods developed in this paper cannot be applied to compute a better lower bound for P ML (M, π), because Proposition 5.9, which is crucial for the compositionally results, does not hold for P ML (M, π). We leave the problem of developing a compositional method for computing the risk of ML-based attacks as a topic for future work.

Another problem that we would like to investigate in the future is the extension our results to other constructs of the language, and in particular to a more liberal type of parallel composition. This is not possible in the present setting, as the examples after Theorem 6.2 show. The problem is related to the scheduler: the standard notion of scheduler is too powerful and can leak secrets, by depending on the secret choices that have been made in the past. All the examples after Theorem 6.2 are based on this kind of problem. In [START_REF] Chatzikokolakis | Making random choices invisible to the scheduler[END_REF], we have studied the problem and we came out with a language-based solution to restrict the power of the scheduler. We are planning to investigate whether such approach could be exploited here to guarantee the safety of more constructs.

  (resp. O) to have different lengths. Thus S ⊆ fin Sec * and O ⊆ fin Obs * . Definition 4.1. Given a term T and a scheduler ζ : S → exec * (M) → T , the matrix M ζ (T ) associated with T under ζ is defined as the matrix such that, for each s ∈ S and o ∈ O, p(o|s) is the probability of the set of the maximal executions in etree(T, s, ζ) whose projection on Obs is o.

  scheduler ζ for T , let ζ ′ be the scheduler on T ′ that chooses the transition ((νSec)(s j .s j+1 . . . . .s h .0 || U ), r, (νSec)(s j .s j+1 . . . . .s h .0 || µ)) if ζ s chooses (U, r, µ), with (r ∈ Sec), and it chooses ((νSec)(s j .s j+1 . . . . .s h .0 || U ), τ, (νSec)(δ(s j+1 . . . . .s h .0 ||

Proposition 5 .

 5 10. (Chatzikokolakis, Palamidessi & Panangaden 2008a) Given S, O, let M be a matrix indexed on S, O such that all the rows of M are equal, namely p(o|s) = p(o|s ′ ) for all o ∈ O, s, s ′ ∈ S. Then, P MAP (M, π) = 1max s π s Furthermore P MAP (M, π) is the maximum probability of error, i.e., for every other matrix M ′ indexed on S, O we have: P MAP (M, π) ≥ P MAP (M ′ , π) Proposition 5.11. (Bhargava & Palamidessi 2005) Given a channel (S, O, M ), the rows of M are equal (and hence the probability of error is maximum) if and only if p(s|o) = π s for all s ∈ S, o ∈ O.

Definition 6. 1 .

 1 Consider process term T , and the observables o 1 , o 2 , . . . , o k such that (i) T does not contain any secret action, and (ii) the observable actions of T are included in o 1 , o 2 , . . . , o k . Then we say that T is safe outside o 1 , o 2 , . . . , o k .

  Example 6.3. Let Sec = {s 1 , s 2 } and assume that S does not contain the empty sequence. Let T = o 1 .0 o 2 .0. For all sequences s, s ′ ∈ S we have p(o 1 |s) = p(o 1 |s ′ ) and p(o 2 |s) = p(o 1 |s ′ ). Hence, by Proposition 5.10 we have Pt MAP (T, π) = 1max s π s .

P

  ML (M, π) = 1 -O p(o|s o ) π so where p(o|s o ) = max s (p(o|s)).

  Consider now, for each i, the scheduler ζ mi defined as as ζ ni , except for the removal of the first state and the first step from the execution fragments in the domain. Obviously ζ mi is still compatible with S, and the observables of T i are i one-to one correspondence with those of i o i .T i via the bijective function f i (o i o j1 . . . o j k ) = o j1 . . . o j k . Furthermore, all the probabilities of the channel M ζni ( i o i .T

i ) are the same as those of M ζmi (T i ) modulo the renaming of o into f (o). Hence we have

† There are other possible definitions of the a posteriori Rényi min entropy. Smith proposed to use this one because of its suitability for the information-hiding problem.

† This work has been partially supported by the project ANR-12-IS02-001 PACE, by the project ANR-11-IS02-0002 LOCALI, by the INRIA Equipe Associée PRINCESS, by the INRIA Large Scale Initiative CAPPRIS, and by EU grant agreement no. 295261 (MEALS). A preliminary version of this work appeared in the proc. of FOSSACS 2008.


Pierre-Yves Durand

Jacques Chanliau

Agnes Mariot

Michèle Kessler

Jean-Pierre Thomesse

Laurant Romary

François Charpillet

Robert Hervy

Telemedicine and Dialysis

Information found in the literature presents only marginal experiences concerning telemedicine in regards to peritoneal dialysis (PD). These experiences are limited to the transmission of data and/or images using new methods of communication. This article presents a new and innovative application of telemedicine in the field of PD and describes its characteristics in comparison to other telemedicine systems. In addition to optimizing the transmission of data via intra/internet, the DIATELIC (Interactive and Cooperative Monitoring of Dialysis Patients) system has an expert system designed to detect anomalies which can appear progressively and imperceptibly. This "intelligent" expert system uses six rules of interpretation simultaneously using basic initial data: Weight, blood pressure, differential blood pressure, orthostatic blood pressure, peritoneal ultrafiltration. These rules enable the system to give warning signs based on values which are pre-established or calculated using the averages of the previous 15 days. Routine use of this system operational now for over a year is conclusive. For the doctor, this system radically changes the way medical team followup on the patient. Daily access to the information concerning the patient resembles more a hospital-like setting and the integrated message service facilitates the contacts. For the patient, the sense of security derived from the expert system which notifies both the center and the patient in case of an anomaly is often mentioned. Telemedicine, which is in full development, will likely represent a major revolution for the public health system when the studies on the cost/benefit ratio reveal its utility.

Introduction and Definitions

Telemedicine, like many other emerging technologies, does not yet have any precise definition. The complexity of the communication systems, their rapid evolution, and the incessant technological innovations in the field of computers constantly open up new fields of applications for telemedicine. It is probably for this reason that the term telemedicine regroups, in fact, a multitude of applications as diverse as they are heterogeneous. Telemedicine is defined by the Anglo-Saxons as the use of an electronic communication network for the transmission of data and information concerning diagnosis or medical treatments. As such, a simple transmission of medical data by fax (lab reports, medical mail, etc.) or by telephone enters into this definition. However, in common language, telemedicine concerns a more recent technology such as the use of a numeric communication network, internet and/or the transmission of data by means other than speech (images, sounds, files, numeric data). From this point of view, the field of telemedicine remains vast and encompasses all medical specialties. Logically, it would be useful to classify the applications of telemedicine not in function of the type of data and their mode of transmission but rather in function of its potential users. This distinction is owed to the particular characteristics which they have in common and is independent of the medical specialty concerned.

-telemedicine between health-care professionals. In this case, the technical and economic imperatives are undoubtedly less important than the quality and integrity of the information transmitted. Indeed, the relatively low number of professionals and their theoretical capacity of mastering computer skills does not necessarily warrant inexpensive and simple material. However, the quality and quantity of the transmission become the priority for a precise and rapid long distance analysis. Telemedicine between professionals is developing rapidly and can be applied to a large variety of domains such as the visioconference, tele-training, hospital-home networks, tele-experts, tele-diagnosis, etc.

-public telemedicine concerns the direct transmission of medical data between the patient and the health-care professional. The heterogeneity of the population concerned and the large number of potential users require more moderately priced, user-friendly systems which are adapted for patients who have no experience and no particular aptitude for computers. This type of telemedicine is developing less rapidly probably because easy to use systems are often the corollary to complex technology. This type of telemedicine will probably represent a major revolution for the public health system in the near future on condition that the cost/benefit study shows an economic advantage. The "public" telemedicine will undoubtedly revolutionize the medical profession and the doctor/patient relationship which may cause a certain amount of apprehension and thus impede its development even further.

The treatment and the monitoring of these chronic patients represent a potential field of application particularly interesting for "public" telemedicine. The first systems mentioned in the literature describe essentially the passive transmission of data from the patient to the doctor allowing different medical parameters to be monitored without requiring any particular action from the patient. In the order of development of these techniques, these interactive systems probably represent the next step. It will undoubtedly be followed by the appearance of intelligent interactive systems; in other words, systems which integrate an automated analysis of the data transmitted.

We will present here one of the first interactive and intelligent public telemedicine systems applied to the treatment and monitoring of dialysis patients. This system, resulting from the collaboration between the CNRS (National Scientific Research Center), LORIA (Lorrain Reserch Laboratory of Computer Science and its Applications), and ALTIR (Lorrain Association for Renal Failure Treatments), was baptized DIATELIC.

Status of telemedicine for dialysis in 1999

1) The telemonitoring of dialysis machines.

Most dialysis methods (hemodialysis, hemofiltration, hemodiafiltration, automated peritoneal dialysis) require machines that are technologically evolved and which benefit from the latest technological innovations. With this in mind, the manufacturers of these machines currently used have anticipated the use of tele-transmissions by either incorporating a micro-chip, an integrated modem or a type RS232 output which enables the long distance recovery and transmission of information. Different tele-transmission systems are already operational (HEMODIAL™ by HOSPAL, GSS™ by GAMBRO, HomeChoice Pro™ by BAXTER) or on the verge of being operational (PD200™ by GAMBRO, SleepSafe™ by FRESENIUS). These systems allow the transmission of numeric data which are essentially technical (for hemodialysis, veinous and arterial blood pressure, ultrafiltration, other diverse characteristics of the hemodialysis session; for the automated peritoneal dialysis : number and characteristics of the cycles, ultrafiltration). The information is available in instantaneously or routinely through the intermediary of an integrated interface located in the computer of the medical center. Most of these systems are also able to transmit basic medical information (weight, arterial pressure, eventual incidents) through a specific interface located in the dialysis machine. These innovations in the field of telemedicine do, however, possess characteristics which limit their utility: -the systems developed by pharmaceutical laboratories are only compatible with dialysis machines from the same company. Even if the information transmitted is generally comparable, the interface and the transmission modes are different. Keeping in mind that medical centers rarely use machines that come exclusively from one pharmaceutical laboratory, this lack of compatibility of these systems is one of the reasons that their use remains limited.

-the technical nature of the data transmitted has undoubtedly a greater technical usefulness than a medical one. The maintenance of these machines, the long distance detection of breakdowns, and the technical security of the sessions could present a particularly interesting application of these systems, on condition that the technicians can familiarize themselves with all the interfaces made by the different manufacturers of the all machines they use.

-the transmission of information is passive. There is no possibility of interaction or dialogue with the patient with these systems. This limits their use for the medical monitoring of patients.

In summary, the "telemedicine" systems actually offered by laboratories implicated in the different dialysis techniques allow mainly the long distance transmission of technical data of the dialysis sessions. This lack of interaction with the patients places these systems more in the category of telemonitoring of machines.

2) Telemedicine for dialysis

There are only few telemedicine experiences with chronic renal failure patients and, in particular, with dialyzed patients. The experiences published are rare, experimental and limited. These studies do not include clinical results nor do they generally include cost/benefit evaluations. The first experiences were initiated in 1995 and published in 1998 [START_REF] Winchester | Hemodialysis and telemedicine: 2 years clinical experience[END_REF][START_REF] Winchester | Telemedicine in peritoneal dialysis: Study design and Implementation[END_REF][START_REF] Kubota | Telemedicine for CAPD: Patient management using the image transfer system[END_REF].

-A team in Washington D.C. [START_REF] Winchester | Hemodialysis and telemedicine: 2 years clinical experience[END_REF][START_REF] Winchester | Telemedicine in peritoneal dialysis: Study design and Implementation[END_REF] proposed an interactive telemedicine system. It consisted of placing an individual multimedia station in the home of each patient with two characteristics: a memory integrating a complete medical file (medical history, anamesis, physical and biological data, treatments, digitalized images (x-rays and others) and an on-line transmission of images and sounds. The images allow a private video-conference between the medical staff and the patient as well as the processing of more precise images (vascular access, exit site of the catheter, etc…) for a direct diagnosis. The sound is mostly used for cardio-pulmonary auscultation and sonar messages. This telemedicine system is thus interactive, polyvalent and has a potential field of application which is greater than that of dialysis. The first publication describing this system indicates a clinical study in progress which evaluates the quality of life of the patients, the morbidity, and the cost/benefit ratio.

-A team in Tokyo [START_REF] Kubota | Telemedicine for CAPD: Patient management using the image transfer system[END_REF] describes an interactive telemedicine system based exclusively on the transmission of images (Image Transfer System). The patients are equipped with cellular telephones and a portable computer on which is connected a numeric camera. The images are transmitted (duration: 4 min per image) to a server situated in the hospital and can be accessed by the doctors either directly or by their personal computers. The images are of good quality (1024 X 768 pixels; 16 700 000 colors) which permits a diagnosis on a portion of the body through a visual monitoring of the peritoneal dialysis treatment (color and aspect of the bags, inspection of the equipment). The Japanese study included 10 patients and emphasized the compactness of the equipment which facilitated the mobility of the patients.

-A team in Texas [START_REF] Moncrief | Telemedicine in PD patient care: Future possibilities[END_REF], historical pioneers in the field of telemedicine, have been using telemedicine for dialysis since 1992. Initially, they proposed a video-conference system linked to the telemonitoring system of the hemodialysis machines (Texas Telemedicine Project) by equipping the dialysis centers far from the medical team. Since 1997, they have been proposing to equip the patient with individual stations containing a rather complicated ensemble of electronic captors which permit a perfunctory consultation from a distance: stethoscope, opthomologic camera, fiber optic monitor, additional close camera. The entire station (cost: 34 000 USD) is connected through a numeric network to a server which is constantly monitored by a doctor.

The appearance in 1995 of a new dialysis technique, the daily home hemodialysis, opened up a new field of application for telemedicine for the individual, integrating simultaneously the telemonitoring of dialysis machines and the interaction with the patients. Until now, two experimental projects have been described:

-Pierratos [START_REF] Pierratos | Nocturnal hemodialysis: Three years of experience[END_REF] equipped his patients treated at home with a personal computer linked to a hemodialysis machine which transmitted the technical data to a server through the telephone network (modem). The medical team accessed this server through internet technology and can consult the data in real time or differed time since the data is stored by the server.

-Agroyannis [START_REF] Agroyannis | Telematics application for home hemodialysis[END_REF] described a project (Homer-D) financed by the European Community. He used the numeric network (ISDN) to establish a bi-directional communication between the doctor and the patient. A UNIX station with a multimedia PC located in the hospital is permanently accessible. Each patient is equipped at home with a multimedia terminal linked to a hemodialysis machine which permits the monitoring and long distance control of this machine. Additional captors permit an automatic monitoring of a patient during dialysis sessions: arterial tension, cardiac rate, electrocardiogram, and transcutaneous oxymetry. A preliminary study which involved two patients, four months, and 100 dialysis sessions will be enlarged to encompass three European centers and will probably include a cost/benefit evaluation.

These telemedicine studies described above involved the instantaneous transmission of a large amount of data, allowing for the long-distance monitoring of the patient and the equipment. However, all these systems depend upon a doctor to analyze the data in order to make a diagnosis. In other words, the transmission of data simply eliminates the geographic distance between the patient and the medical team.

The DIATELIC project

1) Objectives

The main objective of the DIATELIC project is to improve the quality of the CAPD treatment. Optimization of the treatment quality first requires three main telemedicine characteristics:

The prevention of disorders due to chronic or acute hydration (hyperhydration or deshydration). These anomalies often appear progressively and insidiously in patients treated by home PD. It can be responsible for incidents leading if not to death then, at the very least, to a poorly tolerated treatment in a semi-urgent context and which can undoubtedly contribute to the rate of morbidity. An improved long-distance relationship with the medical team. The telephone, invented in 1854 is still the only means of interactive communication between the dialysis patient at home and the medical team. Meanwhile, on the eve of the third millennium, the telephone has shown its limits in comparison to what actual technology can offer: the dialogues are subjective, the parameters transmitted are limited, the frequency of the calls is haphazard, and the availability of the medical staff is variable. These deficiencies in the quality as well as the quantity of the telephone calls can lead to problems with which the medical teams are familiar. Consequently, these problems often lead to the precipitated transportation to the center in order to establish a diagnosis and eventual hospitalization if the call was delayed.

A system which, through daily use, does not lead to a constraint which could underscore its benefits. This implies a quick and easy to use system. The patient interface should be sufficiently "universal" to be practical for all patients and quick enough to avoid any additional constraint on an already imposing treatment. The medical interface should permit the monitoring of a large number of patients without demanding a large amount of time from the medical team.

2) Description a) Principle

The DIATELIC system allows the transmission of medical data in real time, the analyses of the data, and the return of the raw data indiscriminately in the form of a representational graphic or an analysis of the data with an automated diagnosis. This second function answers the need for economy of time when monitoring a large number of patients by the same medical team. DIATELIC contains, then, an original expert system in several respects. DIATELIC uses the Markov model to calculate the probability for a patient to be in a Utilisez Word 6.0c (ou ult rieur) pour afficher une image Macintosh. predetermined hydration condition. Five conditions of have been established: normal hydration, hyperhydration, deshydration, dry-weight under-estimated and dry-weight overestimated. In order to calculate the probability of being in one of these five conditions, the system uses six complex rules simultaneously, and analyses simultaneously the absolute values of weight and blood pressure (differential and orthostatic) as well as their variations over the two previous days and taking, as points of reference, the averages of the previous fifteen days. So, for example, a patient with a permanent moderate systolic hypertension due to a cardiovascular disease will not be classified "hyperhydrated" if his state has been stable for at least fifteen days. Another example, a diabetic patient with a secondary orthostatic hypotension presenting a vegitative neuropathy will not be diagnosed as "deshydrated" if his condition is stable.

A warning message will automatically be sent to the patient as well as to the medical center as soon as the system detects a change in condition which could be a potential anomaly. In the case of a false alarm, the diagnosis of the expert system can easily be modified by the doctor and these corrections are taken into account in future diagnosis of the patient: the expert system is a self-learning. Finally, other rules have been introduced concerning the variations of ultrafiltration which are analyzed daily, exchange by exchange. An integrated email service, simple and easy to use, completes the system. This feature is frequently used by the patients. b) Functional description of the experimental system

The DIATELIC system is composed of three sub-systems. The first is a sub-system in the home of the patient, the second is a server which integrates the data base and the intelligent systems' detection of anomalies, and the third is a medical sub-system. These three subsystems are actually interconnected through several networks as shown in figure 1. The patient's terminal is connected to the server by a commuted telephone network. The server is connected to the Lorrain Reserch Laboratory of Computer Science and its Applications (LORIA); this is accessible through the local internet network (STANNET), permanently connected to the CHRU and ALTIR (Lorrain Association for Renal Failure Treatments) network. (Fig. 1).

Fig 1: Architecture of the experimental platform

Data confidentiality is preserved according to the recommendations of the CNIL: a password is required each time the server is accessed and the data is codified. Only the doctor is familiar with the patient's identification code. In addition, the connection on the patient's side is made through a call-back system with the server having in memory the telephone number of each patient. In the present system, the data entry is done manually by the patient who has already done this on paper. An exploitation in posteriori revealed that certain complications could have been avoided if the information had been transmitted earlier. The patient must get accustomed to entering the data into a computer and the transmission procedures. He can also take advantage of a graphic feed-back system showing the evolution of the data, which may contribute to his compliance. The clinical experience (technical test) has shown that the data entry does not present any great difficulty for the patient who, on the contrary, shows a certain enthusiasm and is reassured by the fact that the information he sends will be analyzed rapidly.

3) Advantages

DIATELIC, thanks to its expert system, analyzes the given information before transmitting them. In doing so it is undoubtedly a precursor of a new generation of telemedicine systems. This essential and original characteristic allows the sorting of information. Such a system is then applicable to a large number of patients monitored by a single doctor: routine consultations of the global data being reduced to those presenting anomalies. Other characteristics which distinguish the DIATELIC from other telemedicine systems currently used:

-an optimized doctor/patient interaction: the data is no longer passively gathered but is entered and transmitted by the patient himself. This interaction is reinforced by an integrated e-mail service which permits a bi-directional exchange of information. The patient now has an active role which reinforces his sense of responsibility with regards to the treatment and its adherence -a feedback directly to the patient of the analyzed data by the expert system. This security function stimulates and motivates the patient to adhere to his treatment and to use the patient interface.

-an expert system precisely adapted to the surveillance parameters of the dialysis technique for which it was developed (CAPD) for DIATELIC. This characteristic of the expert system allows a specialized monitoring and a detection of anomalies adapted to the CAPD.

-finally, the data transmitted is essentially medical and concerns the patient's health. DIATELIC is not a system of monitoring of machines or dialysis equipment. It can thus be used for all peritoneal dialysis patients, regardless of the material used.

Conclusion

Encouraged by the development of the communication network, the decrease in the cost of transmission, and the simplification of the computers, telemedicine will probably develop in the next few years and profoundly modify the medical profession. It will represent a major revolution in the public health system when the current studies undoubtedly reveal a favorable cost/benefit ratio. Concerning DIATELIC, such a study was started in may 1999. It is a propective, randomized study including at least 30 patients, in order to evaluate the quality of life, the mortality, the morbidity and the cost of the therapy between patients followed by telemedicine compared to patients without telemedicine. Preliminary results will be published in year 2000.