Christelle Braun
email: braun@lix.polytechnique.fr

Konstantinos Chatzikokolakis

Catuscia Palamidessi
email: catuscia@lix.polytechnique.fr

Compositional Methods for Information-Hiding

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 the user's privacy is compelling.

We can 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

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.

In the field of information flow and non-interference 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] Clark | Quantitative analysis of the leakage of confidential data[END_REF][START_REF] Clark | Quantified interference for a while language[END_REF][START_REF] Lowe | Quantifying information flow[END_REF] in which the high information and the low information are seen as the input and output respectively of a (noisy) channel. Non-interference is formalized in this setting as the converse of channel capacity.

Channel capacity has been also used in relation to anonymity in [START_REF] Moskowitz | Covert channels and anonymizing networks[END_REF][START_REF] Moskowitz | Quasi-anonymous channels[END_REF]. 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 as information leakage 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.

Hypothesis testing

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. The attempt to infer S from O is called hypothesis testing (the "hypothesis" 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 known the a priori probability distribution of the hypotheses, and 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 also called Bayes risk. In [START_REF] Chatzikokolakis | Probability of error in informationhiding protocols[END_REF], we proposed to define the degree of protection provided by a protocol as the Bayes risk associated to the matrix.

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 both the scenario in which the input distribution is known, in which case we consider the Bayes risk, and the one in which we have no information on the input distribution, or it changes over time. In this second scenario, we consider as degree of protection the probability of error associated to the Maximum Likelihood rule, averaged on all possible input distributions. It turns out that such average is equal to the value of the probability of error on the point of uniform distribution, which is much easier to compute.

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.

The proofs are omitted for lack of space. They can be found in the report version of this paper, available on line at http://www.lix.polytechnique.fr/ ˜catuscia/papers/Anonymity/Compositional/report.pdf.

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

Preliminaries

In this section we recall some basic notions of probability theory 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]).

A discrete probability measure over a set X is a function µ : 2 X → [0, 1] such that µ(X) = 1 and µ(∪ i X i ) = i µ(X i ) where X i is a countable family of pairwise disjoint subsets of X. We denote the set of all discrete probability measures over X by Disc(X). For x ∈ X, we denote by δ(x) (the Dirac measure on x) the probability measure that assigns probability 1 to {x}. 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 )(Y ) = i c i µ i (Y ).
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 because later in the paper states will be process terms, and S will be used for certain 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) the set of all the finite non-maximal executions of M, and by exec(M) the set of all the executions of M.

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 its 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 all nondeterministic choices using ζ. Note that etree(M, ζ) is a fully probabilistic automaton. Given a fully probabilistic automaton M we can define a probability space on the set exec(M) of executions of M (see [START_REF] Segala | Modeling and Verification of Randomized Distributed Real-Time Systems[END_REF] for more details). Similarly, given a probabilistic automaton M and a scheduler ζ for M, we can define a probability space on the set of traces of M by using the same construction on etree(M, ζ), which is a fully probabilistic automaton.

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 finite-state 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 PROB

• P i pi Ti τ -→ P i pi δ(Ti) ACT j ∈ I I ai.Ti a j -→ δ(Tj) PAR1 T1 a -→ µ T1 | T2 a -→ µ | T2 PAR2 T2 a -→ µ T1 | T2 a -→ T1 | µ REP T | ! T a -→ µ ! T a -→ µ | ! T COM T1 a -→ δ(T ′ 1 ) T2 a -→ δ(T ′ 2 ) T1 | T2 τ -→ δ(T ′ 1 | T ′ 2 ) RES T b -→ µ φ = a, a (νa)T b -→ (νa)µ
Table 1. The semantics of CCSp.

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:

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 = 1 -p. Similarly we will use a 1 .T 1 a 2 .T 2 to represent a binary secret or nondeterministic choice.

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 are those derivable from the rules in Table 1. We will use the notations (T, a, µ) and T a -→ µ interchangeably. 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 la-beled 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, so a secret choice (with different guards) is determined by the input. The scheduler has to resolve only the residual nondeterminism.

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 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 * ⇀ T such that:

(i) if 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, if a ∈ Sec then a = s m+1 then ζ(s)(φ) is defined, and it is one of such transitions. 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).

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

Modeling protocols for information-hiding

We propose here 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 π = (π s1 , π s2 , . . . , π sm ), where π s is the probability of the input s.

To fit the model of the channel, we assume that at each run, the protocol is given exactly one secret s i to conceal. This is not a restriction, because the s i 's can be complex information like sequences of keys or tuples of individual data. 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 forms 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 assume that only a finite set of such sequences is relevant. This is certainly true if the term is terminating, which is usually the case in security protocols where each session is supposed to terminate in finite time.

Thus the set S could be, for example, the set of all sequences of secret actions up to a certain length (for example, the maximal length of executions) and analogously O could be the set of all sequences of observable actions up to a certain length. To be more general, we will just assume S ⊆ fin Sec * and O ⊆ fin Obs * .

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 4. 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 1 -p(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 (Probability of error, [20]). 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 to 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 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 to 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 actually a minimum: Proposition 1. For every CCS p process T we have

inf ζ∈A P MAP (M ζ (T ), π) = min ζ∈A P MAP (M ζ (T ), π)
Thanks to previous proposition, we can define the degree of protection provided by a protocols in terms of the minimum probability of error. Definition 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 ), π)
The problem with the MAP rule is that it assumes that the input distribution is known to the adversary. This is often not the case, so it is natural to try to approximate it with some other rule. One such rule is 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 name comes from the fact that p(o|s) is called the likelihood of s given o. We will denote the corresponding probability of error by P ML (M, π). The following characterization is an immediate consequence of Definition 5 and of the Bayes Theorem.

P ML (M, π) = 1 - O max s (p(o|s))π s
It has been shown (see for instance [START_REF] Chatzikokolakis | Anonymity protocols as noisy channels[END_REF]) that under certain conditions on the matrix, the ML rule approximates indeed the MAP rule, in the sense that by repeating the protocol the adversary can make the probability of error arbitrarily close to 0, with either rule.

We could now define the degree of protection provided by a term T under the ML rule as the minimum P ML (M ζ (T ), π), but it does not seem reasonable to give a definition that depends on the input distribution, since the main reason to apply a non-Bayesian approach is that indeed we do not know the input distribution. Instead, we define the degree of protection associated to a process term as the average probability of error with respect to all possible distributions π: Definition 7. Given a CCS p process T , the protection Pt ML (T ) provided by T , in the Maximum Likelihood approach, is given by

Pt ML (T ) = min ζ∈A (m -1)! π P ML (M ζ (T ), π) d π
In the above definition, (m -1)! represents a normalization function:

1 (m-1)! is the hyper-volume of the domain of all possible distributions π on S, namely the (m -1)dimensional space of points π such that 0 ≤ π s ≤ 1 and 0 ≤ s∈S π s = 1 (where m is the cardinality of S).

Fortunately, it turns out that this definition is equivalent to a much simpler one: the average value of the probability of error, under the Maximum Likelihood rule, can be obtained simply by computing P ML on the uniform distribution π u = ( 1 m , 1 m , . . . , 1 m ).

Theorem 1.

Pt ML (T ) = min

ζ∈A P ML (M ζ (T ), π u )
The next corollary follows immediately from Theorem 1 and from the definitions of P MAP and P ML .

Corollary 1.

Pt ML (T ) = min

ζ∈A P MAP (M ζ (T ), π u )
We conclude this section with some properties of P MAP . Note that the same properties hold also for P ML on the uniform distribution, because P ML (M, π u ) = P MAP (M, π u ).

The next proposition shows that the probabilities of error are concave functions with respect to the space of matrices. Proposition 2. 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 , π)
Corollary 2. 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.

P MAP (M ′ , π) ≥ P MAP (M, π)
The following propositions are from the literature.

Proposition 4 ([21]

). 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, π) = 1 -max 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 ([22]

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

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

Theorem 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 [START_REF] Fujioka | A practical secret voting scheme for large scale elections[END_REF] 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
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 π = p 1 or max π = 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 π, hence Pt MAP (T ′ , π) < Pt MAP (T, π).

The reason why we need the condition (i) in Definition 8 for the parallel operator is analogous to the case of secret choice. The following is a counterexample. The reason why we need the condition (ii) in Definition 8 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. It is easy to see that Pt MAP (T 2 , π) = 1 -max π. 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 we have that 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. Following the same reasoning as in example 1, we have that for certain π, 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 in [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 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, which can give either 0 or 1. The coins get 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 payer: the binary sum of all declarations is 1 if and only if there is a payer, because all the coins get 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 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 actions. 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 3 in both directions and derive that P MAP (M ′ , π) = 1 -max i π i .

We can conclude, therefore, that Pt MAP (T, π) = 1 -max i π i in the class of schedulers A ∪ B.

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

Consider now the term T ′ = (νc ℓ,h c r,h )(Coin h | T ) obtained from T by adding back the coin h. By applying Theorem 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 Pt MAP (T, π) is maximum, we have Pt MAP (DC , π) = 1 -max i π i , which concludes the proof.

Interestingly, also the other direction of Theorem 4 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 5. A DC is strongly anonymous only if it has a spanning tree consisting of fair coins only.

Conclusion and future work

In this paper we have investigated the properties of the probability of error associated to a given information-hiding protocol, and we have investigated CCS p constructs that are safe, i.e. that are guaranteed not to decrease the protection of the protocol. 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.

In the future, we would like to extend our results to other constructs of the language. This is not possible in the present setting, as the examples after Theorem 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 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.

Definition 3 .

 3 Given a term T and a scheduler ζ : S → exec * → T , the matrix M ζ (T ) associated to 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 in Obs is o.

Proposition 3 .

 3 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:

Example 2 .

 2 Let Sec and S be as in Example 1. Define T 1 = s 1 .0 s 2 .0 and T 2 = o 1 .0 o 2 .0. Clearly, Pt MAP (T 2 , π) = 1 -max π. 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 1, where T ′ = T 1 | T 2 and T = T 2.

Example 3 .

 3 Let Sec and S be as in Example 1. 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).

Definition 8 .

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

)

  Pt MAP ((νo 1 , o 2 , . . . , o k ) (T 1 | T 2 )) ≥ Pt MAP (T 2 , π) if T 1 ando 1 , o 2 , . . . , o k are safe w.r.t. T 2 Unfortunately the safety property does not hold for the secret choice. The following is a counterexample. Example 1. Let Sec = {s 1 , s 2 } and assume that S does not contain the empty sequence. Let T = o 1 .0 o 2 .0. Then Pt MAP (T, π) is maximum (i.e. Pt MAP (T, π) = 1 -max π) because for every sequence s ∈ S we have p(o 1 |s) = p(o 2 |s). Let T ′ = s 1 .T s 2 .T . We can now define a scheduler such that, if the secret starts with s 1 , it selects o 1 , and if the secret starts with s 2 , it selects o 2 . Hence, under this scheduler, p(o 1 |s 1

⋆ This work has been partially supported by the INRIA DREI Équipe Associée PRINTEMPS and by the INRIA ARC project ProNoBiS.

Crypt i = ci,i 1 (x1) . . . . . ci,i k (x k ) . pay i (x) . di x1 + . . . + x k + x Coin h = cℓ,h 0 . cr,h 0 .0 ⊕p h cℓ,h 1 . cr,h 1 .0 Collect = d1(y1) . d2(y2) . . . . . dn(yn) . out y1, y2, . . . , yn 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 3 ([23]

). If the multigraph is connected, and the coins are fair, then DC is strongly anonymous, namely for every s and o, p(s|o) = π 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 protocol can be described 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. See Table 2. 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 4.

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. This situation corresponds to the original formulation of Chaum and so we can apply Chaum's result (Theorem 3) and Proposition 5 to conclude that all the rows of the matrix M are the same and hence, by Proposition 4, P MAP (M, π) = 1 -max i π i .


Donato Sorgente
email: d.sorgente@poliba.it

Luigi Tricarico
email: tricarico@poliba.it

A NUMERICAL-EXPERIMENTAL APPROACH TO MATERIAL CHARACTERIZATION AND PROCESS ANALYSIS IN THE BLOW FORMING PROCESS

Keywords: Superplasticity, material characterization, blow forming

In carrying out a superplastic forming process, the first step for the process optimization is a detailed material characterization. The achievement of a successfully formed component is strictly related to the material behaviour: commonly, several tensile tests are carried out at different temperatures and strain rates for locating the best deformation parameters, corresponding to which maximum uniform elongation of the material can be found. Additionally, characterization is needed also for estimating material parameters to numerically model the process. Numerical modelling is a necessary step when the pressure profile of a blow forming process has to be optimized. In this paper authors present a methodology for estimating material parameters on the basis of few bulge tests and for analysing the superplastic forming process. Temperature and pressure influences are analysed by means of free inflation tests. Material parameters are calculated starting from an analytical approach and refining the solution by an inverse analysis. A 3D numerical model of the process has been then created and used for evaluating the pressure profile that is able to keep the strain rate value in the sheet close to a target value. A numerical-experimental comparison has been done for testing the model capability and effectiveness of the pressure profile in a prismatic closed die blow forming test. Good agreement has been found between experimental results and numerical simulations. Thickness distribution measurements, optical microscope observations, post-forming characteristics evaluation have been performed to compare constant pressure and constant strain rate tests.

INTRODUCTION

In the superplastic (SP) field, the individuation of the appropriate forming temperature and strain rate is the first step for a successful process implementation but also for its optimization. Usually to understand the best process parameters, tensile tests are carried out on several specimens at different temperatures and strain rates. The temperature and the strain rate that lead to the highest uniform elongation, corresponding to the higher strain rate sensitivity index m, are considered as process parameters for the following step. The superplastic forming (SPF) process is then performed on the basis of tensile tests results. In spite of the consolidated interest in SP light metallic alloys, it is not so simple to find information in the specific literature, because every kind of treatment brings to different material characteristics and, even if the alloy composition of two samples and their mean grain size are similar, their behaviour could be very different as far as SPF applications are concerned [START_REF] Cleveland | Comparison of superplastic behavior in two 5083 aluminum alloys[END_REF]. Furthermore, since Finite Element (FE) numerical modelling and analysis have gained great potentialities and interest in the simulation of forming processes, material characterization and constitutive modelling have become of great significance not only for predicting material behaviour but also for directly optimizing process parameters. Many constitutive equations have been studied and verified for describing and modelling the behaviour of SP materials [START_REF] Chandra | Constitutive behaviour of superplastic materials[END_REF]. In a blow forming (BF) process, the optimal strain rate can be achieved and kept constant on the sheet changing the gas pressure value according to a specific law. This kind of law is generally created by a numerical FE model in order to keep the strain rate constant and close to the optimal value in the whole sheet. Thus, the quality of the formed part is strongly influenced by the accurateness of material constants used in the FE model. Last studies are focused also in obtaining very accurate pressure laws where the equivalent target strain rate is managed and varied during the process for enhancing material properties taking into account also microcavities evolution and grain growth effects [START_REF] Nazzal | On the stability of superplastic biaxial stretching using finite element simulations[END_REF]. In this case material constants become further important as the constitutive equation must consider also parameters like static and dynamic grain growth and cavity growth. Other efforts have been also made in analysing possible differences between the uni-axial characterization by tensile tests and other alternative method with strain conditions more similar to the forming process ones [START_REF] Bellet | Finite Element Modeling of Superplastic Sheet Forming Processes. Identification of Rheological and Tribological Parameters by Inverse Method[END_REF][START_REF] Cheng | The determination of material parameters from superplastic inflation tests[END_REF]. Post-forming mechanical strength of the material is a very important matter in SPF applications: as material goes under cavitation and grain growth, the mechanical strength after forming can be seriously affected according to the forming parameters. Since each geometry and each particular application have different strength requirements, there are not specific procedures to characterize the formed material, but several studies can be found in literature where tensile test specimens have been machined from the formed component and tested to evaluate post-forming static and dynamic strength [START_REF] Khraisheh | Investigation of Post-Superplastic Forming Properties of AZ31 Magnesium Alloy[END_REF][START_REF] Chen | A study of post-form static and fatigue properties of superplastic 7475-SPF and 5083-SPF aluminium alloys[END_REF]. In this work authors have analyzed the SP behaviour of a superplastic aluminium AA7475 alloy. Blanks with an initial thickness of 0.8 mm have been used in the whole experimentation. The SP behaviour of this material has been considered well approximated by the Backofen equation where the equivalent stress is related to the equivalent strain rate by a power law. The characterization has been done with preliminary free inflation constant pressure tests at different temperature and pressure values. Material constants have been calculated by an analytical approach and then verified with a simple 2D FE numerical model. An inverse technique with a gradient-based method has been then used to calibrate the material behaviour in the FE model. Closed die BF tests have been then carried out in a prismatic die cavity, with constant pressure and different forming times. A 3D model of these tests have been created and the pressure profile able to keep the strain rate along the sheet constant have been estimated. Then constant strain rate pressure law has been applied on the sheet in experimental tests. The formed specimen obtained with that pressure profile has been compared, in terms of thickness distribution, microcavities and post-forming tensile strength, with the specimen obtained with constant pressure.

EXPERIMENTAL FACILITY

Both the material characterization and the closed die forming tests have been performed on a laboratory scale Blow Forming (BF) equipment embedded in the cylindrical split furnace of an INSTRON universal testing machine (max load 200kN). The equipment consists in: (i) a blank-holder, (ii) female dies with different cavity shapes for generating on the blank different forming conditions, (iii) a pneumatic circuit for the gas supply with an Argon (Purity: 99.990%) cylinder, proportional electronic valves, steel tubes in the proximity of the forming chamber and flexible polyurethane tubes in colder zones, (iv) an electrical furnace (max power 3kW, precision ± 2°C) with its electronic controllers for upper, central and lower zones which can be set with three different temperatures for compensating thermal dispersion, (v) thermocouples to monitor thermal condition on the sheet and on the tools, (vi) a transducer for measuring, during free inflation test, the dome height on the specimen and (vii) a PC with a data acquisition I/O device by which gas pressure, temperature, blankholder force can be monitored and managed. A little fan, just out of the furnace, is used for the cooling of the upper part of the equipment to avoid excessive heating near the load cell of the INSTRON machine. In this equipment the undeformed sheet is interposed between the creep-resistant steel tools (the die and the blankholder) and the gas pressure acts on one side of the sheet forcing it to copy the geometry of the die cavity. Since forming tools are embedded in the split furnace of the INSTRON machine, the die and blankholder dimensions have been designed to fit the internal furnace diameter (90mm). A blankholder force, which allows having no drawing during the test and no gas leakages from the forming chamber, is applied before the gas adduction and kept constant during the whole test. For material characterization, bulge tests are performed with a cylindrical die cavity (inner diameter 45 mm) in which the sheet can freely expand; the dome height of the specimen is monitored during the whole test by the digital acquisition of the position transducer signal. It is not worthless to notice that the specimen cutting accurateness is much less relevant than in traditional tensile tests where the gauge length zone has to be precisely finished to avoid crack propagation during the test. Further details about the equipment can be found in [START_REF] Sorgente | Material superplastic parameters valuation by a jump pressure blow forming test[END_REF]. Using the same equipment described above and a die with a different cavity shape, closed die tests can be performed and the real forming process can be analysed in a more detailed way. Since some of the most common limits of forming technologies are the minimum corner radius that the sheet can fill without ruptures and the non axially symmetric filling of the die cavity, a prismatic die cavity was chosen for testing the material and the process capabilities in closed die forming tests. A die with a 14.5mm deep prismatic cavity has been used. The cavity has a squared section with a side length of 40 mm and a fillet radius between sides of 5 mm.

MATERIAL CH ARACTERIZATIO N

Material characterization has been based on few free inflation tests performed on the aforementioned BF equipment. As summarized in the schematic flow chart in Fig. 1, material constants have been found first by an analytical approach and then, after the creation of a 2D numerical model of the free inflation test, by optimizing their values by an inverse analysis.

FREE I N F L AT I O N T E S T S

The cylindrical cavity in the female die in which the sheet expands, is depth enough to carry on the test till the failure of the material without any contact between the sheet and the die bottom. In the experimental plan two levels of temperature (410°C and 460°C) and two levels of pressure (0.3 MPa and 0.7 MPa) has been used for testing material formability, as shown in Fig. 2. All the specimens tested in the experimental plan have failed on the dome apex, except for the test carried out with the lowest pressure and temperature levels, in which, after 5000 s, gas pressure was stopped even if the failure of the material was not achieved. Best formability was observed for the lowest pressure level on the highest temperature (0.3 MPa at 460°C) were the specimen reached a final dome height of 25.9 mm that corresponds to a normalized polar height (dome height to die inner radius ratio) of 1.15. In the explored range, the highest temperature level appears to be the most suitable for obtaining SP deformation on the examined material. In Fig. 3 the dome height evolution is shown for all the tests carried out for the material characterization. Pressure and temperature have similar effect on the strain rate imposed on the sheet: increasing either pressure or temperature brings to a reduction of the forming time that the sheet needs to get to a fixed height. In order to develop and to verify the proposed characterization methodology and to analyze the process potentialities, a single temperature level (460°C) was chosen and considered in the following numerical and experimental BF tests.

ANALYTICAL A P P R O A C H

According to one of the first analytical approaches that has been followed by [START_REF] Jovane | An approximate analysis of the superplastic forming of a thin circular diaphragm: theory and experiments[END_REF], during a bulge test of a thin SP sheet in a cylindrical die, some assumptions can be done: the material is isotropic, the volume remains constant, elastic strains are negligible, the thickness to diameter ratio of the sheet is very small and bending effects are negligible, at any instant the sheet is equivalent to part of a thin sphere subjected to internal pressure, so that the curvature and the thickness are uniform and a state of uniform biaxial tension exists at any point on the sheet [START_REF] Jovane | An approximate analysis of the superplastic forming of a thin circular diaphragm: theory and experiments[END_REF]. Starting from these assumptions many researcher has built up models of the BF of thin sheet; among them, Cheng developed a method for the evaluation of material parameters from a simple inflation test done with a BF equipment with a constant forming pressure; Enikeev and Kruglov, starting from two bulge tests with two different pressure values, proposed a method to obtain material constants and to take into account the non-uniform thickness distribution along the sheet [START_REF] Cheng | The determination of material parameters from superplastic inflation tests[END_REF][START_REF] Enikeev | An analysis of the superplastic forming of a thin circular diaphragm[END_REF].

In this work, for the chosen temperature level and starting from the following equation:

σ =C⋅ εm ( 1
)
where σ is the equivalent stress, ε is the equivalent strain rate, C, the strength coefficient, and m, the strain rate sensitivity index, material constants have been calculated by the method proposed by Enikeev and Kruglov, considering free inflation tests obtained, at 460°C, at two different pressure levels (0.3 MPa and 0.7 MPa).

2D N U M E R I C A L M O D E L O F F R E E I N F L AT I O N T E S T

A simple axially symmetric numerical model has been created using the commercial FE code ABAQUS with an elasto-viscoplastic integration. The deformable part corresponding to the aluminium blank has been divided into continuum elements with 4 nodes and one integration point, the die and the blankholder have been considered perfectly rigid. The sheet has been constrained in its periphery to have no translations and allowing only changing its thickness. The temperature has been considered perfectly stable and the material has been modelled with Eq. 1. In the ABAQUS software, for viscoplastic material, the CREEP option is available and the equivalent creep strain in the elements is computed by a power law of the equivalent deviatoric stress:

Δε= ε⋅Δt = A⋅σ n ⋅Δt ( 2
)
where Δt is the time increment in the implicit integration and material constants can easily be related to the Eq. 1 ones: A=(1/C) 1/m and n=1/m [11].

INVERSE A N A LY S I S

To understand if the calculated values of C and m are sufficiently accurate in predicting material behaviour, they have been directly input in the numerical model. Experimental conditions have been simulated for the free inflation tests described in section 3.1. The numerical height evolution during the inflation tests has been compared with the experimental one and the error between numerical and experimental results has been quantified by an objective function Q: the smaller this function the sharper the numerical result. This function is based on information not only related to the final strain distribution of the specimen, but, since hot forming applications are strongly affected by time and strain rate, this function is build also on time evolution of the deformed shape of the specimen. Therefore, to distinguish good solutions from bad ones, the time evolution of the dome height has been taken into account. The dome height h curve has been approximated with a six order polynomial equation. The Q function is computed as follows:

Q= ∑ i=1 N Q i N with Q i = [ h comp t i -h exp  t i  h exp  t i  ] 2 (3)
where the subscript comp indicates the computed values (from the FE simulation), exp the experimental ones, t i are time values of the N numerical frames at which the computation is done (it depends on the output file of the simulation).

The minimum seek of the Q function is done by an iterative procedure, updating material parameters (C and m) by a gradient based optimization technique. The gradient of the objective function is computed by the finite differences method through the interaction between an external python script and the FE solver. This inverse procedure goes on until the objective function reaches a value under a prescribed threshold value [START_REF] Sorgente | Material superplastic parameters valuation by a jump pressure blow forming test[END_REF].

In this kind of analysis the numerical model represents the forward model and the free inflation test is the experimental reference on which the inverse analysis is based [START_REF] Liu | Computational inverse techniques in nondestructive evaluation[END_REF]. Minimizing the error between results from the forward model and the experimental reference, accurate material parameters can be obtained. On the other hand, inverse analysis can occasionally lead to solutions that are not physically valid, even the objective function is sufficiently small. Moreover, a limit of gradient based approaches, in spite of their fast convergence after few iteration steps, is the possibility to find a local minimum that gives a small value of the objective function but not represent the reality in the best way. Furthermore, a strong correlation between C and m exists, since either the variation of first or of the second parameter can lead to similar effect on the consistency of the material. This means that potentially infinite couples of C and m can give good results with small values of the Q function, well predicting the behaviour of the material in the simulated test representing the experimental reference. Generally, if the solution is not sufficiently accurate, the obtained C and m values give good results in reproducing the test that has been used as experimental reference in the inverse analysis but give bad results when load conditions of the test change. Making the inverse analysis starts from values that are not far from real ones can bring to optimized results that can well represent the physical phenomenon. In this work material constants have been firstly calculated by the approach proposed by Enikeev and Kruglov and, then, they have been optimized through the described inverse analysis procedure and finally verified in different load conditions (changing the gas pressure in the free inflation test). In Fig. 4 results of the inverse analysis are shown. In order to compare the starting solution with the optimized one, the numerical dome height curve obtained with the starting C and m values achieved with the analytical approach has been illustrated in the same graph with the experimental and the optimized ones. For the experimental reference test (pressure: 0.3 MPa), in order to avoid numerical instabilities, the time range for the Q calculation was chosen excluding the initial and the final transient phases, during which the dome height rate rapidly changes (time range: 80 s ÷ 1100 s). After two iterations, the Q function is reduced from 0.021, corresponding to the starting value (obtained by the analytical approach), to 0.002 at the end of the optimization procedure.

As can be seen in Fig. 4, the numerical curve obtained after the inverse analysis is much closer to the experimental one than the one obtained by the analytical approach. Material constants refined by the inverse analysis have been then verified simulating the test with a different pressure value (0.7 MPa) obtaining, also in this different load condition, a good agreement with experimental results.

PROCESS ANALYSIS

Free inflation tests can be considered a good way for the characterization of the material but are not enough complete to obtain information about the BF process and its potentialities and limits. In industrial applications of BF, the sheet strongly interacts with the die wall and with the die bottom to get the final shape. In this work the material characterization phase has been followed by an experimental and numerical analysis of the process in closed die forming tests. An experimental plan with constant pressure (CP) and different forming time values has been firstly carried out to observe the deformation evolution during the forming process. Then, a 3D numerical model of the closed die BF process has been created and calibrated on the basis of experimental results. The calibrated numerical model has been then used in a more direct process analysis and for obtaining the pressure profile able to keep the strain rate in the sheet constant and close to a target value. The so calculated pressure profile has been then applied in experiments and differences, in terms of specimen characteristics after forming, between CP and constant strain rate (CSR) tests have been reported and discussed.

CONSTANT P R E S S U R E E X P E R I M E N TA L T ES T S

In the first phase of the experimental activity, CP tests have been carried out. Tests have been stopped at three different time instants to follow the material filling in die cavity. In particular, in Fig. 5, images of the specimens obtained with a CP of 0.7 MPa are shown for 300s, 900s and 1800s. From CP tests it is possible to note that, after 300 s, the sheet has already touched the die bottom and it has started the calibration phase to get to the final shape. After 900 s the contact area between the sheet and the die bottom has increased its extension and, especially along the median axis of the square section of the specimen, the sheet has touched the die vertical walls and gained a sharper corner radius. Finally, comparing specimens at 900 s and 1800 s, it can be said that the shape has no significant changes but along the diagonals the specimen have a more detailed profile. The radius on the profile along the median axis of the square section has been measured by an optical digital system. In Fig. 6 the value of this geometrical parameter is plotted as a function of the forming time. The value of the radius rapidly decreases in the first part of the forming process: from 300 s to 900 s the radius value drops by 57% (from 8.2 mm to 3.2 mm) and takes other 900 s to reach a value of about 2.5 mm. It can be said that, at a CP of 0.7MPa, the die filling rapidly increases in the first part of the process, touching the die bottom in few seconds, but needs much longer forming time to get smaller values of the corner radii between the bottom and the wall of the specimen, especially along the diagonal axis of the square section of the specimen.

3D N U M E R I C A L M O D E L O F T H E BLOW FORMING P R O C E S S

A 3D numerical FE model reproducing the forming process has been developed to test material constants also in closed die forming tests and to analyze in a more detailed way the BF process. In Fig. 7 a schematic representation of the FE model is shown. The die and the blankholder have been modelled as rigid surfaces. Only a quarter of the sheet has been modelled; continuum elements have been used and, in a similar way to the axial symmetric model, the sheet has been constrained in its periphery allowing only its thickness variation. Material behaviour has been modelled in the same way described in section 3.3 concerning the 2D model.

MODEL C A L I B R AT I O N

As seen also in experimental tests, the contact conditions between the sheet and the die surfaces strongly influences the process: after the contact between the sheet and the die bottom the filling rate suddenly decreases and the sheet takes a long time to get to the final shape. The sensitivity of the deformation process to the friction coefficient between the sheet and the die cavity surface is consequently high and by the numerical simulation it can be seen that different forming time and different thickness distribution can be obtained for different friction coefficients. Free inflation tests alone can't give sufficient information about contact conditions, since the contact area is relatively small, so the 3D numerical model of the closed die forming tests has been calibrated on the basis of the previous experimental tests with a prismatic die cavity. By an inverse analysis, similar to the one used to find material constants, the friction coefficient that better represent the real sheet behaviour has been searched among physically plausible values: a Coulomb friction coefficient close to 0.6 has been found. In Fig. 8 results, after the model calibration, are shown for the CP test at different forming times. Numerical simulation allows examining the evolution of the forming process: before the contact between the sheet and the die cavity bottom, the most stressed area is in the central part of the specimen and the strain distribution is similar to the one of a free inflation tests; as soon as the sheet touches the die cavity bottom, the strain in the central zone of the specimen remain almost constant (denoting an almost instantaneous drop of the strain rate in this area) and the deformation moves to the edge areas; at the end of the forming process the areas of the specimen along the diagonal axis appears to be the most critical where the highest thinning can be reported.

PRESSURE P R O F I L E F O R C O N S TA N T S T R A I N R AT E T E S T

Once the material constants have been verified and the contact condition between die and sheet has been calibrated, the numerical model has been used to get the pressure profile able to get a CSR on the sheet during the process. Due to the geometry of the die cavity, sheet undergoes to different strain conditions according to the considered area and to the forming phase. Thus, significantly different strain rates can be found along the sheet and the location of critical zones changes during the process: in first phase, in which the sheet freely expand in the die cavity the most critical zone (with the highest strain rate value), is located on the dome apex, while in the second phase, after the sheet touches the die bottom, the highest strain rates can be found along the diagonal axis of the square section.

The ABAQUS software contains a built-in algorithm (named CREEP STRAIN RATE CONTROL) which allows the maximum strain rate, in a given set of elements, being controlled in order to have an almost constant value regulating the pressure load. This procedure gives good results even if, because of the step condition adopted, it changes the pressure load only if the strain rate value reaches an upper or a lower limit [11]. In this work it has been chosen an other algorithm based on the one proposed by [START_REF] Hwang | Study on superplastic blow-forming of 8090 Al-Li sheets in an ellip-cylindrical closed-die[END_REF]: the ABAQUS numerical model has been interfaced with a FORTRAN subroutine able to continuously control the pressure upon the sheet and to keep the maximum strain rate of the whole sheet around a constant value. The algorithm computes the optimal pressure by the following relation:

p  t Δt = [ 1 -ln  εcomp εt arg et  ⋅Δt ] ⋅p t  (4)
where p is the load value, ε comp is the maximum equivalent strain rate value in the defined element set computed by the FE solver, ε t arg et is the target value of the equivalent strain rate, t is the analyzed time instant and Δt is the time increment, that has to be kept small to avoid oscillations in the pressure curve. The algorithm implemented in the FORTRAN subroutine gives a more continuous curve and the equivalent strain rate is adequately kept constant around the target value. This kind of curve for the pressure controlling is also more suitable for the LabView program interfaced to the pressure regulator and for better results it can be approximated by a six order equation with an elevated correlation factor. The chosen target strain rate was set on 5x10 -4 1/s; in Fig. 9 pressure profiles obtained both from the built-in ABAQUS algorithm and from the external subroutine are plotted. The two different algorithms produces a similar trend of the pressure value: in the first phase, during which the most critical zone is in the centre of the specimen, before the contact between the sheet and the die bottom, the pressure increases with a decreasing derivative; in the second phase, during which the areas with the highest strain rate values are along the edges of the specimen, the pressure derivative is positive and rapidly raises. The pressure profile obtained from the external algorithm has been applied in a closed die forming test with the same material and the same cavity shape of previous tests. A forming time of 3500 s was chosen in order to get a die filling similar to the one achieved with a CP value of 0.7 MPa after 1800 s.

CONSTANT P R E S S U R E A N D C O N S TA N T S T R A I N R AT E C O M PA R I S O N

Experimental test with CP have been compared with CSR ones to analyze the effectiveness of the optimized pressure profile adoption. First of all, experiments, as numerical simulations, show how, to get a similar die filling, the test with a CP value of 0.7 MPa takes about half the time needed with a CSR imposed on the sheet of 5x10 -4 1/s. In an industrial point of view time reduction can be a great advantage in the part manufacturing, but this advantage must go together with a good part quality. As mentioned before, post-forming characteristics is an important matter in SPF application and, in the specific of this work, optical microscopy, measurement of the thickness distribution and of the mechanical strength of the deformed material have been used as characterizing methodologies.

THICKNESS A N D M I C R O C AV I T I E S C O M PA R I S O N

One of the first comparisons has been done in terms of thickness distribution along the sheet: thickness values have been measured along the median axis of the square section of the formed specimens in both conditions (CP and CSR). Considering specimens with similar die filling, the corner radius zone corresponding to the area between the die wall and the die bottom is the most critical one in both cases; no significant differences can be found between the two different load conditions: the larger difference between the thickness in homologous measurement points in the two specimens is about 0.02 mm that is close to the precision of the measurement method. Since thickness measurement has not denoted significant differences between the two specimens, the analysis has moved to the microcavities analysis by optical microscopy. In Fig. Despite the pressure has been profiled in order to keep the strain rate around a controlled target value, a larger cavity presence in the specimen obtained by the CSR test can be seen. Cavity growth is related to the strain, to the strain rate that the material experiences in the forming process, to the grain size and to the temperature [START_REF] Chen | Cavity growth and filament formation of superplastically deformed Al 7475 Alloy[END_REF][START_REF] Blandin | Effect of the nature of grain boundary regions on cavitation of a superplastically deformed aluminium alloy[END_REF]. Since the temperature is the same, the strain level is almost the same in both specimens, the difference between them can be principally explained by the different strain rate and the different exposition times to elevate temperature that influences the grain size during the forming process. Time dependencies of the cavity volume fraction have been evaluated analysing different time steps for the CP test: no significant time variation can be reported since cavities, in the central zone of the specimen, are evident even after 300 s. Their quantity and their dimension remain almost constant as far the CP test is concerned.

STRAIN R AT E C O M PA R I S O N

To better understand the strain rate that the sheet experiences in the test with a CP, in Fig. 11 the variable is plotted versus time for two nodes of the FE mesh corresponding to the central area and to the diagonal corner. The central zone (point A in Fig. 11) is deformed with high strain rates in the first phase of the process, with a maximum value of about 1x10 -2 1/s, and after the contact between the sheet and the cavity bottom its strain does not change anymore. Analyzing the diagonal corner (point B in Fig. 11), after an initial peak the strain rate remains lower than 3x10 -3 1/s and continuously decreases till a value of 5x10 -5 1/s when the test is stopped (1800 s). It can be stated that (i) the sheet, for the majority of the test duration, is not exposed to high strain rate values; (ii) the central part of the specimen experiences a strain rate higher than 4x10 -3 1/s for all the part of the test in which the sheet freely expand without touching the die bottom; (iii) in the second half the strain rate value become lower than the value that in the other test has been used as target value (5x10 -4 1/s). Both the ultimate tensile stress (UTS) and the yield stress of the material are negatively affected by the forming process. On the other hand, the material, that in the base conditions has a strong work hardening, gains ductility after the forming process. Moreover, ductility can be considered one of the most significant factors in comparing tests with different load profiles. The UTS is, in fact, quite similar for all the specimens, its maximum value is registered for the CSR test, denoting a more sound post-formed material condition in the central area of the specimen. In the specimen formed with a CP ductility is always lower than the one of the specimen formed wit a CSR and inversely proportional to the forming time. Another proof of the higher integrity of the material in the central part after the CSR test is the strain distribution in the tensile test specimen. By a digital image correlation system (ARAMIS 3D) the strain maps on the specimen can be obtained during the entire tensile test. For instance in Fig. 13, the major strain maps are plotted for tensile tests performed on specimens from the CP test (0.7 MPa and 1800 s) and the CSR test (5x10 -4 1/s and 3500 s) that have achieved similar die filling. Analyzing local strain distribution, in the CSR test specimen a more uniform distribution can be found resulting in a global measured ductility higher than the one measured in the CP test, even if the maximum local strain value is higher in the latter one. This behaviour can be justified with a higher occurrence of defects in the material that has not been formed with a controlled strain rate.

POST-FORMING M E C H A N I C A L S T R E N G H T C O M

CONCLUSIONS

The experimental-numerical methodology for the characterization of a SP material that have been proposed in this work, have been described and verified: testing the outputs of this methodology, in a BF process analysis, it can be seen that it represent a good instrument for the material characterization and for the process optimization. Numerical model can be used in predicting the material behaviour during forming and for optimizing the BF process according to the best material performances. The experimental and numerical activities described and discussed in this work allow assessing that:

-material superplastic formability is strongly influenced by temperature and strain rate; in a free inflation test, changing the forming gas pressure and consequently the imposed strain rate, can lead to a great difference in the final dome height achieved before failure; in the explored range of pressure and temperature values and for the considered alloy, best results have been found for 460° C and low pressure values;

-for a datum temperature, material constants can be found by means of few bulge tests starting from an analytical approach and refining the solution by an inverse technique; based on a gradient based method, the described inverse procedure is fast and sufficiently accurate; -in CP closed die BF test, strain rate strongly decreases after the contact between the sheet and the die cavity bottom. Comparing a CP test with CSR test with similar die filling it can be said that:

-the test with a CP value of 0.7 MPa takes about half the time needed with a CSR imposed on the sheet of 5x10 -4 1/s; -in the most critical zone (the corner area along the diagonal axis) lower cavities volume fraction can be observed for the CP test; -the mechanical strength measured after forming in the central zone of the formed specimens, CSR shows a slightly higher UTS and a significantly higher ductility; -in the CP test, cavities dimension and quantity reach their maximum value, in the central part of the formed specimen, in the first part of the test, during which the imposed strain rate is maximum. A more detailed analysis can be done extending the explored temperature and pressure values to a wider range and verifying the proposed approach also for different values of those parameters. Free inflation tests, as well closed die forming tests, with a back pressure imposed on the sheet, can be carried out to reduce the cavitation phenomenon and to compare CP and CSR test in a different condition: reducing defects by cavitation, tests can be performed keeping constant the strain rate only in the area of the sheet that show maximum values of the strain in the final configuration and this, according to the part geometry, could speed up the process without reducing part quality.

Figure 1 .

 1 Figure 1. Schematic flow chart of the material characterization phase.

Figure 2 .

 2 Figure 2. Material characterization: scheme of the experimental plan and corresponding specimens.

Figure 3 .

 3 Figure 3. Material Characterization: dome height evolution of free inflation tests.

Figure 4 .

 4 Figure 4. Inverse analysis: experimental dome height versus time curve compared with numerical ones before and after the inverse procedure.

Figure 5 .

 5 Figure 5. Constant pressure test with 0.7 MPa: formed specimens at three different forming time values (starting from the left 300s, 900s and 1800s).

Figure 6 .

 6 Figure 6. Specimen corner radius between the die cavity bottom and the die wall versus forming time.

Figure 7 .

 7 Figure 7. Schematic representation of the numerical 3D model of the BF process.

Figure 8 .

 8 Figure 8. Numerical model of the closed die BF test: results after the model calibration for the a constant pressure test (0.7 MPa) at different forming times (60s, 300s, 900s, 1800s).

Figure 9 .

 9 Figure 9. Constant strain rate closed die BF test: pressure profiles obtained both from the built-in ABAQUS algorithm and from the external subroutine.

  10, two micrographs of the most critical zone along the diagonal corner of the formed part are shown.

Figure 10 .

 10 Figure 10. Micrographs of the most critical zone of the formed specimens for constant pressure (0.7MPa for 1800s) and constant strain rate (5x10 -4 1/s for 3500s) with similar die filling.

Figure 11 .

 11 Figure 11. Strain rate versus time for two nodes of the FE mesh corresponding to the central area and to the diagonal corner in the constant pressure tests with a gas pressure of 0.7 MPa.

  PA R I S O N Small tensile test specimens (gauge length 8 mm, width 5 mm) have been machined from the flat part of the formed component obtained from both CP and CSR tests. Tensile tests have been performed on the base material (undeformed) and on specimens obtained with CP and CSR. In Fig. 12 results are reported. In particular, for the CP tests, the material has been tests after three different forming times to understand the time influence on the mechanical strength of the material.

Figure 12 .

 12 Figure 12. Tensile flow curves for the base material (before forming) and for formed specimens.

Figure 13 .

 13 Figure 13. Major strain values for tensile tests performed on formed specimens from the CP test (0.7 MPa and 1800 s) and the CSR test (5x10 -4 1/s and 3500 s) with similar die filling.

Carcassonne, France from 3-5 September 2008

th EUROSPF Conference

ACKNOWLEDGEMENTS

Authors gratefully acknowledge the Alenia Aeronautica S.p.A. company and, in particular, Massimiliano Di Paola, for making the experiments possible and for the help given in the interpretation of results.