Romain Beauxis

Catuscia Palamidessi

Probabilistic and Nondeterministic Aspects of Anonymity

The concept of anonymity comes into play in a wide range of situations, varying from voting and anonymous donations to postings on bulletin boards and sending emails. The protocols for ensuring anonymity often use random mechanisms which can be described probabilistically, while the agents' behavior may be totally unpredictable, irregular, and hence expressible only nondeterministically. Formal definitions of the concept of anonymity have been investigated in the past either in a totally nondeterministic framework, or in a purely probabilistic one. In this paper, we investigate a notion of anonymity which combines both probability and nondeterminism, and which is suitable for describing the most general situation in which the protocol and the users can have both probabilistic and nondeterministic behavior. We also investigate the properties of the definition for the particular cases of purely nondeterministic users and purely probabilistic users. We formulate the notions of anonymity in terms of probabilistic automata, and we describe protocols and users as processes in the probabilistic π-calculus, whose semantics is again based on probabilistic automata. Throughout the paper, we illustrate our ideas by using the example of the dining cryptographers.

Introduction

The concept of anonymity comes into play in those cases in which we want to keep secret the identity of the agents participating in a certain event. There is a wide range of situations in which this property may be needed or desirable; for instance: voting, anonymous donations, and posting on bulletin boards.

Anonymity is often formulated in a more general way as an information-hiding property, namely the property that a part of information relative to a certain event is maintained secret. One should be careful, though, not to confuse anonymity with other properties that fit the same description, notably confidentiality (aka secrecy). Let us emphasize the difference between the two concepts with respect to sending messages: confidentiality refers to situations in which the content of the message is to be kept secret; in the case of anonymity, on the contrary, it is the identity of the originator, or of the recipient, that has to be kept secret. Analogously, in voting, anonymity means that the identity of the voter associated with each vote must be hidden, and not the vote itself or the candidate voted for. A discussion about the difference between anonymity and other information-hiding properties can be found in [START_REF] Halpern | Anonymity and information hiding in multiagent systems[END_REF].

An important characteristic of anonymity is that it is usually relative to the capabilities of the observer. In general the activity of a protocol can be observed by diverse kinds of observers, differing in the information they have access to. The anonymity property depends critically on what we consider as observables. For example, in the situation of an anonymous bulletin board, a posting by one member of the group is kept anonymous to the other members; however, it may be possible that the administrator of the board has access to some privileged information that may allow him to infer the member who posted it.

In general anonymity may be required for a subset of the agents only. In order to completely define anonymity for a protocol it is therefore necessary to specify which set(s) of members has to be kept anonymous. A further generalization is the concept of group anonymity: the members are divided into a number of sets, and it is revealed which one, among the groups, is responsible for an event, but the information as to which particular member has performed the event remains hidden. In this paper, however, we only consider the case of a single group of anonymous users.

Various formal definitions and frameworks for analyzing anonymity have been developed in literature. They can be classified into approaches based on process-calculi and transition systems [START_REF] Schneider | CSP and anonymity[END_REF][START_REF] Ryan | Modelling and Analysis of Security Protocols[END_REF], epistemic logic [START_REF] Syverson | Group principals and the formalization of anonymity[END_REF][START_REF] Halpern | Anonymity and information hiding in multiagent systems[END_REF], and "function views" [START_REF] Hughes | Information hiding, anonymity and privacy: a modular approach[END_REF]. In this paper, we focus on an approach based on a (probabilistic) process-calculus and on probabilistic automata.

The framework and techniques of process calculi have been used extensively in the area of security, to formally define security properties, and to verify cryptographic protocols. See, for instance, [START_REF] Abadi | A calculus for cryptographic protocols: The spi calculus[END_REF][START_REF] Lowe | Casper: A compiler for the analysis of security protocols[END_REF][START_REF] Roscoe | Modelling and verifying key-exchange protocols using CSP and FDR[END_REF][START_REF] Schneider | Security properties and CSP[END_REF][START_REF] Amadio | On the reachability problem in cryptographic protocols[END_REF]. The common denominator is that the various parties involved in the protocol are specified as concurrent processes and present typically a nondeterministic behavior. In [START_REF] Schneider | CSP and anonymity[END_REF][START_REF] Ryan | Modelling and Analysis of Security Protocols[END_REF], the nondeterminism plays a crucial role in the definition of the concept of anonymity, a definition which is based on the so-called "principle of confusion": a system is anonymous if the set of the possible observable outcomes is saturated with respect to the intended anonymous users. More precisely, if in one computation the culprit (the user who performs the action) is i and the observable outcome is o, then for every other agent j there must be a computation where j is the culprit and the observable is still o.

The principle of anonymity described above is elegant and general, however it is limited in that it does not cope with quantitative information. Now, many protocols for anonymity use random mechanisms, see, for example, Crowds [START_REF] Michael | Crowds: anonymity for Web transactions[END_REF], Onion Routing [START_REF] Syverson | Anonymous connections and onion routing[END_REF], and Freenet [START_REF] Clarke | Freenet: A distributed anonymous information storage and retrieval system[END_REF]. The probability distribution of these may be known or become known through statistical experiments. From this knowledge, and the observables, one may be able to differentiate the agents quantitatively, namely to deduce that one agent is more likely (has higher probability) to be the culprit than the others. This means that we do not have perfect anonymity. However the definition of the non-deterministic approach (in which of course the random mechanisms are approximated by nondeterministic mechanisms) may still be satisfied, as long as it is possible for each of the other agents to be the culprit, even with very low probability. In other words, the approach in [START_REF] Schneider | CSP and anonymity[END_REF][START_REF] Ryan | Modelling and Analysis of Security Protocols[END_REF], is based on the membership relation, and it is therefore only able to detect the difference between possible and impossible, not the quantitative differences.

Another advantage in taking into account probabilistic information is that it allows to classify various notions of anonymity according to their strength. See for instance the hierarchy proposed by Reiter and Rubin [START_REF] Michael | Crowds: anonymity for Web transactions[END_REF]. In this paper we explore a notion of anonymity which corresponds to the strongest one in [START_REF] Michael | Crowds: anonymity for Web transactions[END_REF], namely beyond suspicion 1 : from the observables all agents appear equally likely to be the culprit.

A probabilistic notion of anonymity was developed (as a part of a general epistemological approach) in [START_REF] Halpern | Anonymity and information hiding in multiagent systems[END_REF]. The approach there is purely probabilistic, in the sense that both the protocol and the users are assumed to act probabilistically. In particular the emphasis is on the probability of the users to be the culprit.

In this work, we take the opposite point of view, namely we assume that we may know nothing about the users. They may be totally unpredictable, and change attitude every time, so that the choice of being the culprit cannot be quantified probabilistically, not even by repeating statistical observations. Namely, it is a typical nondeterministic choice 2 . We regard this as a special case, though: In general, we assume that the behavior of the users may be in part probabilistic and in part nondeterministic. As for the protocol, it may use mechanisms like coin tossing, or random selection of a nearby node, which are supposed to exhibit a certain regularity and obey a probabilistic distribution. On the other hand, also the protocol can behave nondeterministically in part, due, for instance, to the (unpredictable) interleaving of the parallel components.

In summary, we investigate a notion of anonymity which combines both probability and nondeterminism, and which is suitable for describing the general situation in which both the users and the protocol can exhibit a combination of probabilistic and nondeterministic behavior. We also investigate the properties of the definition for the particular cases of purely nondeterministic users and purely probabilistic users.

One of the results of our investigation is that the property of anonymity does not depend on the probabilities of the users (cfr. Section 6.1). We consider this independence to be a fundamental property of a good notion of anonymity. In fact, a protocol for anonymity should be able to guarantee this property for every group of users, no matter what is their probability distribution for being the culprit.

In order to define the notion of probability we need, of course, a model of computation able to express both probabilistic and nondeterministic choices. This kind of systems is by now well established in literature, see for instance the probabilistic automata of [START_REF] Segala | Probabilistic simulations for probabilistic processes[END_REF], and has been provided with solid mathematical foundations and sophisticated tools for verification. For expressing the protocols, we will use the probabilistic asynchronous π-calculus introduced in [START_REF] Oltea | Probabilistic asynchronous π-calculus[END_REF][START_REF] Palamidessi | A randomized encoding of the π-calculus with mixed choice[END_REF], whose semantics is based on a model similar to [START_REF] Segala | Probabilistic simulations for probabilistic processes[END_REF]. Some of the results of this paper have appeared (without proofs) in [START_REF] Bhargava | Probabilistic anonymity[END_REF]. 1 To be more precise we should say that we think that it corresponds to the intended notion of beyond suspicion in [START_REF] Michael | Crowds: anonymity for Web transactions[END_REF]. We cannot prove this correspondence because the definition there is given only informally. 2 Some people consider nondeterministic choice as a probabilistic choice with unknown probabilities. Our opinion is that the two concepts are different: the notion of probability implies that we can gain knowledge of the distribution by repeating the experiment under the same conditions and by observing the frequency of the outcomes. In other words, from the past we can predict the future. This prediction element is absent from the notion of nondeterminism.

Plan of the paper

The paper is organized as follows: In Section 2 we recall the nondeterministic approach of [START_REF] Schneider | CSP and anonymity[END_REF][START_REF] Ryan | Modelling and Analysis of Security Protocols[END_REF] to the notion of anonymity. In Section 3 we recall the dining cryptographers' Problem by Chaum [START_REF] Chaum | The dining cryptographers problem: Unconditional sender and recipient untraceability[END_REF], which will serve as a running example throughout the paper, and we motivate the necessity of copying with probabilities. In Section 4 we briefly recall some basic notions about probabilistic automata and the probability of events (a more formal and detailed presentation can be found in Appendix A.2). In Section 5 we illustrate the notions and assumptions which are at the basis of our notion of anonymity.

In Section 6 we propose our notion of anonymity and we show some of its properties, notably the independence from the probability of the users. In Section 7 we consider the special case of purely nondeterministic users. In Section 8 we consider, on the contrary, purely probabilistic systems, and we prove that, under certain conditions, our definition corresponds to what in literature is known as conditional anonymity. In Section 11 we discuss other related work. Finally, in Section 12 we conclude.

The nondeterministic approach to anonymity

In this section we briefly recall the approach in [START_REF] Schneider | CSP and anonymity[END_REF][START_REF] Ryan | Modelling and Analysis of Security Protocols[END_REF]. In these works, the actions of a system S are classified into three sets (see Fig. 1):

-A: the actions whose performer is intended to remain anonymous for the observer, -B: the actions that are intended to be completely visible to the observer, -C: the actions that are intended to be hidden from the observer.

C A B S

Fig. 1. Classification of the actions in an anonymous system (cfr. [START_REF] Ryan | Modelling and Analysis of Security Protocols[END_REF]).

Typically the set A consists of actions of the form a(i), where a is a fixed "abstract" action (the same for all the elements of A), and i represents the identity of an anonymous user. Hence:

A = {a(i) | i ∈ I},
where I is the set of all the identities of the anonymous users.

Consider a dummy action d (different from all actions in S) and let f be the function on the actions of A B defined by f (α) = d if α ∈ A, and f (α) = α otherwise. Then S is said to be (strongly) anonymous on the actions in A if

f -1 (f (S\C)) ∼ T S\C,
where, following the CSP notation [START_REF] Hoare | Communicating Sequential Processes[END_REF], S\C is the system resulting from hiding C in S, f (S ′ ) is the system obtained from S ′ by applying the relabeling f to each (visible) action, f -1 is the relation inverse of f , and ∼ T represents trace equivalence 3 .

Intuitively, the above definition means that for any action sequence α ∈ A * , if an observable trace t containing α (not necessarily as a consecutive sequence) is a possible outcome of S\C, then, any trace t ′ obtained from t by replacing α with an arbitrary α ′ ∈ A * must also be a possible outcome of S\C.

We now illustrate the above definition on the example of the dining cryptographers.

The dining cryptographers' problem

This problem, described by Chaum in [START_REF] Chaum | The dining cryptographers problem: Unconditional sender and recipient untraceability[END_REF], involves a situation in which three cryptographers are dining together. At the end of the dinner, each of them is secretly informed by the master whether he should pay the bill or not. So, either the master will pay, or he will ask one of the cryptographers to pay. The cryptographers, or some external observer, would like to find out whether the payer is one of them or the master. However, if the payer is one of them, they also wish to maintain anonymity over the identity of the payer. Of course, we assume that the master himself will not reveal this information, and also we want the solution to be distributed, i.e. communication can be achieved only via message passing, and there is no central memory or central 'coordinator' which can be used to find out this information.

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

The dining cryptographers' problem will be a running example throughout the paper.

Nondeterministic dining cryptographers

In the approach of [START_REF] Schneider | CSP and anonymity[END_REF][START_REF] Ryan | Modelling and Analysis of Security Protocols[END_REF] the dining cryptographers are formalized as a purely nondeterministic system: the coins are approximated by nondeterministic coins, and the choice on who pays the bill is also nondeterministic. Chaum's protocol for the dining cryptographers [START_REF] Chaum | The dining cryptographers problem: Unconditional sender and recipient untraceability[END_REF][START_REF] Ryan | Modelling and Analysis of Security Protocols[END_REF].

The specification of the solution can be given in a process calculus style as illustrated below. In the original works [START_REF] Schneider | CSP and anonymity[END_REF][START_REF] Ryan | Modelling and Analysis of Security Protocols[END_REF] the authors used CSP [START_REF] Hoare | Communicating Sequential Processes[END_REF]. For the sake of uniformity here we use the π-calculus [START_REF] Milner | A calculus of mobile processes, I and II. Information and Computation[END_REF]. We recall that + ( ) is the nondeterministic sum and | (Π) is the parallel composition. 0 is the empty process. τ is the silent (or internal) action. cm and c(x) are, respectively, send and receive actions on channel c, where m is the message being transmitted and x is the formal parameter. ν is an operator that, in the π-calculus, has multiple purposes: it provides abstraction (hiding), enforces synchronization, and generates new names. For more details on the π-calculus and its semantics, we refer to Appendix A.1.

In the code below, ⊕ and ⊖ represent the sum and the subtraction modulo 3. Messages p and n sent by the master are the requests to pay or to not pay, respectively. pay i is the action of paying for cryptographer i.

We remark that we do not need all the expressive power of the π-calculus for this program. In particular, we do not need guarded choice (all the choices are internal because they start with τ ), and we do not need neither name-passing nor scope extrusion, thus ν is used just like the restriction operator of CCS [START_REF] Milner | Communication and Concurrency[END_REF].

Master = 2 i=0 τ . m i p . m i⊕1 n . m i⊕2 n . 0 + τ.m 0 n . m 1 n . m 2 n . 0 Crypt i = m i (x) . c i,i (y) . c i,i⊕1 (z) . if x = p then pay i . if y = z then out i disagree else out i agree else if y = z then out i agree else out i disagree Coin i = τ . Head i + τ . Tail i Head i = c i,i head . c i⊖1,i head . 0 Tail i = c i,i tail . c i⊖1,i tail . 0 Collect = out 0 (y 0 ) . out 1 (y 1 ) . out 2 (y 2 ) . outall y 0 , y 1 , y 2 DCP = (ν c)(ν m)(ν out )(Master | i Crypt i | h Coin h | Collect )
Let us consider the point of view of an external observer. The actions that are to be hidden (the set C) are the communications of the decision of the master and the results of the coins ( m, c). These are already hidden in the definition of the system DCP . The anonymous users are of course the cryptographers, and the anonymous actions (the set A) is constituted by the pay i actions, for i = 0, 1, 2. The observable actions (the set B) is constituted by those of the form outall x 0 , x 1 , x 2 with x i ∈ {agree, disagree}, for i = 0, 1, 2.

Let f be the function f (pay i ) = pay and f (α) = α for all the other actions. It is possible to check that f -1 (f (DCP ))) ∼ T DCP , where we recall that ∼ T stands for trace equivalence. Hence the nondeterministic notion of anonymity, as defined in Section 2, is satisfied.

Limitations of the nondeterministic approach

As a consequence of approximating the coins by nondeterministic coins, we cannot differentiate between a fair coin and a biased one. However, it is evident that the fairness of the coins is essential to ensure the anonymity property in the system, as illustrated by the following example.

Example 1. Assume that, whenever a cryptographer pays, an external observer obtains almost always one of the three outcomes represented in Fig. 3, where a stands for agree and d for disagree. More precisely, assume that these three outcomes appear with a frequency of 33% In the situation illustrated in the above example, clearly, the system does not provide anonymity. However the nondeterministic definition of anonymity is still satisfied (and it is satisfied in general, as long as "almost always" is not "always", i.e. the fourth configuration d, a, a also appears, from time to time). The problem is that the nondeterministic definition can only express whether or not it is possible to have a particular outcome, but cannot express whether one outcome is more likely than the other.

Probabilistic dining cryptographers

The probabilistic version of the protocol can be obtained from the nondeterministic one by attaching probabilities to the coins. We wish to remark that this is the essential change with respect to [START_REF] Schneider | CSP and anonymity[END_REF][START_REF] Ryan | Modelling and Analysis of Security Protocols[END_REF]: we faithfully model the random mechanisms of the protocol as probabilistic, rather than approximate them as nondeterministic.

Concerning the choices of the users (represented in this example as the choice of the master), those are in a sense independent from the protocol, and can be either nondeterministic, or probabilistic, or both.

We use the probabilistic π-calculus (π p ) introduced in [START_REF] Oltea | Probabilistic asynchronous π-calculus[END_REF][START_REF] Palamidessi | A randomized encoding of the π-calculus with mixed choice[END_REF]. The essential difference with respect to the π-calculus is the presence of a probabilistic choice operator of the form i p i α i .P i where the p i 's represents probabilities, i.e. they satisfy p i ∈ [0, 1] and i p i = 1, and the α i 's are non-output prefixes, i.e. either input or silent prefixes. (Actually, for the purpose of this paper, only silent prefixes are used.) The detailed presentation of this calculus is in Appendix A.2.

With respect to the program presented in Section 3.1, the definition of the Coin i 's must be modified as follows (p h and p t represent the probabilities of the outcomes of the coin tossing):

Coin i = p h τ . Head i + p t τ . Tail i
It is clear that the system obtained in this way combines probabilistic and nondeterministic behavior, not only because the master may be nondeterministic, but also because the various components of the system and their internal interactions can follow different scheduling policies, selected nondeterministically (although it can easily be seen that this latter form of nondeterminism is not relevant for this particular protocol).

Probabilistic automata

The models of computation combining probabilistic and nondeterministic behavior are by now well established in literature, see for instance the probabilistic automata of [START_REF] Segala | Probabilistic simulations for probabilistic processes[END_REF], and have been provided with solid mathematical foundations and tools for verification.

By unfolding a probabilistic automaton we obtain a computation tree, whose nodes, in general, offer both probabilistic and nondeterministic choices. In the probabilistic choices, the arcs are weighted with probabilities. The canonical way of defining the probabilistic notions relevant for our work is the following: First we solve the nondeterminism, i.e. we choose a function ς (called scheduler) which, for each nondeterministic choice in the computation tree, selects one of the possible alternatives. After pruning the tree from all the non-selected alternatives, we obtain a fully probabilistic tree. In such a tree, determined by ς, an execution (or run) is a maximal path, and an event is a (measurable) set of executions. In the finite case, we define the probability of an execution as the product of all the weights in its arcs, and the probability of an event e, p ς (e), as the sum of the probabilities of the executions in e. For the infinite case, and for more details about the above notions, we refer to Appendix A.2.

It should be clear, from the description above, that in general the probability of an event depends on the chosen scheduler. For example, in Fig. 4 the tree P represents a computation tree. From its root there is a nondeterministic choice between two transition groups (aka steps), which represent probabilistic choices. We adopt the convention of identifying a step by drawing a curve across its transitions. Analogously, there is a nondeterministic choice between two steps in the fourth node at the level immediately below the root. The trees Q, R and S represent the result of pruning P under different schedulers. Let us denote these schedulers by ς, ϑ and ϕ respectively. The probability of the event b, under each of these schedulers, is:

p ς (b) = 1/3 + 1/9 = 4/9, p ϑ (b) = 1/2, and p ϕ (b) = 0.

Our framework for probabilistic anonymity

In this section we illustrate the notions and assumptions which constitute the basis for our definition of probabilistic anonymity.

1/3 1/3 1/3 b 1/2 1/2 b 2/3 1/3 1/4 3/4 1/3 1/3 1/3 b b 2/3 1/3 b 1/2 1/2 1/4 3/4 1/2 1/2 b Q P S R
Fig. 4. A computation tree P and the fully probabilistic trees which derive from it under different schedulers. The irrelevant labels are omitted, and the probability is omitted when it is 1.

The system in which the anonymous users live and operate is modeled as a probabilistic automaton M [START_REF] Segala | Probabilistic simulations for probabilistic processes[END_REF], see Appendix A.2. Like in Section 2, we classify the actions of M into the three sets A, B and C, which are determined by the anonymous users, the specific kind of action on which we want anonymity, and the capabilities of the observer:

-The set of the anonymous actions:

A = {a(i) | i ∈ I}
where I is the set of the identities of the anonymous users and a is an injective functions from I to the set of actions which we call abstract action.

-The set of the visible actions, B. We will use b, b ′ , . . . to denote the elements of this set. -The set of the hidden actions C.

In the following we assume that the actions in C are already restricted in the system, so we do not need to mention them explicitly.

It should be remarked that the term "visible" here is relative: we assume that the observer can see only B and a, but, to the purpose of defining anonymity and checking whether a system is anonymous, we need to leave the actions a(i)'s visible (i.e. not restricted) as well.

Differently from [START_REF] Schneider | CSP and anonymity[END_REF][START_REF] Ryan | Modelling and Analysis of Security Protocols[END_REF], we do not assume that the observables are necessarily the traces of visible actions. A trace, indeed, contains not only the information on which actions have been executed, but also in what order they have been executed. Now, the observer may or may not be able to detect the order, and this is important because the order may give information on the culprit. Another reason for considering such abstraction is to make the analysis simpler. If we know, for instance, that the order of the visible actions does not give any information about the culprit (for instance because we know that the interleaving choices do not depend on the choice of the culprit) then we can forget about it.

In general, we abstract from the (visible) traces by assuming a partition O on them. The observables of the system are then the elements of this partition, denoted by o, o ′ , . . .. Note that each of them is a set of traces.

Another difference from [START_REF] Schneider | CSP and anonymity[END_REF][START_REF] Ryan | Modelling and Analysis of Security Protocols[END_REF] is that we consider the possibility that only certain schedulers are allowed. Thus, our notion of anonymity depends on the set of allowed schedulers, regarded as a parameter. One reason for this choice is to make more efficient the verification of the anonymity property. If we know, for instance, that the interleavings do not give any information about the culprit then we can fix one particular interleaving, thus reducing the number of schedulers to be taken into account. Definition 1. An anonymity system is a tuple (M, I, a, O, Z , p), where M is a probabilistic automaton, I is the set of anonymous users, a is the abstract anonymous action, O is a set of observables, Z is a set of schedulers for M , and for every ς ∈ Z , p ς is a probability measure on the event space generated by the execution tree of M under ς (denoted by etree(M, ς)), i.e. the σ-field generated by the cones in etree(M, ς) (cfr. Appendix A.2).

Note that, as expressed by the above definition, given a scheduler ς, an event is a set of executions in etree(M, ς). We introduce the following notation to represent the events of interest:

a(i) : all the executions in etree(M, ς) containing the action a(i) -a : all the executions in etree(M, ς) containing an action a(i) for an arbitrary i o : all the executions in etree(M, ς) containing an element of o.

We use the symbols ∪, ∩ and ¬ to represent the union, the intersection, and the complement of events, respectively. By definition of a, we have

a = i∈I a(i)
Furthermore, by definition of O, all the observables are pairwise disjoint:

∀ς ∈ Z . ∀o 1 , o 2 ∈ O. o 1 = o 2 ⇒ p ς (o 1 ∪ o 2 ) = p ς (o 1 ) + p ς (o 2 ) (1)
and they cover all possible traces:

∀ς ∈ Z . p ς ( o∈O o) = 1 (2)
In this paper we assume there is at most one culprit per run. In other words, we assume that all the a(i)'s are pairwise disjoint. This assumption is fundamental for the notion of anonymity we propose, and for the results we obtain.

Assumption 1 (At most one culprit)

∀ς ∈ Z . ∀i, j ∈ I. i = j ⇒ p ς (a(i) ∪ a(j)) = p ς (a(i)) + p ς (a(j))

Probabilistic anonymity for users with probabilistic and nondeterministic behavior

In this section we develop a notion of anonymity for the general case in which also the users, besides the protocol, combine probabilistic and nondeterministic behavior.

Example 2.

An example of such kind of behavior in the dining cryptographers is the following: assume the master may have a different attitude depending on the group of cryptographers that meet for dinner. Say that there are two groups, and which of them will meet for dinner is decided nondeterministically. The master will select the payer with probabilities p 0 , . . . , p 3 in the case of the first group, and q 0 , . . . , q 3 in the case of the second. Note that this situation may be quite common in practice: a certain protocol may be used by different groups of users, which may act probabilistically, but whose probability distribution may vary from one group to the other. Such a master can be represented in π p as follows:

Master = τ.Master 1 + τ.Master 2 Master 1 = 2 i=0 p i τ . m i p . m i⊕1 n . m i⊕2 n . 0 + p 3 τ.m 0 n . m 1 n . m 2 n . 0 Master 2 = 2 i=0 q i τ . m i p . m i⊕1 n . m i⊕2 n . 0 + q 3 τ.m 0 n . m 1 n . m 2 n . 0
Note that the choice in Master is nondeterministic while the choices in Master 1 and Master 2 are probabilistic.

The notion of anonymity must take into account the probabilities of the a(i)'s. When we observe a certain event o, the probability of o having been induced by a(i) must be the same as the probability of o having been induced by a(j) for any other j ∈ I. To formalize this notion, we need the concept of conditional probability. Recall that, given two events x and y with p(y) > 0, the conditional probability of x given y, denoted by p(x | y), is equal to the probability of x and y, divided by the probability of y:

p(x | y) = p(x ∩ y) p(y)
We are now ready to propose our notion of anonymity:

Definition 2 (Probabilistic anonymity for users with probabilistic and nondeterministic behavior). Example 3. Consider the system in Example 2. Assume that the coins are totally fair. For simplicity, let us fix the order of execution of the various components (interleaving) 4 , so that the only nondeterministic choice is the choice of the master. Hence we have Z = {ς, ϑ} where ς and ϑ selects Master 1 and Master 2 respectively. Assume now that Master 1 and Master 2 select as the payers i ∈ I with probability p i and j ∈ I with probability q j , respectively. The possible observable events, in both cases, are o 0 = a, a, d , o 1 = a, d, a , o 2 = d, a, a , and o 3 = d, d, d . These are the results in case one of the cryptographers is the payer. The case in which none of them is the payer gives the 4 configurations with an even number of d, which we will indicate by o 4 , . . . , o 7 . Consider now the possible outcomes of the coins. These are 8: h, h, h , h, h, t , . . . t, t, t . It is easy to see that, independently from which cryptographer is the payer, each of the above observables is produced by exactly two configurations. If the coins are fair, then, independently from the probability of the selected cryptographer, each observable o corresponds to a cone in the tree (rooted in the node immediately after the selection of the cryptographer) which has probabilistic measure 1/4 (cfr Fig. 5). Therefore

A system (M, I, a, O, Z , p) is anonymous if ∀ς, ϑ ∈ Z . ∀i, j ∈ I. ∀o ∈ O. (p ς (a(i)) > 0 ∧ p ϑ (a(j)) > 0) ⇒ p ς (o | a(i)) = p ϑ (o | a(j)) DCP Master 1 Master 2 o 0 o 1 o 2 o 3 o 3 p 3 o 3 o 0 p 0 o 0 o 1 o 1 o 1 o 1 p 2 o 2 o 2 o 2 o 2 o 2 o 0 o 0 o 0 o 1 o 5 o 4 o 3 o 3 o 3 p 1 q 0 q 1 q 2 q 3 o
p ς (o | a(i)) = 1/4 = p ϑ (o | a(j)). Hence Definition 2 is satisfied.
The behavior of a master which combines nondeterministic and probabilistic behavior can be much more complicated than the one illustrated above. However it is easy to see, by following the reasoning in the example above, that as long as the master does not influence the behavior of the coins, and these are fair, the conditional probability of each observable for a given payer is 1/4.

DCP

Proposition 1. Consider the dining cryptographers with arbitrary master (possibly combining nondeterminism and probability). If the coins are fair under every scheduler, then the system is probabilistically anonymous.

The proof of the above proposition is a straightforward generalization of the Example 3.

Example 4. Consider again the system in Example 2, but assume now that the coins are biased. Say, Coin 0 and Coin 1 give head with probability 9/10 and tail with probability 1/10, and vice-versa Coin 2 gives head with probability 1/10 and tail with probability 9/10. (This situation is analogous to that illustrated in Example 1.) Let us consider the observable o 0 = a, a, d . In case Crypt 1 is the payer, then the probability to get o 0 is equal to the probability that the result of the coins is h, h, t , plus the probability that the result of the coins is t, t, h , which is r = 9/10 * 9/10 * 9/10+1/10 * 1/10 * 1/10 = 730/1000. In case Crypt 2 is the payer, then the probability to get a, a, d is equal to the probability that the result of the coins is h, h, h , plus the probability that the result of the coins is t, t, t , which is s = 9/10 * 9/10 * 1/10 + 1/10 * 1/10 * 9/10 = 90/1000. It is easy to see that the same probability holds for the other cryptographers. Fig. 6 illustrates the situation. The observables o 1 , . . . , o 3 are as before, o 6 is a, d, d .

Hence, in the biased case, Definition 3 is not satisfied. And this is what we expect, because the system, intuitively, is not anonymous: when we observe a, a, d , Crypt 1 is much more likely to be the payer than any of the others.

Independence from the probability distribution of the users

One important property of Definition 2 is that it is independent from the probability distribution of the users. Intuitively, this is due to the fact that the condition of anonymity simply means that the cones for o rooted in the nodes that result from the (probabilistic and/or nondeterministic) selection of the culprit, have the same probabilistic measure, and this measure is independent from the probability of the culprit.

We consider this property fundamental for a good notion of anonymity: An anonymity protocol, in fact, should guarantee anonymity independently from (the attitude of) the users who use it, as long as they follow the protocol.

i)) = p ′ ς (o|a(i)), or equivalently p ς (o ∩ a(i)) p ς (a(i)) = p ′ ς (o ∩ a(i)) p ′ ς (a(i))
Assume that the choice of the a(j) ′ s is the first choice in etree(M, ς). If this is not the case, then we can transform the tree into one which satisfy this assumption, and in which the probability of events is the same. Fig. 7 shows the basic step of this transformation, in the case c is an anonymous action. In case c is an observable actions, then in the second tree c and the rightmost b must be switched in order to preserve the order in the trace (in case such order is observable). Let Ξ be the set of runs whose visible traces are of the form a

(i).b 1 .b 2 . . . . .b k for b 1 .b 2 . . . . .b k ∈ o. We have that p ς (o ∩ a(i)) = p ς (Ξ). Observe now that p ς (Ξ) = p ς (a(i))p ς (Ξ ′ )
, where Ξ ′ is the set of suffixes of the runs that start at the node resulting from the choice of a(i). Hence we have

p ς (o ∩ a(i)) = p ς (a(i))p ς (Ξ ′ ). Analogously, p ′ ς (o ∩ a(i)) = p ′ ς (a(i))p ′ ς (Ξ ′ ).
But, because of the hypothesis that p ς and p ′ ς only differ on the a(i) ′ s, we have p ς (Ξ ′ ) = p ′ ς (Ξ ′ ), which concludes the proof. ⊓ ⊔

Alternative characterization

We give here an alternative characterization of the notion of anonymity. The idea is that a system is anonymous if the probability, under a certain scheduler, of an observable o, given a(i), is the same as the probability of o given a under every other scheduler.

Proposition 2. A system (M, I, a, O, Z , p) is anonymous iff ∀ς, ϑ ∈ Z . ∀i ∈ I. ∀o ∈ O. (p ς (a(i)) > 0 ∧ p ϑ (a) > 0) ⇒ p ς (o | a(i)) = p ϑ (o | a)
Proof. If part) Let ς, ϑ ∈ Z and i, j ∈ I such that p ς (a(i)) > 0 and p ϑ (a(j)) > 0.

Since p ϑ (a(j)) > 0 implies p ϑ (a) > 0, by the hypothesis we have

p ς (o | a(i)) = p ϑ (o | a)
. Furthermore, by replacing in the hypothesis ς with ϑ and i with j we have

p ϑ (o | a(j)) = p ϑ (o | a).

Only if part)

Let ς, ϑ ∈ Z and i ∈ I such that p ς (a(i)) > 0 and p ϑ (a) > 0.

p ϑ (o ∩ a) = p ϑ (o ∩ j∈I a(j)) = p ϑ ( j∈I (o ∩ a(j))) = j∈I p ϑ (o ∩ a(j)) (by Assumption 1) = p ϑ (a(j))>0 p ϑ (o ∩ a(j)) = p ϑ (a(j))>0 p ϑ (o | a(j)) p ϑ (a(j)) = p ς (o | a(i)) p ϑ (a(j))>0 p ϑ (a(j)) (by Definition 2) = p ς (o | a(i)) p ϑ (a) Hence p ϑ (o | a) = p ϑ (o ∩ a)/p ϑ (a) = p ς (o | a(i)). ⊓ ⊔

Probabilistic Anonymity for nondeterministic users

The case in which the users are purely nondeterministic is characterized by the fact that each scheduler determines completely whether an action of the form a(i) takes place or not. Formally:

∀ς ∈ Z . ∀i ∈ I. p ς (a(i)) = 0 ∨ p ς (a(i)) = 1 (3)
In the case of nondeterministic users, the definition of anonymity simplifies as follows: Proposition 3. A system (M, I, a, O, Z , p) in which the choice of a(i)

(for i ∈ I) is nondeterministic in each run, is anonymous if ∀ς, ϑ ∈ Z . ∀o ∈ O. p ς (a) = p ϑ (a) = 1 ⇒ p ς (o) = p ϑ (o)
Proof. Immediate by instantiating Definition 2 to the case in which (3) holds, and by observing that, if p ς (a(i

)) = 1, then p ς (o | a(i)) = p ς (o).
⊓ ⊔

Probabilistic Anonymity for fully probabilistic systems

In this section we investigate how the removal of the nondeterminism influences our definition of anonymity. We consider therefore purely probabilistic systems. This will allow us also to compare our notion with other probabilistic proposals in literature.

Since the system is totally probabilistic, the probability measures do not depend on the choice of the scheduler. To be more precise, there is only one scheduler. So we can eliminate the component Z from the tuple and we can write p(x) instead of p ς (x). The definition of probabilistic anonymity given in previous section (cfr. Definition 2) simplifies into the following:

Definition 3. A fully probabilistic system (M, I, a, O, p) is anonymous if ∀i, j ∈ I. ∀o ∈ O. (p(a(i)) > 0 ∧ p(a(j)) > 0) ⇒ p(o | a(i)) = p(o | a(j))
Furthermore, the alternative characterization in Proposition 2 reduces to the following:

Proposition 4. A fully probabilistic system (M, I, a, O, p) is anonymous iff ∀i ∈ I. ∀o ∈ O. p(a(i)) > 0 ⇒ p(o | a(i)) = p(o | a)
In the fully probabilistic case there are two other notions of anonymity that seem rather natural. The first is based on the intuition that a system is anonymous if the observations do not change the probability of a(i). The probability of a(i) before the observation is called a priori probability; the probability of a(i) after the observation is called a posteriori probability. So the intuition is that a protocol does not leak information if these probabilities coincide. This is already known in literature as conditional anonymity (cfr. [START_REF] Halpern | Anonymity and information hiding in multiagent systems[END_REF]). It is interesting to point out the link with Information Theory: the condition means, indeed, that the entropy of the random variable associated to the culprit remains the same after the observation; i.e. the observation does not increase the information about the culprit.

The second notion is based on the (similar) idea that observing o rather than o ′ should not change our knowledge of the probability of a(i).

It is possible to prove that these two notions are equivalent. Furthermore, if we assume that the action a (i.e. the existence of a culprit) is totally visible to the observer, then we can prove that these notions are equivalent to ours. The condition "a is totally visible" means that every observable o indicates unambiguously whether a has taken place or not, i.e. it either implies a, or it implies ¬a. In other words this means that either o (as a set) is contained in a (as a set) or in the complement of a. Formally: Assumption 2 (The existence of a culprit is observable)

∀o ∈ O. p(o ∩ a) = p(o) ∨ p(o ∩ ¬a) = p(o)
We prove now our claims of equivalence. Proposition 5. Under Assumption 2, the following conditions are equivalent to each other and to our condition of anonymity.

(i) ∀i ∈ I. ∀o ∈ O. p(o ∩ a) > 0 ⇒ p(a(i) | o) = p(a(i))/p(a) (ii) ∀i ∈ I. ∀o, o ′ ∈ O. (p(o ∩ a) > 0 ∧ p(o ′ ∩ a) > 0) ⇒ p(a(i) | o) = p(a(i) | o ′ ).
Proof. We first show the equivalence of (i) and our condition of anonymity, using Proposition 4.

Assume (i) and p(a(i)

) > 0. If p(o ∩ a) = 0 then p(o | a(i)) = p(o | a) = 0. Otherwise, p(o | a(i)) = p(a(i) | o) p(o) p(a(i)) = p(a(i)) p(o) p(a) p(a(i)) (by (i)) = p(o) p(a) = p(o ∩ a) p(a) (by Assumption 2)) = p(o | a)
Viceversa, assume that the condition in Proposition 4 holds, and

p(o ∩ a) > 0. If p(a(i)) = 0, then p(a(i) | o) = p(a(i))/p(a) = 0. Otherwise we derive p(a(i) | o) = p(a(i))/p(a) from p(o | a(i)) = p(o | a)
, essentially reverting the above derivation.

As for the equivalence of (i) and (ii), we have: Proposition 5 is based on general properties of probabilistic spaces, independently from the particular setting (in our case, probabilistic automata) which we use to define the probabilities. Similar results have been presented in [START_REF] Grunwald | Updating probabilities[END_REF] and in [START_REF] Gill | Coarsening at random: Characterizations, conjectures and counterexamples[END_REF] (for the case in which a always occurs, i.e. p(a) = 1).

(i) ⇒ (ii)) Let i ∈ I,
p(a(i)) = p(a(i) ∩ o ′ ∈O o ′ ) (by (2)) = p( o ′ ∈O (a(i) ∩ o ′ )) = o ′ ∈O p(a(i) ∩ o ′ ) (by (1)) = p(o ′ ∩a)>0 p(a(i) ∩ o ′ ) = p(o ′ ∩a)>0 p(a(i) | o ′ ) p(o ′ ) = p(a(i) | o) p(o ′ ∩a)>0 p(o ′ ) (by (ii)) = p(a(i) | o) p(a) (by (
Since the notion of conditional anonymity (as well as the other notion in Proposition 5) is equivalent to ours, we have that also these notions are independent from the probability of the users. On the other hand, one has to keep in mind that the correspondence only holds under the Assumptions 1 (only one culprit) and 2 (the existence of a culprit is observable). Without Assumption 2 conditional anonymity is not independent from the probabilities of the users. Without Assumption 1 neither conditional anonymity nor our notion are independent.

Example 5. Fig. 8 shows an example in which Assumption 2 does not hold, and conditional anonymity depends on the probability of the users. In fact the first tree satisfies conditional anonymity, while the second does not. (They both satisfy our notion of anonymity.) Example 6. Fig. 9 shows an example in which Assumption 1 does not hold, and both conditional anonymity and our notion of anonymity depend on the probability of the users. In fact the first tree satisfies both kinds of anonymity, while the second does not.

Conditional anonymity and nondeterminism

It is not clear whether conditional anonymity [START_REF] Halpern | Anonymity and information hiding in multiagent systems[END_REF] can be generalized to the case of the users with nondeterministic behavior. The "naive" extensions obtained by introducing the scheduler in the formulae would not work. Let us consider the first characterization, i.e. conditional anonymity (for the other we would follow an analogous reasoning): One possible way of reintroducing the notion of scheduler is

∀i ∈ I. ∀o ∈ O. p(o ∩ a) > 0 ⇒ p(a(i) | o) = p(a(i))/p(a) a(2) a(1) 1/2 1/2 a(1) 1/2 1/2 1/2 1/2 a(2) a(1) 1/3 2/3 a(1) 2/3 1/3 1/2 1/2 1/2 o 1/2 o 1/2 o 1/2 o
∀ς, ϑ ∈ Z . ∀i ∈ I. ∀o ∈ O. (p ς (o ∩ a) > 0 ∧ p ϑ (a) > 0) ⇒ p ς (a(i) | o) = p ϑ (a(i))/p ϑ (a)
However this condition is too strong because it implies that p ϑ (a(i))/p ϑ (a) is the same for every ϑ, and this is clearly not the case for instance for the nondeterministic and probabilistic master specified in Section 2.

On the other hand, if we weaken the condition by identifying ς and ϑ:

∀ς ∈ Z . ∀i ∈ I. ∀o ∈ O. p ς (o ∩ a) > 0 ⇒ p ς (a(i) | o) = p ς (a(i))/p ς (a)
then the condition would be too weak to ensure anonymity, as shown by the following example:

Example 7. Consider a system in which the master influences the behavior of the coins somehow, in such a way that when Crypt i is chosen as the payer (say, purely nondeterministically, by ς i ) the result is always o 0 = d, a, a for i = 0, o 1 = a, d, a for i = 1, and o 2 = a, a, d for i = 2. Then we would have p ςi (o j ∩ a) > 0 only if j = i, and p ςi (a(i) | o i ) = 1 = p ςi (a(i))/p ςi (a). Hence the above condition would be satisfied, but the system is not be anonymous at all: whenever we observe d, a, a , for instance, we are sure that Crypt 0 is the payer.

Toward an automatic probabilistic checker

We have formulated the notion of anonymity in terms of observables for processes in the probabilistic π-calculus, whose semantics is based on the probabilistic automata of [START_REF] Segala | Probabilistic simulations for probabilistic processes[END_REF]. This opens the way to the automatic verification of the property.

It is worth noting that existing probabilistic model checkers, like PRISM, cannot be used directly to prove anonymity. In fact, PRISM computes only the infimum and the supremum of the probabilities of a given formula with respect to all possible schedulers. The anonymity property, on the contrary, requires computing the exact probability for each scheduler.

We are currently developing a model checker using the probabilistic π-calculus. In order to achieve this goal, several practical issues have to be fixed.

An automatic checker for our probabilistic notion of anonymity needs a full evaluation of the execution. This differs from the model checkers, where the process is checked against a single property. In our case, we want to collect all the various outcomes of the protocol and relate them to the inputs.

The natural language for an implementation is the asynchronous version of the πcalculus. In the asynchronous variant of the π-calculus, only internal (blind) choice is allowed and message sending is limited. The sending construct of the synchronous language, xy.P is replaced by an atomic sending process xy. In [START_REF] Beauxis | Formal approaches to information-hiding (tutorial)[END_REF], this limitation is shown to be equivalent to using an unordered buffered communication medium.

A process in the asynchronous π-calculus cannot natively send a message and wait until it is received to continue its execution. Encodings exist that mostly consist in an acknowledgment of the reception, much like for the TCP protocol.

For a majority of applications, the asynchronous π-calculus is the natural language for expressing a protocol or an algorithm, since most real-life communications and modern electronic networks use asynchronous communication mediums. For instance, the implementation of the the dining cryptographers proposed in this paper is purely asynchronous. However, asynchronous communications imply algorithmic limitations, such as for implementing a distributed consensus, as studied in [START_REF] Palamidessi | Comparing the expressive power of the synchronous and the asynchronous π-calculus[END_REF].

A naive evaluation of the probabilistic executions can be very inefficient. When communicating asynchronously, most communications happen without a particular order. This generates interleavings, where several sequence of actions can be observed in any order, but the overall result is the same. When evaluating this kind of executions, it is much more efficient to constrain the evaluation to only one of these possible interleavings. This leads to the definition of restricted executions that we call focused.

Such focused evaluations have been proved to maintain all relevant informations on the evaluated process. The may testing semantics is equivalent on focused and original executions. Furthermore, two bisimilar processes for the focused executions are bisimilar for the original executions. The implementation of such focused evaluator for the asynchronous π-calculus is currently under development.

Related work

The work [START_REF] Hughes | Information hiding, anonymity and privacy: a modular approach[END_REF] presents a modular framework to formalize a range of properties (including numerous flavors anonymity and privacy) of computer systems in which an observer has only partial information about system behavior, thereby combining the benefits of the knowledge-based approach (natural specification of information-hiding) and the algebra-based approach (natural specification of system behavior). It proposes the notion of function view to represent a mathematical abstraction of partial knowledge of a function. The logical formulae describing a property are characterized as opaqueness of certain function views, converted into predicates over observational equivalence classes, and verified, when possible, using the proof techniques of the chosen process formalism.

In [START_REF] Halpern | Anonymity and information hiding in multiagent systems[END_REF][START_REF] Syverson | Group principals and the formalization of anonymity[END_REF] epistemic logic is used to characterize a number of information-hiding requirements (including anonymity). In particular, [START_REF] Syverson | Group principals and the formalization of anonymity[END_REF] introduces the notion of a group principal and an associated model, language and logic to axiomatize anonymity. The main advantage of modal logic is that even fairly complex properties can be stated directly as formulae in the logic. On the other hand, [START_REF] Halpern | Anonymity and information hiding in multiagent systems[END_REF] uses a completely semantic approach and provides an appropriate semantic framework in which to consider anonymity. It also propose notions of probabilistic anonymity in a purely probabilistic framework. In particular, it propose a notion of conditional probability (cfr. Definition 4.4 in [START_REF] Halpern | Anonymity and information hiding in multiagent systems[END_REF]) which is similar to the first characterization in Proposition 5, if we interpret the formula ϕ in [START_REF] Halpern | Anonymity and information hiding in multiagent systems[END_REF] as the occurrence of the event a. Another notion defined in [START_REF] Halpern | Anonymity and information hiding in multiagent systems[END_REF] is that of (strong) Probabilistic Anonymity, which is expressed as the requirement that the a posteriory probabilities of two different anonymous events are the same under every observable, i.e.

∀i, j ∈ I. ∀o ∈ O. p(o) > 0 ⇒ p(a(i) | o) = p(a(j) | o)
This condition seems quite natural at a first sight; however a more careful analysis reveals that it is too strong. In [START_REF] Beauxis | Formal approaches to information-hiding (tutorial)[END_REF] it was indeed proved (see also Appendix A.3) that it is equivalent to our notion of anonymity (for fully probabilistic users) plus the condition that the a priori probabilities of two anonymous events are the same, namely: ∀i, j ∈ I. p(a(i)) = p(a(j)) So Probabilistic Anonymity in the sense of [START_REF] Halpern | Anonymity and information hiding in multiagent systems[END_REF] requires a uniform distribution on the anonymous events, which, in our opinion, is too much of a restriction for the users.

The first characterization in Proposition 5 was also implicitly used by Chaum in [START_REF] Chaum | The dining cryptographers problem: Unconditional sender and recipient untraceability[END_REF] (in which he considered a purely probabilistic system) as definition of anonymity. The factor p(a) is not present in the formula of Chaum, but that may be a typo, because in the informal explanation he gives, that factor is taken into account.

In literature there have been other works involving the use of variants of the πcalculus for formalizing protocols providing anonymity or similar properties. See for example [START_REF] Abadi | Private authentication[END_REF][START_REF] Kremer | Analysis of an electronic voting protocol in the applied pi-calculus[END_REF].

The research on the probabilistic foundations of anonymity (and more in general, information-hiding, and the related field of information flow) has recently evolved towards the use of Information Theory [START_REF] Díaz | Towards measuring anonymity[END_REF][START_REF] Serjantov | Towards an information theoretic metric for anonymity[END_REF][START_REF] Malacaria | Assessing security threats of looping constructs[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 Hypothesis Testing [START_REF] Chatzikokolakis | On the bayes risk in information-hiding protocols[END_REF][START_REF] Smith | On the foundations of quantitative information flow[END_REF]. The advantage in the use of these frameworks is that they allow to define quantitative degrees of anonymity. On the other hand, these framework are purely probabilistic, i.e. assume that the behavior of the user is probabilistic, and do not consider the existence of internal nondeterminism in the protocol.

With respect to the protocol's nondeterminism, our definition of anonymity is quite strict, because it requires that there is no leakage of information under any scheduler. But in the majority of cases, we can define a scheduler that follows a different policy depending on the choice of the anonymous event, thus leaking the information about the anonymous event. In the case of our example of the Dining Cryptographers we do not have such problem, but we would have it if the declarations of the cryptographers were observed as a sequence instead of a tuple. In fact, the scheduler could for instance always schedule the declaration of the payer at last, thus revealing entirely who the payer is. The problem of the scheduler in security, and a proposal for its solution, are discussed in [START_REF] Chatzikokolakis | Making random choices invisible to the scheduler[END_REF] and [START_REF] Chatzikokolakis | Bisimulation for demonic schedulers[END_REF].

Conclusion and future work

We have proposed a notion of anonymity based on a model which combines probability and nondeterminism, and we have shown that under certain assumptions it can be regarded as a generalization of conditional anonymity [START_REF] Halpern | Anonymity and information hiding in multiagent systems[END_REF].

We have formulated the notion of anonymity in terms of observables for processes in the probabilistic π-calculus, whose semantics is based on the probabilistic automata of [START_REF] Segala | Probabilistic simulations for probabilistic processes[END_REF]. This opens the way to the automatic verification of the property. We are currently developing a model checker for the probabilistic π-calculus.

The rules for the early semantics are given in Table 1. The symbol ≡ used in Rule CONG stands for structural congruence, a form of equivalence which identifies "statically" two processes. Again, there are several definition of this relation in literature. For our purposes we do not need a very rich notion, we will just use it to simplify the presentation. Hence we only assume this congruence to satisfy the following:

(i) P ≡ Q if Q can be obtained from P by alpha-renaming, notation P ≡ α Q, (ii) P |Q ≡ Q|P , (iii) (P |Q)|R ≡ P |(Q|R), (iv) (νxP )|Q ≡ νx(P |Q) if x ∈ fv (Q), (v) ! P ≡ P | ! P , (vi) [x = x] P ≡ P , (vii) [x = y] P ≡ P , if x is syntactically different from y.

A.2 The probabilistic π-calculus

In this section we recall the definition of the probabilistic π-calculus, π p , which was introduced in [START_REF] Oltea | Probabilistic asynchronous π-calculus[END_REF]. This calculus was used in [START_REF] Palamidessi | A randomized encoding of the π-calculus with mixed choice[END_REF] to express various randomized algorithms, notably the distributed implementation of the π-calculus with mixed choice. In this paper, we are going to use it as a formalism to express systems of probabilistic anonymous agents.

Probabilistic automata

The π p -calculus is based on the model of probabilistic automata of Segala and Lynch [START_REF] Segala | Probabilistic simulations for probabilistic processes[END_REF], which are able to express both probabilistic and nondeterministic behaviors.

A discrete probabilistic space is a pair (X, p) where X is a finite or countable set and p is a function p : X → (0, 1] such that x∈X p(x) = 1. Given a set Y , we define the sets of all probabilistic spaces on Y as

Prob(Y ) = {(X, p) | X ⊆ Y and (X, p) is a discrete probabilistic space }.
Given a set of states S and a set of actions A, a probabilistic automaton on S and A is a triple (S, T , s 0 ) where s 0 ∈ S (initial state) and T ⊆ S × Prob(A × S). We call the elements of T transition groups (in [START_REF] Segala | Probabilistic simulations for probabilistic processes[END_REF] they are called steps). The idea behind this model is that the choice between two different groups is made nondeterministically and possibly controlled by an external agent, e.g. a scheduler, while the transition within the same group is chosen probabilistically and it is controlled internally (e.g. by a probabilistic choice operator). An automaton in which there is at most one transition group for each state is called fully probabilistic.

We define now the notion of execution of an automaton under a scheduler, by adapting and simplifying the corresponding notion given in [START_REF] Segala | Probabilistic simulations for probabilistic processes[END_REF]. A scheduler can be seen as a function that solves the nondeterminism of the automaton by selecting, at each moment of the computation, a transition group among all the ones allowed in the present state. Schedulers are sometimes called adversaries, thus conveying the idea of an external I-SUM

P i αi.Pi x(z) -→ Pj[z/y] αj = x(y) O/τ -SUM P i αi.Pi α j -→ Pj αj = xy or αj = τ OPEN P xy -→ P ′ νyP x(y) -→ P ′ x = y RES P µ -→ P ′ νyP µ -→ νyP ′ y ∈ n(µ) PAR P µ -→ P ′ P |Q µ -→ P ′ |Q bn(µ) ∩ fn(Q) = ∅ COM P x(y) -→ P ′ Q xy -→ Q ′ P |Q τ -→ P ′ |Q ′ CLOSE P x(y) -→ P ′ Q x(y) -→ Q ′ P |Q τ -→ νy(P ′ |Q ′ ) CONG P ≡ P ′ P ′ µ -→ Q ′ Q ′ ≡ Q P µ -→ Q Table 1.
The transition system of the π-calculus.

entity playing "against" the process. For the purpose of this paper, however, we stick to the term "scheduler" in order to avoid confusion with the notion of adversary used in security. We will assume that a scheduler can decide the next transition group depending not only on the current state, but also on the whole history of the computation till that moment, including the random choices made by the automaton. Given a probabilistic automaton M = (S, T , s 0 ), define tree(M ) as the tree obtained by unfolding the transition system, i.e. the tree with a root n 0 labeled by s 0 , and such that, for each node n, if s ∈ S is the label of n, then for each (s, (X, p)) ∈ T , and for each (µ, s ′ ) ∈ X, there is a node n ′ child of n labeled by s ′ , and the arc from n to n ′ is labeled by µ and p(µ, s ′ ). We will denote by nodes(M ) the set of nodes in tree(M ), and by state(n) the state labeling a node n.

A scheduler for M is a function ς that associates to each node n of tree(M ) a transition group among those which are allowed in state(n). More formally, ς : nodes(M ) → Prob(A × S) such that ς(n) = (X, p) implies (state(n), (X, p)) ∈ T .

The execution tree of an automaton M = (S, T , s 0 ) under a scheduler ς, denoted by etree(M, ς), is the tree obtained from tree(M ) by pruning all the arcs corresponding to transitions which are not in the group selected by ς. More formally, etree(M, ς) is a fully probabilistic automaton (S ′ , T ′ , n 0 ), where S ′ ⊆ nodes(M ), n 0 is the root of tree(M ), and (n, (X ′ , p ′ )) ∈ T ′ iff X ′ = {(µ, n ′ ) | (µ, state(n ′ )) ∈ X and n ′ is a child of n in tree(M )} and p ′ (µ, n ′ ) = p(µ, state(n ′ )), where (X, p) = ς(n). If (n, (X ′ , p ′ )) ∈ T ′ , (µ, n ′ ) ∈ X ′ , and p ′ (µ, n ′ ) = p, we will use sometime the notation n . . ., the probability of ξ is defined as p(ξ) = i p i . If ξ is maximal, then it is called execution. We denote by exec(M, ς) the set of all executions in etree(M, ς).

We define now a probability on certain sets of executions, following a standard construction of Measure Theory. Given an execution fragment ξ, let C ξ = {ξ ′ ∈ exec(M, ς) | ξ ≤ ξ ′ } (cone with prefix ξ). Define p(C ξ ) = p(ξ). Let {C i } i∈I be a countable set of disjoint cones (i.e. I is countable, and ∀i, j. i = j ⇒ C i ∩ C j = ∅). Then define p( i∈I C i ) = i∈I p(C i ). Two countable sets of disjoint cones with the same union produce the same result for p, so p is well defined. Further, we define the probability of an empty set of executions as 0, and the probability of the complement of a certain set of executions, with respect to the all executions as the complement with respect to 1 of the probability of the set. The closure of the cones (plus the empty set) under countable unions and complementation generates what in Measure Theory is known as a σ-field. Syntax and transition system of the π p -calculus We will now illustrate the π pcalculus. Syntactically, the only difference with respect to the π-calculus is that we do not have the free choice (or mixed guarded choice depending on the presentation), and we have instead the output prefix xy.P and the following probabilistic non-output choice operator i p i α i .P i where the p i 's represents positive probabilities, i.e. they satisfy p i ∈ (0, 1] and i p i = 1, and the α i 's are non-output prefixes, i.e. either input or silent prefixes.

Note that the nondeterministic blind choice τ.P + τ.Q can be obtained in this calculus by using the parallel operator: it is in fact equivalent to (νx)(x x.P x.Q).

In order to give the formal definition of the probabilistic model for π p , it is convenient to introduce the following notation: given a probabilistic automaton (S, T , s 0 ) and s ∈ S, we write s { The operational semantics of a π p process P is a probabilistic automaton whose states are the processes reachable from P and the T relation is defined by the rules in Table 2.

The following is an informal explanation of the rules in Table 2.

SUM: This rule models the behavior of a choice process: each transition corresponds to the possible execution of an enabled guard α i and the consequent commitment to the branch P i . Note that all possible transitions belong to the same group, meaning that the transition is chosen probabilistically by the process itself. OUT: This rule expresses the fact that an output prefix process α.P simply performs the action, and then continues with P . RES: This rule models restriction on channel y: only the actions on channels different from y can be performed and possibly synchronize with an external process. The probability is redistributed among these actions. OPEN: This rule works in combination with CLOSE by signaling that the send action labeling the transition is on a name which is private to the sender. PAR: This rule represents the interleaving of parallel processes. All the transitions of the processes involved are made possible, and they are kept separated in the original groups. In this way we model the fact that the selection of the process for the next computation step is determined by a scheduler. In fact, choosing a group corresponds to choosing a process. COM: This rule models communication by handshaking. The output action synchronizes with all matching input actions of a partner, with the same probability of the input action. The other possible transitions of the partner are kept with the original probability as well. Note that the side condition ensure that all matching inputs are considered. Thanks to alpha-conversion, we can always rewrite a process so that this condition is met.

  Fig. 2.Chaum's protocol for the dining cryptographers[START_REF] Chaum | The dining cryptographers problem: Unconditional sender and recipient untraceability[END_REF][START_REF] Ryan | Modelling and Analysis of Security Protocols[END_REF].

Fig. 3 .

 3 Fig. 3. Illustration of Example 1: the results that are observed with high frequency.

Fig. 5 .

 5 Fig. 5. Illustration of Example 3.

Fig. 6 .

 6 Fig. 6. Illustration of Example 4.

Theorem 1 .

 1 If (M, I, a, O, Z, p) is anonymous then for any p ′ which differs from p only on the a(i)'s, (M, I, a, O, Z, p ′ ) is anonymous. Proof. Assume that (M, I, a, O, Z, p) is anonymous. Consider a scheduler ς ∈ Z. It is sufficient to show that for every o ∈ O and every i ∈ I, p ς (o|a(

Fig. 7 .

 7 Fig. 7. Basic transformation step for the proof of Theorem 1.

  and o, o ′ ∈ O such that p(o ∩ a) > 0 and p(o ′ ∩ a) > 0. By (i) we have p(a(i) | o) = p(a(i))/p(a) = p(a(i) | o ′ ).(ii) ⇒ (i)) Let i ∈ I and o ∈ O such that p(o ∩ a) > 0. We have

Fig. 8 .

 8 Fig. 8. Illustration of Example 5.

Fig. 9 .

 9 Fig. 9. Illustration of Example 6.

  execution fragment ξ is any path (finite or infinite) from the root of etree(M, ς). The notation ξ ≤ ξ ′ means that ξ is a prefix of ξ ′ . If ξ is n 0

  i ∈ I} iff (s, ({(µ i , s i ) | i ∈ I}, p)) ∈ T and ∀i ∈ I p i = p(µ i , s i ),where I is an index set. When I is not relevant, we will use the simpler notation s { µi -→ pi s i } i . We will also use the notation s { µi -→ pi s i } i:φ(i) , where φ(i) is a logical formula depending on i, for the set s { µi -→ pi s i | i ∈ I and φ(i)}.

  each, while the missing configuration, d, a, a, appears with a frequency of only 1%. What can the observer deduce? We note that Crypt 1 and Crypt 2 exhibit the same behavior while Crypt 0 behaves differently. Hence, by symmetry considerations (Coin 0 , Coin 1 and Coin 2 are opposite to Crypt 1 , Crypt 2 and Crypt 0 respectively) he can deduce that Coin 0 and Coin 1 must be biased in the same way, and Coin

2 must be biased differently. More precisely, Coin 0 and Coin 1 must produce almost always head, and Coin 2 must produce almost always tail (or vice-versa). From this estimation, it is immediate to conclude that, in the first case, the payer is almost for sure Crypt 1 , in the second case Crypt 2 , and in the third case Crypt 0 .

The definition given here corresponds to that in[START_REF] Schneider | CSP and anonymity[END_REF]. In[START_REF] Ryan | Modelling and Analysis of Security Protocols[END_REF] the authors use a different (but equivalent) definition: they require ρ(S\C) ∼T S\C for every permutation ρ in A.

It is easy to see that, for this example, it does not matter which interleaving we consider.

A Appendix

A.1 The π-calculus

We recall here the basic notions about the π-calculus. We choose the variant used in [START_REF] Boreale | Some congruence properties for π-calculus bisimilarities[END_REF][START_REF] Sangiorgi | π-calculus, internal mobility and agent-passing calculi[END_REF], which differs from the standard one because is has a guarded choice instead of the free choice. This is convenient because it will allow to introduce the probabilistic π-calculus, in the next section, in a smoother way.

Let N be a countable set of names, x, y, . . .. The set of prefixes, α, β, . . ., and the set of π-calculus processes, P, Q, . . ., are defined by the following abstract syntax:

Prefixes represent the basic actions of processes: x(y) is the input of the (formal) name y from channel x; xy is the output of the name y on channel x; τ stands for any silent (non-communication) action.

The process i α i .P i represents guarded (global) choice and it is usually assumed to be finite. We will use the abbreviations 0 (inaction) to represent the empty sum, α.P (prefix) to represent sum on one element only, and P + Q for the binary sum. The symbols νx, |, and ! are the restriction, the parallel, and the replication operator, respectively.

To indicate the structure of a process expression we will use the following conventions:

), i.e. the parallel operator is left associative, and α 1 .P 1 | α 2 .P 2 stands for (α 1 .P 1 )|(α 2 .P 2 ), i.e. the prefix operator has precedence over |. In all other cases of ambiguity we will use parentheses.

The operators νx and y(x) are x-binders, i.e. in the processes νxP and y(x).P the occurrences of x in P are considered bound, with the usual rules of scoping. The set of the free names of P , i.e. those names which do not occur in the scope of any binder, is denoted by fn(P ). The alpha-conversion of bound names is defined as usual, and the renaming (or substitution) P {y/x} is defined as the result of replacing all occurrences of x in P by y, possibly applying alpha-conversion to avoid capture.

In the paper we use also the construct if x = y then P else Q This expression is syntactic sugar standing for the process

The operational semantics is specified via a transition system labeled by actions µ, µ ′ . . .. These are given by the following grammar:

Action xy corresponds to the input prefix x(z), where the formal parameter z is instantiated to the actual parameter y (see Rule I-SUM in Table 1). Action xy correspond to the output of a free name. The bound output x(y) is introduced to model scope extrusion, i.e. the result of sending to another process a private (ν-bound) name. The bound names of an action µ, bn(µ), are defined as follows: bn(x(y)) = {y}; bn(xy) = bn(xy) = bn(τ ) = ∅. Furthermore, we will indicate by n(µ) all the names which occur in µ.

In literature there are two definitions for the transition system of the π-calculus which induce the so-called early and late bisimulation semantics respectively. Here we choose to present the first one. There is no difference between the two for the purposes of our paper. SUM

∃i. y ∈ fn(µi) and ∀i. p ′ i = pi/ P j:y ∈fn(µ j ) pj

Qi}i

Table 2. The probabilistic transition system of the πp-calculus.

CLOSE: This rule is analogous to COM, the only difference is that the name being transmitted is private (local) to the sender. CONG: This rule rule says that structurally equivalent processes perform the same transitions.

A.3 Relation between notions of anonymity for probabilistic users

In this appendix we prove the claim we made in Section 11 (and already proved in [START_REF] Beauxis | Formal approaches to information-hiding (tutorial)[END_REF]), namely that the notion of probabilistic anonymity of Halpern and O'Neil (cfr. Definition 4.4 in [START_REF] Halpern | Anonymity and information hiding in multiagent systems[END_REF]), i.e.

∀i,

is equivalent to our notion of anonymity (for fully probabilistic users) plus the condition that the a priori probabilities of two anonymous events are the same, that is:

In order to prove the above claim, let us recall our definition of anonymity as given in Definition 3:


Jonas Aparicio
email: jonas.aparicio@enpc.fr

Tien Hoang

Gwendal Cumunel

Gilles Foret

Yannick Jeanjean

Saint Julien Castres

Experimental and numerical study on the re-anchoring of wire in grouted prestressed tendons

Keywords: external prestressing, prestressed tendon, strand wire damage, wire re-anchoring

Some recent researches have focused on strand wire damage in external prestressing tendon. When some strand wires of a grouted prestressing cable are damaged, the tension in the cable can be preserved due to the re-anchoring phenomenon. For safety issues, it is important to study the damage limit that a tendon can suffer before the rupture. While the re-anchoring of a strand is well studied, there is less literature on wire re-anchoring. In this study, we tested grouted seven-wire strands which are put under tension and then cut out wire by wire to simulate the wire damages. The re-anchoring is observed by strain gauges installed in the strands and on the sheath. In addition, a numerical model has been developed with the help of FEM to analyse the mechanical phenomenon during and after the wire cuts. The results show that the tendon is bent and twisted because of the loss of tension and moment when one or several wires are cut off. Moreover, the strand strain is various following the gauge position in each wire and its distance to the cut section. This result contributes to the comprehension of the wire damages in grouted tendons, and could be extended to grouted multiplestrand tendons.

INTRODUCTION

The re-anchoring of tendons with a whole broken strand was reviewed by [START_REF] Abdelatif | Modeling and Parametric Study of the Reanchorage of Ruptured Tendons in Bonded Posttensioned Concrete[END_REF]. The re-anchoring occurs due to friction. The mechanical characteristics of steel and concrete turn out to be the main parameters influencing the re-anchoring length. This result was confirmed by experimental studies of [START_REF] Watanabe | Evaluation for Flexural-load Capacity of Prestressed Concrete Girders with Broken Tendons[END_REF]. The re-anchoring is similar to a pretensioned strand bond, studied in some articles such as Oh, [START_REF] Hwan Oh | Theoretical Analysis of Transfer Lengths in Pretensioned Prestressed Concrete Members[END_REF] or [START_REF] Ramirez-Garcia | A Higher-Order Equation for Modeling Strand Bond in Pre-tensioned Concrete Beams[END_REF], which take into account loss of grout strength due to cracking. It suggests that the stress of the strand changes exponentially from 0, at the cutting position, to the final stress value, at a distance called transfer length from the cut strand. The Poisson's effect causes the cut end to adopt a wedge-like form that leads to friction with the other wires and the grout. Furthermore, the loss of tension in the wire unfolds the wire and thus increases the contact with the concrete; this is called the Hoyer effect, [START_REF] Briere | Dilation Behavior of Seven-Wire Prestressing Strand -The Hoyer Effect[END_REF]. The re-anchoring of a whole strand is presented in several Preprint 2 construction codes such as American Concrete Institute 2011, Eurocode EN-1992-1-1(2004) ( §8.10.2), and British code CS 455 ( §8.3.1). According to these codes, the re-anchoring length of a cut strand is of the order of one meter. Ghoreishi et al. (2007) have reviewed the difference generalized stiffness models for 7 wires strand. In those model, individual wires are modelled as beam in the Frenet coordinate system. Depending on the model, the friction, Poisson effect, and the wire flattening are considered. 3D finite element models of strand with contact conditions have been developed by de Menezes and Marczak (2021), [START_REF] Zhang | Finite Element Solutions to the Bending Stiffness of a Single-Layered Helically Wound Cable With Internal Friction[END_REF], [START_REF] Judge | Full 3D Finite Element Modelling of Spiral Strand Cables[END_REF] or [START_REF] Karathanasopoulos | Finite Element Modeling of the Elastoplastic Axial-Torsional Response of Helical Constructions to Traction Loads[END_REF]. These articles focus on the generalised mechanical behaviour of the strand.

When no wire is cut, each helical wire has the same tension, which is proportional to the central wire tension [START_REF] Foti | Modeling the Axial-Torsional Response of Metallic Strands Accounting for the Deformability of the Internal Contact Surfaces: Derivation of the Sym-metric Stiffness Matrix[END_REF].Otherwise, the re-anchoring of a strand wire has been studied by [START_REF] Colin | Mechanical Model for Unbonded Seven-Wire Tendon with Single Broken Wire[END_REF]. This study shows that the cutting of a wire of a strand not subjected to radial confinement but deflected leads to a re-anchoring length of more than 10 meters. When a wire is cut on a monostrand, the stress in the wire is redistributed according to the angle made by the wire, the central wire and the cut wire, as shown in FIGURE 1. The re-anchoring is partial and the strand tension decreases by 2-4 % for each cut (in a seven-wire strand, each wire account for around 14% of the tension). They assume that stress redistribution is symmetric but nonhomogeneous. 2018) used analytical and FE models to derive the static response of a strand with broken wires. Other finite element models of strands with broken wires have been developed by Abdullah et al. (2016a and b). In the second article, wires are cut with radial confinement done by other steel strands tied together. This radial confinement is less efficient than the one presented in the present paper. The measured transfer length between the cut and the end of the bench is more than 30 meters.

The study proposed in this paper aims at understanding the mechanical evolution of a grouted monostrand in which the steel wires were damaged. Three 50 m long grouted monostrands were built and damaged until the rupture of the cable. The tendons were monitored while they were damaged. A numerical model faithful to the built tendons was created to further enhance the understanding of the mechanical behaviour of a monostrand. Preprint 3

EXPERIMENTAL CAMPAIGN

The experimental tests were performed on a 200 m bench at Gustave Eiffel University (UGE) in Nantes -France (see Figure 3). This campaign was funded by the AFSA (Association des sociétés françaises d'autoroutes). Three tendons were built by Freyssinet company. First, the strands were put through the anchoring system and HDPE sheaths. In the first two tests, the central sheath was transparent PVC in order to be able to visually follow the propagation of the cracks in the grout. The PVC and HDPE sheaths were linked with a screw connection. The anchoring systems were installed at the two ends of the tendon with a force sensor at the passive end. Then, the tension was applied with a jack at the active end to a tension of 70 % of the strand strength and the tendon was injected with Superstressem grout. The tension of the monostrands before the cut test was between 186 kN and 204 kN. The tendon have a length of 46.6 m and the grout rested for 7 days before the cutting. A 20 cm hatch (10 cm for the third tendon) was made in the sheath by removing the grout in order to access the strand wires. The wires were cut manually, one by one, with of a rotating Dremel (see Figure 2).The tension was measured by a dynamometric cell at the tendon passive end. Some strain gauges are glued on the wires and the HDPE sheath.

FIGURE 2 Cutting of wires on the 3rd and 2nd tendon A limit of this experiment is that we cannot reproduce the corrosion in the strands. The wire breaking occurs due to mechanical cutting and not corrosion. Another limit is that only monostrands were tested. Grouted prestressed tendons are mostly composed of multiple strands, usually 19. Furthermore, a 10 cm hatch was done to reach the wires with the saw, which has a mechanical impact.

NUMERICAL MODEL

A FEM model was developed using Abaqus to study the behaviour of tendons during and after the wire cuts. In this model, the wires are modelled by Timoshenko beam elements and the other tendon components (grout, HDPE sheath) are 3D elements. The wire diameters are 5.4 mm and 5.2 mm for the central and the outer wires respectively. An offset of 0.1 mm is set between wires and no offset between the outer wires and the grout. The lay angle of the helix is 7.8°and the pitch is 243.9 mm. This model does not take into account wire flattening and Poisson's effect but it allows the modelling of multiple lay length which would otherwise be too computationally expensive.

The material property were taken from the reference sheets when available. Poisson coefficients used are usual values (0.45 for HDPE, 0.3 for steel, and 0.2 for grout). The only remaining unknown is the grout Young's modulus but it was tested in the sensibility analysis. The contact between the wires and the grout is achieved with the generalised contact law implemented in Abaqus, allowing contacts between edges of two elements and between an edge and a face. A dynamic analysis with mass scaling is performed which is equivalent to a quasi-static analysis.

The two main simplifying assumptions are that wire are modelled as 1D Timoshenko beam and that the material density is changed in order to speed up computations by using mass scaling as done by de Menezes and Marczak (2021). Mass scaling change the density of the elements in order to reach a target stable increment. Thus the model is not accurate for the dynamic effect but remain accurate for the equilibrium once the computation has converged. Poisson effect is not taken into account. The re-anchoring of wires only occurs due to the Hoyer effect. According to [START_REF] Foti | Modeling the Axial-Torsional Response of Metallic Strands Accounting for the Deformability of the Internal Contact Surfaces: Derivation of the Sym-metric Stiffness Matrix[END_REF], wire flattening and Poisson effect have little effect on the mechanical behaviour of the strand for low lay angle. This leads to a necessary overestimation of the friction coefficient. No breaking of the grout was considered in the simulation. Preprint 5

RESULTS

Loss of tension

This study shows experimentally and numerically that loss of tension related to wire damage is small enough to be within accuracy of most of tension measurement methods. However, an important damage will lead to a tension variation sufficient to be detectable. A very small loss of tension implies that most of the energy and strength in the cut wire is transferred to the other wires of the tendon (FIGURE 4). FIGURE 4 Experimental and numerical results of the tendon tension in function of the number of wire cuts (left) and Tension in each wire in numerical pseudo-time by the numerical model (right)

A numerical sensitivity analysis is performed to highlight the dependencies of the numerical model to different parameters (TABLE 1). The weak influence of the Young's modulus of the grout shows either that the re-anchoring is mostly due to inter-wire friction rather than grout-wire friction, or that the numerical model is not able to capture grout-wire friction. This could explain why the tension loss is higher in the numerical model than in the experimental tests.

Reanchoring (stress distribution in wires)

Friction causes the cut wire to regain its stress at a distance from the cutting position. This phenomenon, called re-anchoring, was previously studied with cut strand but sparsely with cut wire. The re-anchoring occurs because of the confinement of the strand in the grout. The re-anchoring of wire for an ungrouted tendon is of the order of 10 m. Contrary to the article of [START_REF] Colin | Mechanical Model for Unbonded Seven-Wire Tendon with Single Broken Wire[END_REF], the cut was performed while the strand is loaded, thus allowing a loss of tension. Cuts of the wires of the numerical model were simulated until the rupture of the tendon. FIGURE 5 shows that the grout confinement allows re-anchoring over lengths less than 10 m. The numerical model successfully captures the re-anchoring of a wire and the redistribution of the stresses inside the strand. FIGURE 5 Strain on the wire according to the state of the strand and the distance to the cut

Damage of the grout and the sheath

The sheath of the first monostrand, chosen transparent to follow the propagation of the cracks, is brittle. The sheath was found to be more brittle than the grout and so the cracks could be traced directly to the sheath. Cracks on the grout and the sheath follow the same helical geometry as the geometry of stress on the numerical model (FIGURE 7). This result is important because it shows that the cracks follow the helical geometry of the wires caused by the damage part. The experimental and numerical results show that the strain on the sheath has a lay length periodicity and is exponentially decreasing, as shown FIGURE 6.

CONCLUSION

Experimental tests were carried out by cutting one by one the wires of a grouted monostrand. The results show that a stress redistribution occurs inside the strand. A FE numerical model was developed by using beam element for the wires and 3D elements for the grout and the sheath. The numerical results agree well with the experimental results. Then, the model is used to analyse the sensitivity of the model parameters and to study how the stresses are redistributed between the wires. The re-anchoring of wires is different from strand re-anchoring due to the helical geometry of the cut wires. The tension loss is all the more important as the radial confinement is degraded. In the experimental tests, the degradation of the grouting was responsible for the different values of tension loss. The impact of wire damage on sheath strain was also explored. In future works, we will present the experimental and numerical results achieved on 5-strand tendons to contribute more on the understanding of the re-anchoring behaviour of prestressed tendons.

FIGURE 1

 1 FIGURE 1 Left different class of symmetry in a strand with one broken wire. Right strain in the different wire after breaking of a wire. Both extracted from MacDougall and Bartlett (2006) Beltran et al. (2018) used analytical and FE models to derive the static response of a strand with broken wires. Other finite element models of strands with broken wires have been developed byAbdullah et al. (2016a and b). In the second article, wires are cut with radial confinement done by other steel strands tied together. This radial confinement is less efficient than the one presented in the present paper. The measured transfer length between the cut and the end of the bench is more than 30 meters.

Preprint 4 FIGURE 3

 43 FIGURE 3 Set up of the experimental bench

Figure 6

 6 Figure 6 Strain on the upper and lower line of the sheath

TABLE 1

 1 Evolution of tension (kN) due to the variation of different parameters of the numerical model

	Preprint