Véronique Cortier

Antoine Dallon

Stéphanie Delaune

Bounding the number of agents, for equivalence too ⋆

Bounding the number of agents is a current practice when modeling a protocol. In 2003, it has been shown that one honest agent and one dishonest agent are indeed sufficient to find all possible attacks, for secrecy properties. This is no longer the case for equivalence properties, crucial to express many properties such as vote privacy or untraceability. In this paper, we show that it is sufficient to consider two honest agents and two dishonest agents for equivalence properties, for deterministic processes with standard primitives and without else branches. More generally, we show how to bound the number of agents for arbitrary constructor theories and for protocols with simple else branches. We show that our hypotheses are tight, providing counter-examples for non actiondeterministic processes, non constructor theories, or protocols with complex else branches.

Introduction

Many decision procedures and tools have been developed to automatically analyse cryptographic protocols. Prominent examples are ProVerif [START_REF] Blanchet | An automatic security protocol verifier based on resolution theorem proving (invited tutorial)[END_REF], Avispa [START_REF] Armando | The AVISPA Tool for the automated validation of internet security protocols and applications[END_REF], Scyther [START_REF] Cremers | The Scyther Tool: Verification, falsification, and analysis of security protocols[END_REF], or Tamarin [START_REF] Schmidt | Automated analysis of Diffie-Hellman protocols and advanced security properties[END_REF], which have been successfully applied to various protocols of the literature. When modeling a protocol, it is common and necessary to make some simplifications. For example, it is common to consider a fix scenario with typically two honest and one dishonest agents. While bounding the number of sessions is known to be an unsound simplification (attacks may be missed), bounding the number of agents is a common practice which is typically not discussed. In 2003, it has been shown [START_REF] Comon-Lundh | Security properties: Two agents are sufficient[END_REF] that bounding the number of agents is actually a safe practice for trace properties. One honest agent and one dishonest agent are sufficient to discover all possible attacks against secrecy (for protocols without else branches). The reduction result actually holds for a large class of trace properties that encompasses authentication: if there is an attack then there is an attack with b + 1 agents where b is the number of agents used to state the security property.

Trace properties are typically used to specify standard properties such as confidentiality or authentication properties. However, privacy properties such as vote privacy [START_REF] Delaune | Verifying privacy-type properties of electronic voting protocols[END_REF] or untraceability [START_REF] Arapinis | Analysing unlinkability and anonymity using the applied pi calculus[END_REF], or simply properties inherited from cryptographic games [START_REF] Comon-Lundh | Computational soundness of observational equivalence[END_REF] (e.g. strong secrecy) are stated as equivalence properties. For example, Alice remains anonymous if an attacker cannot distinguish between a session with Alice from a session with Bob. When studying equivalence properties, the practice of bounding the number of agents has been continued. For example, most of the example files provided for equivalence in the ProVerif development [START_REF] Blanchet | Proverif 1.91[END_REF] model only two or three agents.

The objective of this paper is to characterise when it is safe to bound the number of agents, for equivalence properties. In case of secrecy expressed as a trace property, bounding the number of agents is rather easy. If there is an attack then there is still an attack when projecting all honest agents on one single honest agent, and all dishonest agents on one single dishonest agent. This holds because the protocols considered in [START_REF] Comon-Lundh | Security properties: Two agents are sufficient[END_REF] do not have else branches: the conditionals only depend on equality tests that are preserved by projection.

Such a proof technique no longer works in case of equivalence. Indeed, an attack against an equivalence property may precisely rely on some disequality, which is not preserved when projecting several names on a single one. Consider for example a simple protocol where A authenticates to B by sending him her name, a fresh nonce, and a hash of these data.

A → B : A, B, N, h(A, N )

Let's denote this protocol by P (A, B). This is clearly a wrong authentication protocol but let assume we wish to know whether it preserves A's privacy. In other words, is it possible for the attacker to learn whether A or A ′ is talking? That is, do we have P (A, B) equivalent to P (A ′ , B)? We need A = A ′ to observe an attack, otherwise the two processes are identical. This example shows in particular that it is not possible to consider one honest agent and one dishonest agent as for trace properties. Another issue comes from non deterministic behaviours. Non equivalence between P and Q is typically due to some execution that can be run in P and not in Q due to some failed test, that is, some disequality. Even if we maintain this disequality when projecting, maybe the projection enables new behaviours for Q, rendering it equivalent to P . Since non-determinism is usually an artefact of the modelling (in reality most protocols are perfectly deterministic), we assume in this paper action-deterministic protocols: the state of the system is entirely determined by the behaviour of the attacker. Such determinacy hypotheses already appear in several papers, in several variants [START_REF] Cheval | Deciding equivalence-based properties using constraint solving[END_REF][START_REF] Chadha | Automated verification of equivalence properties of cryptographic protocols[END_REF][START_REF] Baelde | Partial order reduction for security protocols[END_REF].

Our contribution. We show that for equivalence, four agents are actually sufficient to detect attacks, for action-deterministic protocols without else branches and for the standard primitives. We actually provide a more general result, for arbitrary constructor theories and for protocols with (some) else branches. Equational theories are used to model cryptographic primitives, from standard ones (e.g. encryption, signature, or hash) to more subtle ones such as blind signa-tures [START_REF] Delaune | Verifying privacy-type properties of electronic voting protocols[END_REF] or zero-knowledge proofs [START_REF] Backes | Zero-knowledge in the applied pi-calculus and automated verification of the direct anonymous attestation protocol[END_REF]. The notion of constructor theories (where agents can detect when decryption fails) has been introduced by B. Blanchet [START_REF] Blanchet | An efficient cryptographic protocol verifier based on prolog rules[END_REF]. It captures many cryptographic primitives and in particular all the aforementioned ones, although associative and commutative properties (e.g. exclusive or) are out of their scopes since we assume the exchanged messages do not contain destructors. Else branches are often ignored when studying trace properties since most protocols typically abort when a test fails. However, a privacy breach may precisely come from the observation of a failure or from the observation of different error messages. A famous example is the attack found on the biometric French passport [START_REF] Chothia | A traceability attack against e-passports[END_REF]. We therefore consider protocols with simple else branches, where error messages may be emitted in the else branches.

Our general reduction result is then as follows. We show that, for arbitrary constructor theories and action-deterministic protocols with simple else branches, we may safely bound the number of agents to 4b + 2 where b is the blocking factor of the theory under consideration. Any theory has a (finite) blocking factor and the theories corresponding to standard primitives have a blocking factor of 1. Moreover, in case protocols do not have else branches, then the number of agents can be further reduced to 2b + 2 (b + 1 honest agents and b + 1 dishonest agents), yielding a bound of 2 honest agents and 2 dishonest agents for protocols using standard primitives.

We show moreover that our hypotheses are tight. For example, and rather surprisingly, it is not possible to bound the number of agents with the pure equational theory dec(enc(x, y), y) (assuming the function symbol dec may occur in messages as well). Similarly, we provide counter-examples when processes are not action-deterministic or when processes have non simple else branches.

Due to lack of space, the reader is referred to the companion technical report [START_REF] Cortier | Bounding the number of agents, for equivalence too[END_REF] for the missing proofs and additional details.

Related work.

Compared to the initial work of [START_REF] Comon-Lundh | Security properties: Two agents are sufficient[END_REF] for trace properties, we have considered the more complex case of equivalence properties. Moreover, we consider a more general framework with arbitrary constructor theories and protocols with (simple) else branches. Our proof technique is inspired from the proof of [START_REF] Chrétien | Checking trace equivalence: How to get rid of nonces[END_REF], where it is shown that if there is an attack against equivalence for arbitrary nonces, then there is still an attack for a fix number of nonces. Taking advantage of the fact that we bound the number of agents rather than the number of nonces, we significantly extend the result: (simple) else branches; general constructor theories with the introduction of the notion of b-blocking factor; general action-deterministic processes (instead of the particular class of simple protocols, which requires a particular structure of the processes); and protocols with phase (to model more game-based properties).

Model for security protocols

Security protocols are modelled through a process algebra inspired from the applied pi calculus [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF]. Participants in a protocol are modelled as processes, and the communication between them is modelled by means of the exchange of messages that are represented by terms.

Term algebra

We consider two infinite and disjoint sets of names: N is the set of basic names, which are used to represent keys, nonces, whereas A is the set of agent names, i.e. names which represent the agents identities. We consider two infinite and disjoint sets of variables, denoted X and W. Variables in X typically refer to unknown parts of messages expected by participants while variables in W are used to store messages learnt by the attacker. Lastly, we consider two disjoint sets of constant symbols, denoted Σ 0 and Σ error . Constants in Σ 0 will be used for instance to represent nonces drawn by the attacker and this set is assumed to be infinite, while constants in Σ error will typically refer to error messages. We assume a signature Σ, i.e. a set of function symbols together with their arity. The elements of Σ are split into constructor and destructor symbols, i.e.

Σ = Σ c ⊎ Σ d . We denote Σ + = Σ ⊎ Σ 0 ⊎ Σ error , and Σ + c = Σ c ⊎ Σ 0 ⊎ Σ error .
Given a signature F , and a set of atomic data A, we denote by T (F , A) the set of terms built from atomic data A by applying function symbols in F . Terms without variables are called ground. We denote by T (Σ + c , N ∪ A ∪ X ) the set of constructor terms. The set of messages M Σ is some subset of ground constructor terms. Given a set of atomic data A, an A-renaming is a function ρ such that dom(ρ) ∪ img(ρ) ⊆ A. We assume M Σ as well as T (Σ + c , N ∪ A ∪ X )\M Σ to be stable under any A-renaming and (Σ 0 ∪ Σ error )-renaming. Intuitively, being a message or not should not depend on a particular constant or name.

Example 1. The standard primitives (symmetric and asymmetric encryption, signature, pair, and hash) are typically modelled by the following signature. Σ std = {enc, dec, shk s , aenc, adec, pub, priv, sign, checksign, h, , proj 1 , proj 2 , eq}. The symbols enc and dec (resp. aenc and adec) of arity 2 represent symmetric (resp. asymmetric) encryption and decryption whereas shk s , pub, priv are constructor keys of arity 1. Pairing is modelled using of arity 2, whereas projection functions are denoted proj 1 and proj 2 (both of arity 1). Signatures are represented by sign of arity 2 with an associated verification operator checksign of arity 3. Hash functions are modelled by h, of arity 1. Finally, we consider the function symbol eq to model equality test. This signature is split into two parts: we have that Σ c = {enc, aenc, h, sign, shk s , pub, priv, } and Σ d = Σ std Σ c .

We denote vars(u) the set of variables that occur in a term u. The application of a substitution σ to a term u is written uσ, and we denote dom(σ) its domain. The positions of a term are defined as usual. The properties of cryptographic primitives are modelled through a rewriting system, i.e. a set of rewriting rules of the form g(t 1 , . . . , t n ) → t where g is a destructor, and t, t 1 , . . . , t n are constructor terms. A term u can be rewritten in v if there is a position p in u, and a rewriting rule g(t 1 , . . . , t n ) → t such that u| p = g(t 1 , . . . , t n )θ for some substitution θ. Moreover, we assume that t 1 θ, . . . , t n θ as well as tθ are messages. We only consider sets of rewriting rules that yield a convergent rewriting system. We denote u↓ the normal form of a given term u.

A constructor theory E is given by a signature Σ together with a notion of messages M Σ , and a finite set of rewriting rules R (as decribed above) that defines a convergent rewriting system.

Example 2. The properties of the standard primitives are reflected through the theory E std induced by the following convergent rewriting system: dec(enc(x, y), y) → x proj i ( x 1 , x 2 ) → x i with i ∈ {1, 2}. adec(aenc(x, pub(y)), priv(y)) → x checksign(sign(x, priv(y)), x, pub(y)) → ok eq(x, x) → ok

We may consider M Σ to be T (Σ + c , N ∪ A) the set of all ground constructor terms. We may as well consider only terms with atomic keys for example.

Constructor theories are flexible enough to model all standard primitives. However, such a setting does not allow one to model for instance a decryption algorithm that never fails and always returns a message (e.g. dec(m, k)).

For modelling purposes, we split the signature Σ into two parts, namely Σ pub and Σ priv , and we denote Σ + pub = Σ pub ⊎ Σ 0 ⊎ Σ error . An attacker builds his own messages by applying public function symbols to terms he already knows and that are available through variables in W. Formally, a computation done by the attacker is a recipe, i.e. a term in T (Σ + pub , W).

Process algebra

We assume an infinite set Ch = Ch 0 ⊎ Ch fresh of channels used to communicate, where Ch 0 and Ch fresh are infinite and disjoint. Intuitively, channels of Ch fresh are used to instantiate channels when they are generated during the execution of a protocol. They should not be part of a protocol specification. Protocols are modelled through processes using the following grammar:

P, Q = 0 | let x = v in P else 0 | new n.P | in(c, u).P | let x = v in P else out(c, err) | (P | Q) | out(c, u).P | ! new c ′ .out(c, c ′ ).P | i: P
where c, c ′ ∈ Ch, x ∈ X , n ∈ N , err ∈ Σ error , and i ∈ N. We have that u is a constructor term, i.e. u ∈ T (Σ + c , N ∪ A ∪ X ) whereas v can be any term in

T (Σ + , N ∪ A ∪ X ).
Most of the constructions are rather standard. We may note the special construct ! new c ′ .out(c, c ′ ).P that combines replication with channel restriction. The goal of this construct, first introduced in [START_REF] Baelde | Partial order reduction for security protocols[END_REF], is to support replication while preserving some form of determinism, as formally defined later. Our calculus allows both message filtering in input actions as well as explicit application of destructor symbols through the let construction. The process "let x = v in P else Q" tries to evaluate v and in case of success the process P is executed; otherwise the process is blocked or an error is emitted depending on what is indicated in Q. The let instruction together with the eq theory introduced in Example 2 can encode the usual "if then else" construction. Indeed, the process if u = v then P else Q can be written as let x = eq(u, v) in P else Q. Since P can be executed only if no destructor remains in the term eq(u, v), this implies that u and v must be equal. Our calculus also introduces a phase instruction, in the spirit of [START_REF] Blanchet | Automated verification of selected equivalences for security protocols[END_REF], denoted i: P . Some protocols like e-voting protocols may proceed in phase. More generally, phases are particularly useful to model security requirements, for example in case the attacker interacts with the protocol before being given some secret.

We denote by fv (P ) (resp. fc(P )) the set of free variables (resp. channels) that occur in a process P , i.e. those that are not in the scope of an input or a let construction (resp. new construction). A basic process built on a channel c is a process that contains neither | (parallel) nor ! (replication), and such that all its inputs/outputs take place on the channel c.

Example 3. The Denning Sacco protocol [START_REF] Denning | Timestamps in key distributed protocols[END_REF] is a key distribution protocol relying on symmetric encryption and a trusted server. It can be described informally as follows, in a version without timestamps:

1. A → S : A, B 2. S → A : {B, K ab , {K ab , A} K bs } Kas 3. A → B : {K ab , A} K bs
where {m} k denotes the symmetric encryption of a message m with key k. Agent A (resp. B) communicates to a trusted server S, using a long term key K as (resp. K bs ), shared with the server. At the end of a session, A and B should be authenticated and should share a session key K ab . We model the Denning Sacco protocol as follows. Let k be a name in N , whereas a and b are names from A. We denote by x 1 , . . . , x n-1 , x n the term x 1 , . . . x n-1 , x n . The protocol is modelled by the parallel composition of three basic processes P A , P B , and P S built respectively on c 1 , c 2 , and c 3 . They correspond respectively to the roles of A, B, and S.

P DS =! new c 1 .out(c A , c 1 ).P A | ! new c 2 .out(c B , c 2 ).P B | ! new c 3 .out(c S , c 3 ).P S
where processes P A , P B , and P S are defined as follows.

-

P A = out(c 1 , a, b ).in(c 1 , enc( b, x AB , x B , shk s (a))).out(c 1 , x B ) -P B = in(c 2 , enc( y AB , a , shk s (b))) -P S = in(c 3 , a, b ). new k.out(c 3 , enc( b, k, enc( k, a , shk s (b)) , shk s (a))).

Semantics

The operational semantics of a process is defined using a relation over configurations. A configuration is a tuple (P; φ; i) with i ∈ N, and such that:

-P is a multiset of ground processes; -φ = {w 1 ⊲ m 1 , . . . , w n ⊲ m n } is a frame, i.e. a substitution where w 1 , . . . , w n are variables in W, and m 1 , . . . , m n are messages, i.e. terms in M Σ .

In (i: in(c, u).P ∪ P; φ; i)

in(c,R) ----→ (i: P σ ∪ P; φ; i)
where R is a recipe such that Rφ↓ is a message, and Rφ↓ = uσ for σ with dom(σ) = vars(u). Const (i: out(c, cst).P ∪ P; φ; i)

out(c,cst) -----→ (i: P ∪ P; φ; i) with cst ∈ Σ0 ∪ Σerror.
Out (i: out(c, u).P ∪ P; φ; i)

out(c,w)
-----→ (i: P ∪ P; φ ∪ {w ⊲ u}; i) with w a fresh variable from W, and u ∈ MΣ (Σ0 ∪ Σerror). Sess

(i: ! new c ′ .out(c, c ′ ).P ∪ P; φ; i) sess(c,ch) ------→ (i: P { ch / c ′ } ∪ i: ! new c ′ .out(c, c ′ ).P ∪ P; φ; i)
with ch a fresh name from Ch fresh .

Let (i: let x = v in P else Q ∪ P; φ; i) τ -→ (i: P { v↓ /x} ∪ P; φ; i) when v↓ ∈ MΣ. Let-Fail (i: let x = v in P else Q ∪ P; φ; i) τ -→ (i: Q ∪ P; φ; i)
when v↓ ∈ MΣ.

Null (i: 0 ∪ P; φ; i) τ -→ (P; φ; i) Par (i: (P | Q) ∪ P; φ; i) τ -→ (i: P ∪ i: Q ∪ P; φ; i) New (i: new n.P ∪ P; φ; i) τ -→ (i: P { n ′ /n} ∪ P; φ; i) with n ′ a fresh name from N .

Move

(P; φ; i) Intuitively, i is an integer that indicates the current phase; P represents the processes that still remain to be executed; and φ represents the sequence of messages that have been learnt so far by the attacker.

phase i ′ ----→ (P; φ; i ′ ) with i ′ > i. Phase (i: i ′ : P ∪ P; φ; i) τ -→ (i ′ : P ∪ P; φ; i) Clean (i: P ∪ P; φ; i ′ ) τ -→ (P; φ; i ′ ) when i ′ > i.
We often write P instead of 0: P or ({0: P }; ∅; 0). The operational semantics of a process P is induced by the relation α -→ over configurations as defined in Figure 1.

The rules are quite standard and correspond to the intuitive meaning of the syntax given in the previous section. When a process emits a message m, we distinguish the special case where m is a constant (Const rule), in which case the constant m appears directly in the trace instead of being stored in the frame. This has no impact on the intuitive behaviour of the process but is quite handy in the proofs. Regarding phases (rules Move, Phase, and Clean), the adversary may move to a subsequent phase whenever he wants while processes may move to the next phase when they are done or simply disappear if the phase is over.

Given a sequence of actions α 1 . . . α n , the relation α1...αn -----→ between configurations is defined as the transitive closure of α -→. Given a sequence of observable action tr, we denote C tr = ⇒ C ′ when there exists a sequence α 1 , . . . , α n for some n such that C α1...αn -----→ C ′ , and tr is obtained from this sequence by removing all the unobservable τ actions. Definition 1. Given a configuration C = (P; φ; i), we denote trace(C) the set of traces defined as follows:

trace(C) = {(tr, φ ′ ) | C tr = ⇒ (P; φ ′ ; i ′ ) for some configuration (P; φ ′ ; i ′ )}.
Example 4. Let C DS = (P DS ; ∅; 0) with P DS as defined in Example 3. We have that (tr, φ) ∈ trace(C DS ) where tr, and φ are as described below:

tr = sess(c A , ch 1 ).sess(c B , ch 2 ).sess(c S , ch 3 ).out(ch 1 , w 1 ).in(ch 3 , w 1 ).

out(ch 3 , w 2 ).in(ch 1 , w 2 ).out(ch 1 , w 3 ).in(ch 2 , w 3 ); and

-φ = {w 1 ⊲ a, b , w 2 ⊲ enc( b, k, enc( k, a , shk s (b)) , shk s (a)), w 3 ⊲ enc( k, a , shk s (b))}.
This trace corresponds to a normal execution of the Denning Sacco protocol.

Action-determinism

As mentioned in introduction, we require processes to be deterministic. We provide in Section 4.3 an example showing why the number of agents may not be bound when processes are not deterministic. We consider a definition similar to the one introduced in [START_REF] Baelde | Partial order reduction for security protocols[END_REF], extended to process with phase.

Definition 2. A configuration C is action-deterministic if whenever C tr -→ (P; φ; i), and i: α.P and i: β.Q are two elements of P with α, β instruction of the form in(c, u), out(c, u) or new c ′ .out(c, c ′ ) then either the underlying channels c differ or the instructions are not of the same nature (that is, α, β are not both an input, nor both an output, nor both channel creations).

A process P is action-deterministic if C = (P ; φ; 0) is action-deterministic for any frame φ.

For such protocols, the attacker knowledge is entirely determined (up to αrenaming) by its interaction with the protocol. Lemma 1. Let C be an action-deterministic configuration such that C tr = ⇒ C 1 and C tr = ⇒ C 2 for some tr, C 1 = (P 1 ; φ 1 ; i 1 ), and C 2 = (P 2 ; φ 2 ; i 2 ). We have that i 1 = i 2 , and φ 1 and φ 2 are equal modulo α-renaming.

Trace equivalence

Many privacy properties such as vote-privacy or untraceability are expressed as trace equivalence [START_REF] Delaune | Verifying privacy-type properties of electronic voting protocols[END_REF][START_REF] Arapinis | Analysing unlinkability and anonymity using the applied pi calculus[END_REF]. Intuitively, two configurations are trace equivalent if an attacker cannot tell with which of the two configurations he is interacting. We first introduce a notion of equivalence between frames. Definition 3. Two frames φ 1 and φ 2 are in static inclusion, written φ 1 ⊑ s φ 2 , when dom(φ 1 ) = dom(φ 2 ), and:

-for any recipe R ∈ T (Σ + pub , W), we have that Rφ 1 ↓ ∈ M Σ implies that Rφ 2 ↓ ∈ M Σ ; and -for any recipes R, R ′ ∈ T (Σ + pub , W) such that Rφ 1 ↓, R ′ φ 1 ↓ ∈ M Σ , we have that: Rφ 1 ↓ = R ′ φ 1 ↓ implies Rφ 2 ↓ = R ′ φ 2 ↓.
They are in static equivalence, written

φ 1 ∼ φ 2 , if φ 1 ⊑ s φ 2 and φ 2 ⊑ s φ 1 .
An attacker can see the difference between two sequences of messages if he is able to perform some computation that succeeds in φ 1 and fails in φ 2 ; or if he can build a test that leads to an equality in φ 1 and not in φ 2 (or conversely).

Example 5. Consider φ 1 = φ ∪ {w 4 ⊲ enc(m 1 , k)} and φ 2 = φ ∪ {w 4 ⊲ enc(m 2 , k ′ )}
where φ has been introduced in Example 4. The terms m 1 , m 2 are public constants in Σ 0 , and k ′ is a fresh name in N . We have that the two frames φ 1 and φ 2 are statically equivalent. Intuitively, at the end of a normal execution between honest participants, an attacker can not make any distinction between a public constant m 1 encrypted with the session key, and another public contant m 2 encrypted with a fresh key k ′ that has never been used.

Trace equivalence is the active counterpart of static equivalence. Two configurations are trace equivalent if, however they behave, the resulting sequences of messages observed by the attacker are in static equivalence. Definition 4. Let C and C ′ be two configurations. They are in trace equivalence, written C ≈ C ′ , if for every (tr, φ) ∈ trace(C), there exist (tr ′ , φ ′ ) ∈ trace(C ′ ) such that tr = tr ′ , and φ ∼ φ ′ (and conversely).

Note that two trace equivalent configurations are necessary at the same phase. Of course, this is not a sufficient condition. Example 6. The process P DS presented in Example 3 models the Denning Sacco protocol. Strong secrecy of the session key, as received by the agent B, can be expressed by the following equivalence: P 1 DS ≈ P 2 DS , where P 1 DS and P 2 DS are defined as follows. Process P 1 DS is process P DS with the instruction 1: out(c 2 , enc(m 1 , y AB )) added at the end of the process P B ; and P 2 DS is as the protocol P DS with the instruction 1: new k.out(c 2 , enc(m 2 , k)) at the end of P B . The terms m 1 and m 2 are two public constants from Σ 0 , and we use the phase instruction to make a separation between the protocol execution, and the part of the process that encodes the security property.

While the key received by B cannot be learnt by an attacker, strong secrecy of this key is not guaranteed. Indeed, due to the lack of freshness, the same key can be sent several times to B, and this can be observed by an attacker. Formally, the attack is as follows. Consider the sequence: tr ′ = tr.sess(c B , ch 4 ).in(ch 4 , w 3 ).phase 1.out(ch 2 , w 4 ).out(ch 4 , w 5 ) where tr has been defined in Example 4. The attacker simply replays an old session. The resulting (uniquely defined) frames are:

-φ ′ 1 = φ ∪ {w 4 ⊲ enc(m 1 , k), w 5 ⊲ enc(m 1 , k)}; and -φ ′ 2 = φ ∪ {w 4 ⊲ enc(m 2 , k ′ ), w 5 ⊲ enc(m 2 , k ′′ )}. Then (tr ′ , φ ′ 1 ) ∈ trace(P 1 DS ) and (tr ′ , φ ′ 2 ) ∈ trace(P 2 DS ). However, we have that φ ′ 1 ∼ φ ′ 2 since w 4 = w 5 in φ ′ 1 but not in φ ′ 2 .
Thus P 1 DS and P 2 DS are not in trace equivalence. To avoid this attack, the original protocol relies on timestamps.

Results

Our main goal is to show that we can safely consider a bounded number of agents. Our result relies in particular on the fact that constructor theories enjoy the property of being b-blockable, which is defined in Section 3.2. Our main reduction result is then stated in Section 3.3 with a sketch of proof provided in Section 3.4. We first start this section with a presentation of our model for an unbounded number of agents.

Modelling an unbounded number of agents

In the previous section, for illustrative purposes, we considered a scenario that involved only 2 honest agents a and b. This is clearly not sufficient when performing a security analysis. To model an unbounded number of agents, we introduce some new function symbols Σ ag = {ag, hon, dis}, each of arity 1. The term ag(a) with a ∈ A will represent the fact that a is an agent, hon(a) and dis(a) are intended to represent honest and compromised agents respectively. This distinction is used in protocol description to state the security property under study: typically, we wish to ensure security of data shared by honest agents. These symbols are private and not available to the attacker. We thus consider a term algebra as defined in Section 2. We simply assume in addition that Σ ag ⊆ Σ c ∩ Σ priv , and that our notion of messages contains at least {ag(a), hon(a), dis(a) | a ∈ A}.

Example 7. Going back to the Denning Sacco protocol presented in Example 3, we consider now a richer scenario.

P ′ A = in(c 1 , ag(z A )).in(c 1 , ag(z B )).1: P A P ′ B = in(c 2 , ag(z A ))
.in(c 2 , ag(z B )).1: P B P ′ S = in(c 3 , ag(z A )).in(c 3 , ag(z B )).1: P S where P A , P B , and P S are as defined in Example 3 after replacement of the occurrences of a (resp. b) by z A (resp. z B ). Then the process P ′ DS models an unbounded number of agents executing an unbounded number of sessions:

P ′ DS =! new c 1 .out(c A , c 1 ).P ′ A | ! new c 2 .out(c B , c 2 ).P ′ B | ! new c 3 .out(c S , c 3 ).P ′ S
It is then necessary to provide an unbounded number of honest and dishonest agent names. This is the purpose of the following frame. Definition 5. Given an integer n, the frame

φ hd (n) = φ a (n) ⊎ φ h (n) ⊎ φ d (n) is defined as follows: -φ a (n) = {w h 1 ⊲ a h 1 ; . . . ; w h n ⊲ a h n ; w d 1 ⊲ a d 1 ; . . . ; w d n ⊲ a d n }; -φ h (n) = {w hag 1 ⊲ ag(a h 1 ); w hon 1 ⊲ hon(a h 1 ); . . . ; w hag n ⊲ ag(a h n ); w hon n ⊲ hon(a h n )}; -φ d (n) = {w dag 1 ⊲ ag(a d 1 ); w dis 1 ⊲ dis(a d 1 ); . . . ; w dag n ⊲ ag(a d n ); w dis n ⊲ dis(a d n )};
where a h i , and

a d i (1 ≤ i ≤ n) are pairwise different names in A.
Of course, to model faithfully compromised agents, it is important to their keys to the attacker. This can be modelled through an additional process K that should be part of the initial configuration.

Example 8. Going back to our running example, we may disclose keys through the following process.

K =! new c ′ .out(c K , c ′ ).in(c ′ , dis(x)).out(c ′ , shk s (x)).
This process reveals all the keys shared between the server and a compromised agent. Strong secrecy of the exchanged key can be expressed by the following family of equivalences with n ≥ 0:

(P ′ DS | ! new c ′ 2 .out(c ′ B , c ′ 2 ).P ′ 1 | K; φ hd (n); 0) ≈ (P ′ DS | ! new c ′ 2 .out(c ′ B , c ′ 2 ).P ′ 2 | K; φ hd (n); 0) where P ′
1 and P ′ 2 are processes that are introduced to model our strong secrecy property as done in Example 6.

P ′ 1 = in(c ′ 2 , hon(z A )).in(c ′ 2 , hon(z B )). 1: in(c ′ 2 , enc( y AB , z A , shk s (z B ))). 2: out(c ′ 2 , enc(m 1 , y AB )) P ′ 2 = in(c ′ 2 , hon(z A )).in(c ′ 2 , hon(z B )). 1: in(c ′ 2 , enc( y AB , z A , shk s (z B ))). 2: new k ′ .out(c ′ 2 , enc(m 2 , k ′ ))
Our reduction result applies to a rather large class of processes. However, we have to ensure that their executions do not depend on specific agent names. Moreover, we consider processes with simple else branches: an else branche can only be the null process or the emission of an error message. Definition 6. A protocol P is a process such that fv (P ) = ∅, and fc(P ) ∩ Ch fresh = ∅. We also assume that P does not use names in A. Moreover, the constants from Σ error only occur in the else part of a let instruction in P . Example 9. Considering Σ error = ∅, it is easy to see that the processes

P ′ DS | ! new c ′ 2 .out(c ′ B , c ′ 2
).P ′ i | K with i ∈ {1, 2} are protocols. They only have trivial else branches.

Blocking equational theories

We aim at reducing the number of agents. To preserve equivalence, our reduction has to preserve equalities as well as disequalities. It also has to preserve the fact of being a message or not. We introduce the notion of b-blockable theories: a theory is b-blockable if it is always sufficient to leave b agents unchanged to preserve the fact of not being a message. Definition 7. A constructor theory E is b-blockable if for any term t ∈ T (Σ + , N ∪ A) M Σ in normal form, there exists a set of names A ⊆ A of size at most b such that for any A-renaming ρ with (dom(ρ) ∪ img(ρ)) ∩ A = ∅, we have that tρ↓ ∈ M Σ .

Example 10. Let eq 2 ∈ Σ d be a symbol of arity 4, and ok ∈ Σ c be a constant. Consider the two following rewriting rules: eq 2 (x, x, y, z) → ok and eq 2 (x, y, z, z) → ok This theory can be used to model disjonction. Intuitively, eq 2 (u 1 , u 2 , u 3 , u 4 ) can be reduced to ok when either u 1 = u 2 or u 3 = u 4 . Note that this theory is not 1-blockable. Indeed, the term t = eq 2 (a, b, c, d) is a witness showing that keeping one agent name unchanged is not sufficient to prevent the application of a rewriting rule on tρ (for any renaming ρ that leaves this name unchanged). Actually, we will show that this theory is 2-blockable.

A constructor theory is actually always b-blockable for some b.

Proposition 1. Any constructor theory E is b-blockable for some b ∈ N.

We note b(E) the blocking factor of E. This is the smallest b such that the theory E is b-blockable. Actually, not only all the theories are b-blockable for some b, but this bound is quite small for most of the theories that are used to model cryptographic primitives.

Example 11. The theory E std given in Example 2 is 1-blockable whereas the theory given in Example 10 is 2-blockable. These results are an easy consequence of Lemma 2 stated below.

The blocking factor of a constructor theory is related to the size of critical tuples of the theory. Definition 8. A constructor theory E with a rewriting system R has a critical set of size k if there exist k distinct rules ℓ 1 → r 1 , . . . , ℓ k → r k in R, and a substitution σ such that ℓ 1 σ = . . . = ℓ k σ.

Lemma 2. If a constructor theory E has no critical set of size

k + 1 with k ≥ 0 then it is k-blockable.
This lemma is a consequence of the proof of Proposition 1 (see [START_REF] Cortier | Bounding the number of agents, for equivalence too[END_REF]). From this lemma, we easily deduce that many theories used in practice to model security protocols are actually 1-blockable. This is the case of the theory E std and many variants of it. We may for instance add function symbols to model blind signatures, or zero-knowledge proofs.

Main result

We are now able to state our main reduction result.

Theorem 1. Let P , Q be two action-deterministic protocols built on a constructor theory E. If (P ; φ hd (n 0 ); 0) ≈ (Q; φ hd (n 0 ); 0) where n 0 = 2b(E) + 1 and b(E) is the blocking factor of E, we have that

(P ; φ hd (n); 0) ≈ (Q; φ hd (n); 0) for any n ≥ 0.
Moreover, when P and Q have only let construction with trivial else branches considering n 0 = b(E) + 1 is sufficient.

This theorem shows that whenever two protocols are not in trace equivalence, then they are already not in trace equivalence for a relatively small number of agents that does not depend on the protocols (but only on the underlying theory).

Example 12. Continuing our running example, thanks to Theorem 1, we only have to consider 4 agents (2 honest agents and 2 dishonest ones) for the theory E std introduced in Example 2, that corresponds to the standard primitives. Therefore we only have to perform the security analysis considering φ a (2)⊎φ h (2)⊎φ d (2) as initial frame.

This reduction result bounds a priori the number of agents involved in an attack. However, due to our setting, the resulting configurations are not written in their usual form (e.g. compromised keys are emitted through process K instead of being included in the initial frame). We show that it is possible to retrieve the equivalences written in a more usual form, after some clean-up transformations and some instantiations. This step is formalised in Proposition 2. We first define the notion of key generator process. The purpose of such a process is to provide long-term keys of compromised agents to the attacker.

Definition 9.

A key generator is an action-deterministic process K with no phase instruction in it. Moreover, for any n ∈ N, we assume that there exists φ K (n) with no occurrence of symbols in Σ ag , and such that:

-C n K = (K; φ hd (n); 0) tr = ⇒ (K ′ ; φ hd (n) ⊎ φ K (n); 0) for some tr and K ′ ; -img(φ) ⊆ img(φ K (n)) for any (P; φ hd (n) ⊎ φ; 0) reachable from C n K .
Such a frame φ K (n) is called a n-saturation of K, and its image, i.e. img(φ K (n)), is uniquely defined.

Intuitively, the attacker knowledge no longer grows once the frame φ K (n) has been reached. Then two processes P | K and Q | K are in trace equivalence for some initial knowledge φ hd (n 0 ) if, and only if, P ′ and Q ′ are in trace equivalence with an initial knowledge enriched with φ K (n 0 ) and P ′ and Q ′ are the instantiations of P and Q considering 2n 0 agents (n 0 honest agents and n 0 dishonest ones). Proposition 2. Consider 2n processes of the form (1 ≤ i ≤ n):

P ′ i =! new c ′ i .out(c i , c ′ i ).in(c ′ i , x 1 i (z 1 i )). . . . .in(c ′ i , x ki i (z ki i )).1: P i (z 1 i , . . . , z ki i ) Q ′ i =! new c ′ i .out(c i , c ′ i ).in(c ′ i , x 1 i (z 1 i )). . . . .in(c ′ i , x ki i (z ki i )).1: Q i (z 1 i , . . . , z ki i )
where each P i (resp. Q i ) is a basic process built on c ′ i , and x j i ∈ {ag, hon, dis} for any 1 ≤ j ≤ k i , and the c i for 1 ≤ i ≤ n are pairwise distinct. Moreover, we assume that ag, hon and dis do not occur in P i , Q i (1 ≤ i ≤ n). Let n 0 ∈ N, and K be a key generator such that fc(K) ∩ {c 1 , . . . , c n } = ∅. We have that:

(K ⊎ {P ′ i |1 ≤ i ≤ n}; φ hd (n 0 ); 0) ≈ (K ⊎ {Q ′ i |1 ≤ i ≤ n}; φ hd (n 0 ); 0) if,

and only if, (

n i=1 P i ; φ a (n 0 ) ⊎ φ K (n 0 ); 0) ≈ ( n i=1 Q i ; φ a (n 0 ) ⊎ φ K (n 0 ); 0)
where φ K (n 0 ) is a n-saturation of K, and

P i ={! new c ′ i .out(c i z 1 i ,...,z k i i , c ′ i ).1: P i (z 1 i , ..., z ki i )|x 1 i (z 1 i ), ..., x ki i (z ki i )∈img(φ hd (n 0 ))}; Q i ={! new c ′ i .out(c i z 1 i ,...,z k i i , c ′ i ).1: Q i (z 1 i , ..., z ki i )|x 1 i (z 1 i ), ..., x ki i (z ki i )∈img(φ hd (n 0 ))}.
Example 13. Using more conventional notations for agent names and after applying Proposition 2, we deduce the following equivalence: (P DS ⊎ P ′ 1 ; φ 0 ; 0) ≈ (P DS ⊎ P ′ 2 ; φ 0 ; 0) where

-φ 0 = {w a ⊲ a; w b ⊲ b; w c ⊲ c; w d ⊲ d; w kc ⊲ shk s (c); w kd ⊲ shk s (d)}; -P DS =    ! new c 1 .out(c A,zA,zB , c 1 ).P A (z A , z B ) z A , z B ∈ {a, b, c, d} | ! new c 2 .out(c B,zA,zB , c 2 ).P B (z A , z B ) | ! new c 3 .out(c S,zA,zB , c 3 ).P S (z A , z B )    -P ′ i = { ! new c ′ 2 .out(c ′ B,zA,zB , c ′ 2 ).P ′ i (z A , z B ) | z A , z B ∈ {a, b} }.
This corresponds to the standard scenario with 2 honest agents and 2 dishonest ones when assuming that agents may talk to themselves.

Sketch of proof of Theorem 1

First, thanks to the fact that we consider action-deterministic processes, we can restrict our attention to the study of the following notion of trace inclusion, and this is formally justified by the lemma stated below. Definition 10. Let C and C ′ be two configurations. We say that C is trace included in C ′ , written C ⊑ C ′ , if for every (tr, φ) ∈ trace(C), there exists (tr ′ , φ ′ ) ∈ trace(C ′ ) such that tr = tr ′ , and φ ⊑ s φ ′ . Lemma 3. Let C and C ′ be two action-deterministic configurations. We have C ≈ C ′ , if, and only if, C ⊑ C ′ and C ′ ⊑ C.

Given two action-deterministic configurations C and C ′ such that C ⊑ C ′ , a witness of non-inclusion is a trace tr for which there exists φ such that (tr, φ) ∈ trace(C) and:

either there does not exist φ ′ such that (tr, φ ′ ) ∈ trace(C ′ ) (intuitively, the trace tr cannot be executed in C ′ ); -or such a φ ′ exists and φ ⊑ s φ ′ (intuitively, the attacker can observe that a test succeeds in φ and fails in φ ′ ).

Second, we show that we can restrict our attention to witnesses of noninclusion that have a special shape: in case a constant from Σ error is emitted, this happens only at the very last step. In other words, this means that we may assume that the rule Let-Fail is applied at most once, at the end of the execution. More formally, a term t is Σ error -free if t does not contain any occurrence of error for any error ∈ Σ error . This notion is extended as expected to frames, and traces. Lemma 4. Let P and Q be two action-deterministic protocols, and φ 0 and ψ 0 be two frames that are Σ error -free. If (P ; φ 0 ; 0) ⊑ (Q; ψ 0 ; 0) then there exists a witness tr of this non-inclusion such that:

either tr is Σ error -free; -or tr is of the form tr ′ .out(c, error) with tr ′ Σ error -free and error ∈ Σ error .

This lemma relies on the fact that else branches are simple: at best they yield the emission of a constant in Σ error but they may not trigger any interesting process.

We can then prove our key result: it is possible to bound the number of agents needed for an attack. To formally state this proposition, we rely on the frame φ hd(n) as introduced in Definition 5. Theorem 1 then easily follows from Proposition 3. Proposition 3. Let E be a constructor theory, and P and Q be two actiondeterministic protocols such that (P ; φ hd (n); 0) ⊑ (Q; φ hd (n); 0) for some n ∈ N. We have that

(P ; φ hd (n)ρ; 0) ⊑ (Q; φ hd (n)ρ; 0) for some A-renaming ρ such that φ h (n)ρ (resp. φ d (n)ρ) contains at most 2b(E)+1
distinct agent names, and φ h (n)ρ and φ d (n)ρ do not share any name.

Proof. (sketch) Of course, when n ≤ 2b(E) + 1, the result is obvious. Otherwise, let tr be a witness of non-inclusion for (P ; φ hd (n); 0) ⊑ (Q; φ hd (n); 0). Thanks to Lemma 4, we can assume that tr is either Σ error -free or of the form tr ′ .out(c, error) for some error ∈ Σ error . This means that the trace tr can be executed from (P ; φ hd (n); 0) without using the rule Let-Fail at least up to its last visible action.

Considering a renaming ρ 0 that maps any honest agent name h to h 0 , and any dishonest agent name d to d 0 , we still have that the trace trρ 0 can be executed from (P ; φ hd (n)ρ 0 ; 0) at least up to its last visible action. Indeed, this renaming preserves equality tests and the property of being a message. Now, to ensure that the trace can still not be executed in the Q side (or maintaining the fact that the test under consideration still fails), we may need to maintain some disequalities, and actually at most b(E) agent names have to be kept unchanged for this (remember that our theory is b(E)-blockable). Moreover, in case P executes its else branch, we have also to maintain some disequalities from the P side, and again we need at most to preserve b(E) agent names for that. We do not know whether those names for which we have to maintain distinctness correspond to honest or dishonest agents, but in any case considering 2b(E) + 1 of each sort is sufficient.

⊓ ⊔

The following example illustrates why we may need 2b(E) + 1 agents of a particular sort (honest or dishonest) to carry out the proof as explained above.

Example 14. We also consider two constants error 1 , error 2 ∈ Σ error . In processes P and Q below, we omit the channel name for simplicity. We may assume that all input/outputs occur on a public channel c. P = in(hon(x 1 )).in(hon(x 2 )).in(hon(x 3 )).in(hon(x 4 )).let z 1 = eq(x 1 , x 2 ) in let z 2 = eq(x 3 , x 4 ) in 0 else out(error 1 ) else out(error 2 ) The process Q is as P after having swapped the two tests, and the two constants error 1 and error 2 .

Q = in(hon(x 1 )).in(hon(x 2 )).in(hon(x 3 )).in(hon(x 4 )).let z 1 = eq(x 3 , x 4 ) in let z 2 = eq(x 1 , x 2 ) in 0 else out(error 2 ) else out(error 1 ) We have that P ≈ Q. To see this, we may consider a trace where x 1 , x 2 , x 3 , and x 4 are instantiated using distinct agent names. However, any trace where x 1 = x 2 or x 3 = x 4 (or both), does not allow one to distinguish these two processes. It is thus important to block at least one agent name among x 1 , x 2 , and one among x 3 , x 4 . This will ensure that both P and Q trigger their first else branch. Then, the remaining agent names can be mapped to the same honest agent name. Thus, applying our proof technique we need b + b + 1 honest agent names (and here b = 1). Note however that a tighter bound may be found for this example since 2 distinct honest agent names are actually sufficient. Indeed, choosing x 1 = x 3 and x 2 = x 4 allows one to establish non-equivalence. But such a choice would not be found following our technique.

Actually, we can show that there is no attack that requires simultaneously 2b + 1 honest agents and 2b + 1 dishonest agents. We could elaborate a tighter bound, at the cost of having to check more equivalences.

Tightness of our hypothesis

Our class of protocols is somewhat limited in the sense that we consider processes that are action-deterministic, with simple else branches, and constructor theories. The counter-examples developed in this section actually suggest that our hypotheses are tight. We provide impossibility results for protocols in case any of our hypotheses is removed, that is, we provide counter-examples for processes with complex else branches, or non constructor theories, or non action-deterministic protocols.

Complex else branches

A natural extension is to consider processes with more expressive else branches. However, as soon as messages emitted in else branches may rely (directly or indirectly) on some agent names, this may impose some disequalities between arbitrary many agent names. This negative result already holds for the standard secrecy property expressed as a reachability requirement.

Formally, we show that we can associate, to any instance of PCP (Post Correspondance Problem), a process P (that uses only standard primitives) such that P reveals a secret s for n agents if, and only if, the corresponding PCP instance has a solution of length smaller than n. Therefore computing a bound for the number of agents needed to mount an attack is as difficult as computing a bound (regarding the length of its smallest solution) for the PCP instance under study. Computing such a bound is undecidable since otherwise we would get a decision procedure for the PCP problem by simply enumerating all the possible solutions until reaching the bound.

Property 1. There is an execution (P ; φ hd (n); 0) tr.out(c,w) = ===== ⇒ (P; φ ⊎ {w ⊲ s}; 0) if, and only if, the instance of PCP under study admits a solution of length at most n.

An instance of PCP over the alphabet A is given by two sets of tiles U

= {u i | 1 ≤ i ≤ n} and V = {v i | 1 ≤ i ≤ n} where u i , v i ∈ A * . A solution of PCP is a non-empty sequence i 1 , . . . , i p over {1, . . . , n} such that u i1 . . . u ip = v i1 . . . v ip .
Deciding whether an instance of PCP admits a solution is well-known to be undecidable, and thus there are instances for which a bound on the size of a solution is not computable. We describe here informally how to build our process P made of several parts. For the sake of clarity, we simply provide the informal rules of the protocol. It is then easy (but less readable) to write the corresponding process. First, following the construction proposed e.g. in [START_REF] Comon-Lundh | Security properties: Two agents are sufficient[END_REF], we write a process P PCP that builds and outputs all the terms of the form:

enc( u, v , ℓ , k)
where u = u i1 . . . u ip , v = v i1 . . . v ip , and ℓ is a list of agent names of length p that can be encoded using pairs. The key k is supposed to be unknown from the attacker. This can be easily done by considering rules of the form (where concatenation can be encoded using nested pairs): ag(z), enc( x, y , z ℓ , k) → enc( x.u i , y.v i , z, z ℓ , k) for any pair of tiles (u i , v i ). We then need to check whether a pair u, v embedded in the term enc( u, v , ℓ , k) is a solution of PCP. enc( x, x , z , k), enc(z, k diff ) → s Second, to build our counter-example, we write a process that relies on some else branches to ensure that a list ℓ is made of distinct elements. The idea is that enc(ℓ, k diff ) is emitted if, and only if, elements in ℓ are distinct agent names.

ag(x) → enc( x, ⊥ , k diff ) ag(x), ag(y), enc( x, z , k diff ), enc( y, z , k diff ) x =y ---→ enc( x, y, z , k diff )
The first rule allows us to generate list of length ---→ v is the informal description for the following process: on input u and if t 1 = t 2 then emit v. This can be encoded in our framework as explained in Section 2.3. The formalisation of these rules yields a process P that satisfies Property 1, and it is not difficult to write a proces P that satisfies in addition our actiondeterminisim condition. This encoding can be adapted to show a similar result regarding trace equivalence. We may also note that this encoding works if we consider an execution model in which agents are not authorised to talk to themselves. In such a case, we even do not need to rely explicitly on else branches.

Pure equational theories

We now show that it is actually impossible to bound the number of agents for non constructor theories. This impossibility result already holds for the standard equational theory E enc : dec(enc(x, y), y) = x.

To prove our result, given a list ℓ of pairs of agent names, we build two terms t P (ℓ) and t Q (ℓ) using the function symbols enc, dec, the public constant c 0 , and some agent names a 1 , . . . , a n in A. The terms t P (ℓ) and t Q (ℓ) are such that they are equal as soon as two agent names of a pair in ℓ are identical.

Property 2. The terms t P (ℓ) and t Q (ℓ) are equal modulo E enc if, and only if, there exists a pair (a, b) in ℓ such that a = b.

The terms t P (ℓ) and t Q (ℓ) are defined inductively as follows:

-t P (ℓ) = dec(enc(c 0 , a), b) and t Q (ℓ) = dec(enc(c 0 , b), a) when ℓ = [(a, b)]; -In case ℓ = (a, b) :: ℓ ′ with ℓ ′ non
-empty, we have that t X (ℓ) = dec(enc(c 0 , dec(enc(a, t 1 ), t 2 )), dec(enc(b, t 1 ), t 2 ))

where m, t 1 and t 2 are such that t X (ℓ ′ ) = dec(enc(c 0 , t 1 ), t 2 ) and X ∈ {P, Q}.

For illustration purposes, the term t P (ℓ 0 ) for ℓ 0 = [(a 2 , a 3 ), (a 1 , a 3 ), (a 1 , a 2 )] is depicted below. A subtree whose root is labelled with n having subtrees t 1 and t 2 as children represents the term dec(enc(n, t 1 ), t 2 ). The term t Q (ℓ 0 ) is the same as t P (ℓ 0 ) after permutation of the labels on the leaves. a 1 a 2 a 1 a 2 a 1 a 2 a 1 a 2 a 1 a 3 a 1 a 3 a 2 a 3 c 0 First, we may note that t P (ℓ 0 ) = t Q (ℓ 0 ) when a 1 = a 2 . Now, in case a 1 = a 3 , we obtain t P (ℓ 0 ) = t Q (ℓ 0 ) = dec(enc(c 0 , a 2 ), a 3 ), and we have that t P (ℓ 0 ) = t Q (ℓ 0 ) = c 0 when a 2 = a 3 . These are the only cases where t P (ℓ 0 ) and t Q (ℓ 0 ) are equal modulo E enc . More generally, we can show that t P (ℓ) and t Q (ℓ) enjoy Property 2. Now we may rely on these terms to build two processes P n and Q n such that (P n ; φ hd (n 0 ); 0) ≈ (Q n ; φ hd (n 0 ); 0) if, and only if, n 0 ≥ n. These processes are as follows:

P n = in(c, ag(z 1 )) . . . in(c, ag(z n )).out(c, t P (ℓ)) Q n = in(c, ag(z 1 )) . . . in(c, ag(z n )).out(c, t Q (ℓ))

Proof sketch. (⇐) if PCP has a solution of length at most n, it is possible to build the term enc( u, v , ℓ , k) corresponding to this solution with u = v and ℓ of length at most n. Moreover, we can assume that ℓ is made of distinct elements. Hence, the additional rules in Q will not be really useful to generate a certificate on the list ℓ with the flag set to no. Actually, only enc( yes, ℓ , k check ) will be generated, and thus P will emit ok and Q will not be able to mimic this step.

(⇒) Now, if PCP has no solution of length at most n, then either PCP has no solution at all, and in such a case, the part where P and Q differ is not reachable, and thus the processes are in trace equivalence. Now, assuming that PCP has a solution of length n ′ with n ′ > n, the only possibility to distinguish P from Q is to build the term enc( yes, ℓ , k check ) with ℓ of length n ′ . This term will allow us to trigger the rule (1) in P but not in Q. The problem is that ℓ contains a duplicate entry, and due to this, at some point it would be possible to mimic what is done in P using rule (3) with the additional rule (3a), and to pursue the construction of this certificate relying on (3b) and (3c). This will allow Q to go through the rule (1) as P did. ⊓ ⊔

Conclusion

We have shown that we can bound the number of agents for a large class of protocols: action-deterministic processes with simple else branches and constructor theories, which encompasses many primitives. The resulting bound is rather small in general. For example, 4 agents are sufficient for standard primitives and processes without else branches. Our assumptions are rather tight. Surprisingly, such a reduction result does not hold in case processes are not actiondeterministic, or if they include more complex else branches, or else for more general equational theories. This draws a thin line between our result (where terms with destructors may not be sent) and a more general framework. Our result applies for any equivalence between two processes. This allows us to cover various security properties such as strong secrecy or anonymity. However, assuming deterministic processes discards the encoding of some properties such as unlinkability. We devise in [START_REF] Cortier | Bounding the number of agents, for equivalence too[END_REF] an alternative encoding to check for unlinkability in our framework, considering only deterministic processes.

Our reduction result enlarges the scope of some existing decidability results. For example, [START_REF] Chrétien | From security protocols to pushdown automata[END_REF] provides a decision procedure for an unbounded number of sessions, for processes that use at most one variable per rule. In case an arbitrary number of agents is considered, one or two variables are typically used simply to describe the agents. Bounding the number of agents is therefore needed to consider non trivial protocols.

The proof of our reduction result is inspired from [START_REF] Chrétien | Checking trace equivalence: How to get rid of nonces[END_REF], which shows how to bound the number of nonces. Taking advantage of the properties of agent names, we extend [START_REF] Chrétien | Checking trace equivalence: How to get rid of nonces[END_REF] to processes with simple else branches, action-determinism and general constructor theories. As future work, we plan to study how to generalize both results in a framework that would allow to bound several types of data.

Fig. 1 .

 1 Fig. 1. Semantics for processes

  1 whereas the second rule gives us the possibility to build list of greater length, like [a 1 , a 2 , . . . , a n ] as soon as the sublists [a 1 , a 3 , . . . , a n ] and [a 2 , a 3 , . . . , a n ] have been checked, and a 1 and a 2

	are distinct agent names. The rule u	t1 =t2

⋆ The research leading to these results has received funding from the European Research Council under the European Union's Seventh Framework Programme (FP7/2007-2013) / ERC grant agreement n • 258865, project ProSecure, the ANR project JCJC VIP n o 11 JS02 006 01, and the DGA.

where ℓ is a list of length n(n -1)/2 which contains all the pairs of the form (z i , z j ) with i < j.

Note that in case n 0 < n, in any execution, we are thus forced to use twice the same agent names, and thus the resulting instances of t P (ℓ) and t Q (ℓ) will be equal modulo E enc . In case we have sufficiently many distinct agent names, the resulting instances of t P (ℓ) and t Q (ℓ) will correspond to distinct public terms. Hence, in such a case trace equivalence does not hold.

Note that, for sake of simplicity, our encoding directly relies on the agent names, but a similar encoding can be done using for instance shk s (a) instead of a so that agent names will not be used in key position.

Beyond action-deterministic processes

Another natural extension is to get rid of the action-determinism condition, or at least to weaken it in order to consider processes that are determinate (as defined e.g. in [START_REF] Chadha | Automated verification of equivalence properties of cryptographic protocols[END_REF]). This is actually not possible. The encoding is quite similar to the one presented in Section 4.1. Since we have no easy way to ensure that all the terms of the form enc(ℓ, k diff ) will contain distinct elements, the encoding is more involved.

To prove our result, we show that given an instance of PCP, it is possible to build two processes P and Q (that use only standard primitives and no else branch) that are in equivalence for n agents if, and only if, the corresponding PCP instance has a solution of length at most n. Property 3. (P ; φ hd (n); 0) ≈ (Q; φ hd (n); 0) if, and only if, the instance of PCP under study admits a solution of length at most n.

Our process P is quite similar to the one described in Section 4.1. Note that the test x = y has been removed, and a public constant yes has been added inside each encryption. The presence of such a constant is not mandatory when defining P but will become useful when defining Q. enc( x, x , z , k), enc( z b , z , k check )

ag(x), ag(y), enc( z b , x, z , k check ), ---→ enc( yes, x, y, z , k check ) (3) enc( z ′ b , y, z , k check ) Then, Q is quite similar except that we replace the test z b = yes by z b = no and we consider in addition three other versions of the last protocol rule (rule (3)) giving us a way to generate encryption containing the flag no. More precisely, we consider the following rule with ϕ equal to x = y (rule 3a), z b = no (rule 3b), and z ′ b = no (rule 3c). ag(x), ag(y), enc( z b , x, z , k check ), ϕ -→ enc( no, x, y, z , k check ) enc( z ′ b , y, z , k check ) Putting all these rules together and considering randomised encryption to avoid spurious equalities to happen, this yields two processes P and Q that actually satisfy Property 3.


Dragos Dancila
email: dragos.dancila@angstrom.uu.se

Václav Valenta

Alina-Cristina Bunea

Dan Neculoiu

Hermann Schumacher

Anders Rydberg

Differential Microstrip Patch Antenna as Feeder of a Hyper-Hemispherical Lens for F-Band MIMO Radars

Keywords: millimeter wave (mm-wave), differential microstrip patch antenna (DMPA), 3D printing, polyamide lens. I

In this paper, a novel differential microstrip patch antenna (DMPA) is designed and used to feed a lens antenna for short range F-band MIMO radars. The DMPA is fed differentially by a pair of coupled lines. The antenna is connected via a differential impedance matching network to the differential output of the modules, eliminating this way the need of a balun in the RF frontend. The simulated antenna gain is about 8 dBi and bandwidth (S11 < -10 dB) is between 125 -137 GHz. Preliminary experimental measurements are shown using Transmit/Receive modules in 0.13 m SiGe:C BiCMOS technology, hybrid connected using wirebonding to off chip DMPAs. It is shown by the transmission link evaluation that the gain is increased by about 15 dBi adding a 10 mm radius 3D printed polyamide lens in the near field of the DMPA.

INTRODUCTION

Short-range F-band radar systems based on Transmit-Receive (TR) MMIC modules are for instance provided with differential output-inputs. Such modules, implemented in standard SiGe processes using BiCMOS technologies and fast Heterojunction Bipolar Transistors (HBTs) with fmax values of 500 GHz allow the spread of millimeter-wave imaging and radar systems technology [START_REF] Schumacher | Smarter ICs[END_REF]. Having the flexibility to operate the TR IC as a transmitter or a receiver is of a great interest for Multiple-Input-Multiple-Output (MIMO) systems and could be implemented on-chip using RF-MEMS [START_REF] Spreng | Wideband 120 GHz to 140 GHz MIMO radar: System design and imaging results[END_REF]. The question of on-chip antenna vs. off-chip hybrid integration is often raised and recent empirical developments have demonstrated the viability of hybrid integration above 100 GHz, provided a compensation of bondwire interconnects [START_REF] Valenta | Design and Experimental Evaluation of Compensated Bondwire Interconnects above 100 GHz[END_REF]. At the same time, the hybrid integration allows for instance using large 3D printed lenses for beam focusing. On the other hand, the antenna design should accommodate MMIC's differential interfaces and a traditional solution is the implementation of baluns, while the conventional antennas are of single-ended type. Therefore, research on differential antennas has become more and more attractive recently [START_REF] Zhang | Theory and analysis of differentially-driven microstrip antennas[END_REF].

In this paper, a novel differential microstrip patch antenna (DMPA) is designed and used to feed a lens antenna for short range F-band MIMO radars. The DMPA is using a differential pair of coupled lines wirebonded to the MMIC and compensation structures. It is shown, by the transmission link evaluation that the gain is increased by about 15 dB adding a 10 mm radius 3D printed polyamide hyper-hemispherical lens in the near field of the DMPA. A manufactured TR module at 130 GHz implementing a differential microstrip patch antenna to feed a hyper-hemispherical lens antenna is shown in Fig. 1 Fig. 1: One of the manufactured TR modules with a hyperhemispherical lens placed above the differential patch.

II. ANTENNA DESIGN

A broadside differential patch antenna was designed using the HFSS software. The simulation set-up comprises a port exciting both a differential mode with a characteristic impedance of 100 Ohm and a common mode of 25 Ohm, using driven terminal simulations with HFSS. The substrate used is RO3003 with thickness, h = 127 m, a relative permittivity r = 3 and loss tangent, tan = 0.0013. Following [START_REF] Balanis | Antenna Theory: Analysis and Design[END_REF], the initial design starts with the width, w a :

where c is the speed of light and f is the centre frequency. The length, l a can be calculated as:

with eff as the effective permittivity and as the relative wavelength. A differential feeding with 100 Ohm transmission lines with l l = 700 m, s l = 100 m and w l = 200 m is implemented. A quarter-wavelength matching network is designed as in [START_REF] Tong | A Novel Differential Microstrip Patch Antenna and Array at 79 GHz[END_REF], with l m = 520 m, w m = 100 m and s m = 300 m. After optimization, the differential patch antenna dimensions are calculated as follows: l a = 745 m and w a = 545 m. The layout of the differential patch antenna designed for a central frequency of 130 GHz is presented Fig. 2. The antenna impedance with and without matching (corresponding to m1 and m2 frequency points at 130 GHz, respectively) are presented in Fig. 3, for the frequency range 120-140 GHz. The matching network is designed between the antenna patch and the 100 Ohm differential feed line. The matching network consists of a quarter-wavelength coupled lines and converts the antenna impedance from a slightly inductive part in the Smith chart (m2 in Fig. 3) to the 100 Ohm differential impedance (m1 in Fig. 3). The resulting optimised matching is broadband (S 11 <-10dB) between 125-137 GHz, see Fig. 4. The radiation pattern is broadside and shows a max gain of 8 dBi, as can seen Fig. 5.

III. LENS DESIGN

The millimeter wave lens was manufactured using a selective laser sintering printing process for 3D printing of polyamide ( r =3.3). The lens was integrated in a package and at a certain optimized distance (d = 2.75 mm) above the differential patch antenna. The hyper-hemispherical lens has an extension of 1.5 x R where R= 10 mm is the radius of the lens. The near fields around the differential microstrip patch antenna, feeding the hemispherical lens are presented Fig. 6. In Fig. 7, the directivity of the off-chip antennas is increased by about 13.5 dB in simulations, using the hyper-hemispherical polyamide lens, with a radius of 10 mm, placed at 2.75 mm distance from the patch antenna. More details on the design and fabrication of the hemispherical lens could be found in [START_REF] Tong | A Novel Differential Microstrip Patch Antenna and Array at 79 GHz[END_REF].

IV. SYSTEM DESCRIPTION

A block diagram of the TR module is shown in Fig. 8 and a photograph of the fabricated IC is presented in Fig. 9. The TR module can be configured either as a transmitter or a receiver. Therefore, for single-channel radar measurements, two modules are required. Having the flexibility to operate the TR IC as a transmitter or a receiver is of a great interest for Multiple-Input-Multiple-Output (MIMO) systems where different virtual arrays configurations can be arranged [START_REF] Valenta | High Performance Transmit/Receive Modules in 0.13 m SiGe:C BiCMOS for Short Range F-band MIMO Radars[END_REF]. The whole module consists of a TR IC glued into a cavity in a customized board with a differentially fed off-chip end-fire patch antenna, connected to the TR IC using wire bonding. To overcome losses caused by the bondwire interconnects a dedicated compensation structure developed by the authors is used [START_REF] Valenta | Experimental Evaluation of Differential Chip-to-Antenna Bondwire Interconnects above 100 GHz[END_REF]. The TR IC uses frequency multipliers to translate the MIMO radars' specific Frequency-Modulated-Continuous-Wave (FMCW) LO signal from X-band to F-Band. The same multiplying topology is used for the down-conversion.

V. EXPERIMENTAL RESULTS

Two TR ICs were hybrid connected using wirebonding to the differential antenna: ICs realized in SG13S technology (f t /f max =250/300 GHz) were packaged into customized boards made of three separate PCBs. The bottom PCB is FR4 and contains all bonding pads and routing for DC, IF, digital control and ESD protection. The second board is a 130 m thick RO3003 with 9 m Cu cladding, suitable for fabrication of fine off-chip structures (antenna and bondwire compensation). The input LO feed is made on a separate RO3003. Fig. 10 shows a cross-section and a photograph of the realized module. In the experiment, two TR modules were arranged in a bidirectional 0.5 m wireless link. Two independent LO signals with offset of 1 MHz were swept from 13.75 to 17.5 GHz (i.e. 110 to 140 GHz at the wireless interface) and fed to the modules to create an IF tone exactly at 8 MHz. While sweeping the LOs, the resulting 8 MHz IF was recorded at the mixer's output (before the off-chip op-amps). Frequency responses for SG13S TR modules are shown in Fig. 11.

VI. CONCLUSIONS

A differential microstrip patch antenna was wirebond connected to SiGe BiCMOS TR modules, demonstrating a 0.5 m wireless link between 120-140 GHz. By simulations, a gain increase of about 13.5 dB is obtained using a hyperhemispherical lens with a radius of 10 mm and placed optimally above the patch antenna. Experimental results using two TR modules show that the gain is increased by about 15 dB, adding a 10 mm radius 3D printed polyamide lens above the differential patch antenna. The overall link budget is therefore improved by about 30 dB, demonstrating the very high directivity of this solution.

Fig. 2 :

 2 Fig. 2: Layout of the differential patch antenna at 130 GHz.

Fig. 3 :

 3 Fig. 3: Antenna impedance with and without matching (m1 and m2 frequency points at 130 GHz, respectively) in the frequency range 120-140 GHz.

Fig. 4 :

 4 Fig. 4: Design matching (S11< -10dB) is between 125-137 GHz

Fig. 5 :

 5 Fig. 5: Far field radiation of the differential patch antenna at 130 GHz. The maximum gain is 8 dBi.

Fig. 6 :

 6 Fig. 6: Fields around the differential microstrip patch antenna, feeding the hemispherical lens (scale: 0 to Emax= 100 V/m).

7 :

 7 Far fields of the differential patch antenna with hyperhemispherical lens at 130 GHz. The maximum gain is 21.5 dBi.

Fig. 8 :Fig. 9 :

 89 Fig. 8: A block diagram of the Tx and Rx modules used for evaluation of Tx and Rx ICs

Fig. 10 :

 10 Fig. 10: A cross-section and a photograph of the realized TR IC module. Differential end-fire antenna, bondwire interconnect compensation elements and the LO feed line on RO3003.

Fig. 11 :

 11 Fig. 11: Frequency responses for a 0.5 m wireless link (left). Note the wide bandwidth (>20 GHz) of the wire-bonded 13S modules.

Global Symposium on Millimeter Waves (GSMM) & ESA Workshop on Millimetre-Wave Technology and Applications

ACKNOWLEDGEMENTS This work is supported by the EU project NANOTEC (FP7-ICT-2011-7). The authors wish to acknowledge Dr. M. Kaynak from IHP GmbH and Dr. W. Winkler from Silicon Radar GmbH. A.C. Bunea and D. Neculoiu would like to thank Mr. Victor Moagar-Poladian and Dr. Gabriel Moagar-Poladian for manufacturing the 3D printed lens, for useful discussions regarding the 3D printing process and acknowledge the support of the Romanian Ministry of National Education and Research, under the project no. PN-IIID-PCE-2011-3-0830.


Dr Pascal Willis

PhD; Bruce J Haines

PhD Da Kuang

PSD1 -Satellite Dynamics: Meeting the Challenges of Positioning on Giga-to-Nanometer Scales

Keywords: DORIS, GPS, antenna phase center, Terrestrial Reference Frame, geocenter

We analyzed one year of DORIS data to estimate daily corrections to the mean locations of the satellite antenna phase centers. For each DORIS satellite, we looked for possible biases, discontinuities, trends or annual signals. All SPOT satellites show very similar patterns, which are characterized by a significant constant bias of about 20 mm in the cross-track direction as well as a clear annual signal of 5 mm amplitude. All DORIS satellites show a consistent systematic radial offset of 10 to 20 mm (equivalent to 1.5 to 3.0 ppb in the Terrestrial Reference Frame) when using ITRF2000. However, this bias mostly disappears with the adoption of ITRF2005P. A discontinuity appears in DORIS radial antenna phase center offset of the ENVISAT satellite on October 12, 2004, at the time of a flight software switch. GPS phase center offsets were also computed for Jason and TOPEX/Poseidon and compared to the corresponding DORIS estimates.

Significant differences were found between DORIS and GPS estimations. Finally, we applied these estimated DORIS satellite antenna phase center offsets to derive weekly time series of station coordinates in 2004. Results showed very small improvement for station coordinates and confirmed that DORIS scale could match ITRF2000 scale by modifying the vector between the center of mass of the satellite and the phase center of the on-board antenna with a constant radial offset. We do not recommend the adoption of any empirical DORIS satellite phase center offsets at this point

Introduction

DORIS (Doppler Orbit Determination and Radiopositioning on Satellite

) is a French tracking system initially designed for precise tracking of low-earth orbiting satellites (Willis et al., in press,a). It is an uplink Doppler system with a dense tracking network (Fagard, in press), allowing almost continuous observation for satellites above 800 km altitude. Recently, following the example of the International GNSS Service (IGS) (Beutler et al., 2002), an International DORIS Service (IDS) was created (Tavernier et al., in press).

The current accuracies of space geodetic products are usually altered by many systematic errors. Within the GPS community, several studies have been conducted to estimate antenna corrections in order to decrease possible systematic errors. These corrections can be expressed in terms of mean phase-center offsets for both ground and satellite antennas (e.g., [START_REF] Mader | The Block IIA satellite, Calibrating Antenna Phase Centers[END_REF]. A more comprehensive approach is to use antenna phase-center variations (PCV) models, which provide estimates of the PCV Manuscript as a function of elevation and azimuth, seen by the antenna ground station or by the satellite antenna [START_REF] Rothacher | Combination of absolute and relative antenna phase center variations[END_REF]Schmidt and Rothacher, 2003;[START_REF] Haines | GPS satellite antenna phase center variations, New perspectives from the GRACE mission[END_REF]. Similar investigations have not been carried out yet on a systematic basis for DORIS. Willis et al. (2005b), however, did estimate DORIS satellite antenna maps that described corrections to the Doppler measurements as a function of elevation and azimuth.

Recent studies (Willis et al., in press, b) indicate that the scale of the Terrestrial Reference Frame (TRF) derived solely from DORIS (equivalent to a constant error in height of all DORIS station coordinates) is biased by a few parts per billion (ppb) with respect to the scale of ITRF2000 [START_REF] Altamimi | A new release of the International Terrestrial Reference Frame for Earth science applications[END_REF]. By estimating the radial offset between the center of mass (CM) of the satellite and the center of phase of the DORIS antenna, this systematic scale error could be significantly reduced or eliminated. It should be noted that the success of this approach depends to a large extent on the accuracy of the modeled location of the CM in the body-fixed s/c frame. A time-dependent model for the migration of the center of mass of the SPOT satellites (as fuel is consumed) is not presently available. Such information is provided for all other DORIS satellites (TOPEX/Poseidon, Jason and ENVISAT) but not for the SPOT, for which only a constant value of this vector is provided by CNES (French Space Agency) to the IDS users.

The goals of this paper are: to estimate for all DORIS satellites empirical phase center offsets in the three directions (body-fixed frame); to compare these results with similar results obtained from GPS data when available (TOPEX/Poseidon and Jason); and finally, to test if reprocessing with these empirical offsets provides some improvement, either in terms of Terrestrial Reference Frame (geocenter and scale) or in terms of station coordinate precision.

Description of the method

We chose to analyze data from one full year of DORIS data in order to get reliable results. We selected the year 2004, as it is the last year for DORIS/TOPEX data. Represented in this year are data from as many as 6 satellites (Table 1). Of all possible DORIS satellites, only SPOT-3 was not studied because data are only available from 1996 to 1998.

(Table 1) DORIS orbit solutions were computed on a daily basis independently for each satellite. Station coordinates were fixed to our latest cumulative solution IGN04D02 (Willis et al., 2005a). This solution is based on more than 12 years of DORIS data and provides a precise position and velocity for each tracking station. The frame was a posteriori aligned to ITRF2000 [START_REF] Altamimi | A new release of the International Terrestrial Reference Frame for Earth science applications[END_REF] using a conformal 14-parameter transformation. When fixing station coordinates to a standard frame such as ITRF2000, it is advisable to use an internal solution, such as IGN04D02, established using more data, adding the most recent stations as well. This approach also accounts for the stationrelated problems that were not known at the time of computation of the ITRF2000 [START_REF] Willis | Defining a DORIS core network for Jason-1 precise orbit determination based on ITRF2000[END_REF].

The DORIS data were processed with the GIPSY/OASIS II software, using the latest analysis strategy and the latest models, including a recent GRACE-derived gravity field GGM01C [START_REF] Tapley | The Gravity Recovery and Climate Experiment, Mission Overview and Early Results[END_REF] up to degree and order 120 as it provided a significant improvement in DORIS station positioning accuracy as measured externally by GPS [START_REF] Willis | External validation of the GRACE GGM01C gravity field using GPS and DORIS positioning resul, ts[END_REF].

Estimating DORIS phase center offsets

2.1 SPOT results Figure 1 displays an example of such results in the case of all three SPOT satellites for the radial component ( pointing opposite to the Earth).

(Figure 1)

Figure 1 shows that all SPOT satellite estimates present a common systematic bias of about 15 mm in the zenith direction (away from the Earth). All results are also affected by a clear annual signal of about 5 mm amplitude: 5.5 mm for SPOT-2, 4.3 mm for SPOT-4 and 5.4 for SPOT-5. The exact causes of these temporal variations are still unknown. In our opinion, they could be related to mis-modeling in the solar pressure or albedo acceleration or to remaining errors in tropospheric or ionospheric corrections.

However, the explanation of the bias itself is consistent with the fact that the IGN/JPL (Institut Geographique National/Jet Propulsion Laboratory) station coordinates solutions all suffer from a constant bias of about -2.5 ppb, equivalent to -16 mm in station height, relative to ITRF2000 (Willis et al.; in press, b). Our own solution is consistent with the DORIS measurements and to the systematic error present in our analysis. When we force the station coordinates to be aligned on ITRF2000 (being pushed up in the direction of the satellite), we need to compensate this error in our computation. As the position of the center of mass will remain the same (the semi-major axis remains the same, as the time definition is not changed, through the 3 rd Keper's law), one way to compensate these errors, is to push the satellite antenna upward, so that the distances (through the Doppler measurements) remain the same. We should then estimate a positive vector offset (from satellite center of mass to the antenna phase center), in the radial component (opposite to the Earth).

We extended this study by estimating this antenna phase center offset, only in the case of the SPOT-2 satellite, using the preliminary ITRF2005P solution [START_REF] Altamimi | Terrestrial reference frame requirements within GGOS perspective[END_REF] instead of the older ITRF2000.

(Figure 2) It can be seen in Figure 2 that the estimated radial offset is quite different when fixing station coordinates to ITRF2000 or to ITRF2005P (a preliminary version of ITRF2005 that was distributed to small validation group for test purposes in May 2006). The offset estimated using ITRF20005P coordinates gets closer to zero: the mean value over 2004 is 19 mm for ITRF2000 and only 10 mm for ITRF2005P. This is consistent with the fact the DORIS TRF scale of our IGN/JPL station coordinates solutions is more consistent with ITRF2005P (-0.7 ppb) than with ITRF2000 (-2.5 ppb). If the ITRFs scales based on VLBI and Laser results can show these large differences on the DORIS subnetwork, it seems rather risky to estimate such a radial offset using a specific ITRF. First, the derived DORIS TRF scale would lose all physical meaning. Secondly, the DORIS solutions would only be compatible with the current ITRF (used to derived these satellite antenna offsets) but not with the future ITRFs.

ENVISAT

All estimated phase center corrections showed some small offsets and small annual signal. Only one of the DORIS satellites also showed a clear discontinuity in the estimated radial offset. Figure 3 shows that a discontinuity can be found for ENVISAT on October 12, 2004.

(Figure 3) It is intriguing that this discontinuity occurs at the exact time of the in-flight update of the ENVISAT DORIS software. The reason for that is still unknown, but other analysis (Doornbos and Willis, in press) using results from all ACs showed that a different signature could be found in the DORIS residuals after this software change. In this study, ENVISAT data were processed using the attitude model (instead of using the DORIS phase center correction proposed by CNES in the data files) as well as the most recent solar pressure model [START_REF] Sibthorpe | Precision non-conservative force modeling for Low Earth Orbiting spacecraft[END_REF].

Synthesis of results

Table 2 presents a synthesis of the mean values of these phase center offsets for all satellites. For non-yawing satellite, the X represents the along-track component (in the direction of the velocity), the Y represents the cross-track component (right direction) and the R represents the radial direction (opposite to the Earth). For the other satellites (TOPEX/Poseidon and Jason), X and Y are defined in the s/c body frame. Due to the changes in attitude of the model, these do not have a meaningful interpretation in the velocity or cross-track direction. For Topex/Poseidon and Jason, R represents also the radial direction (opposite to the Earth).

(Table 2)

For non-yawing satellites (SPOTs and ENVISAT), the along-track offset is not observable (noted as N/A in Table 2).

All estimated radial corrections are positive in the direction opposite to the Earth so the estimation tries to put the antenna farther from the Earth. This is compatible with the fact that the DORIS IGN/JPL TRF scale is negative (-2.5 ppb) when compared to ITRF2000. When fixing DORIS station coordinates to ITRF2000 (going up), the estimation tries to find a way to put the satellite farther from the Earth, in order to keep the measurements constant (basically distances from ground stations to satellite, and in the case of DORIS difference in time of such distances). Previous analysis showed that other DORIS Analysis Center find a different TRF scale for each satellite (Willis et al., in press, b).

The DORIS/Jason data are affected by an abnormal acceleration of the on-board clock over the South Atlantic Anomaly (SAA) due to an extreme sensitivity to radiation (Willis et al., 2004). In this investigation, we did not use the recent correction model developed by Lemoine and Capdeville (in press), but we disregarded any data from ground stations located nearby the SAA. This could probably explain the larger radial offset found for this specific satellite as the global effect is not properly addressed in a proper way. All other DORIS satellite show a common bias of about 16 mm opposite to the Earth. This is equivalent to a 2.5 ppb error in the TRF scale at this altitude.

The estimated cross-track vectors are also at the same level (under 20 mm). As discussed by Willis et al., 2006, errors in this component could dissipate in error in TZgeocenter component with an amplification factor of 6.5 for the SPOT non-yawing sunsynchronous satellites.

GPS phase center offsets

Estimating GPS phase center offset for Jason and TOPEX/Poseidon

Estimation of the phase-center location has long been a standard approach for diagnosing possible scale errors in the GPS measurement system (e.g., [START_REF] Bertiger | GPS precise tracking of TOPEX/Poseidon, Results and implications[END_REF]. Of the DORIS missions considered in this paper, two of them -TOPEX/Poseidon (T/P) and Jason-1 -also carried precise GPS receivers. [START_REF] Haines | Initial orbit determination results for Jason-1, Towards a 1-cm orbit[END_REF] reported GPS-derived phase-center offsets for the Jason-1 mission. These results, however, were based on the prevailing GIPSY/OASIS II (GOA-II) software standards for the locations of the phase center of the transmitters on the GPS satellites. We present herein results based on our new GRACE-based transmitter phasecenter variation (PCV) maps [START_REF] Haines | GPS satellite antenna phase center variations, New perspectives from the GRACE mission[END_REF]. For the Jason-1 antenna, we used alternatively the pre-launch anechoic PCV map (Figure 4) or a map derived empirically from in-flight data (Figure 5). While the boresite of the Jason-1 GPS antenna is canted 30° from zenith, the daily estimates depicted in the Figure are expressed in the Jason s/c body-fixed frame, with the vertical (R) component of the phase center expressed as positive in the zenith direction.

(Figures 4 and5) Evident in the time series (Figure 4) is a dependence on the yaw regime of the satellite, which is dictated by the variation of the β' angle (~117-d period). Note that fixed-yaw periods are excluded from the time series since the X axis of the s/c aligns with the along-track component of the orbit, and the corresponding X offset cannot be distinguished from timing/orbit errors. The average offset corrections in the X, Y and Z s/c directions (with sample standard deviations) are respectively -0.4 ± 1.4 cm, -0.4 ± 2.0 cm and -1.6 ± 0.5 cm. With the exception of the Z component, the estimated location of the Jason-1 GPS phase center is within a few mm of the model. The source of the small remaining Z bias (-1.6 cm) is not presently known, but multipath reflections off the Jason s/c could certainly contribute at this level. Of course, we cannot rule out some contribution from a scale error in the adopted reference frame (IGS derivative of ITRF2000) as manifest in the GPS spacecraft orbit and clock products used in computing the Jason-1 orbit. As expected, use of the empirical antenna map reduces this Z bias to insignificance (Figure 5). The RMS phase-center variation (LC) explained by the empirical map is ~1 cm, and reflects principally the combination of intrinsic antenna PCV and multipath. The aggregate effect of multipath is expected to vary with β' angle because different portions of the canted Jason antenna are sampled depending upon the yaw attitude of the spacecraft.

Published estimates of the T/P phase-center offset [START_REF] Bertiger | GPS precise tracking of TOPEX/Poseidon, Results and implications[END_REF] were based on dual-frequency data collected early in the mission. With the routine activation of Anti-spoofing (AS) in January, 1994, the older GPS Demonstration Receiver (GPSDR) design operated on a single frequency (L1) only. Figure 6 depicts daily estimates of the T/P GPS phase-center offset (L1) for the 2004 timeframe considered in the present study. While the ionosphere delay was modeled using the approach described by [START_REF] Lough | Precise orbit determination for low-Earth orbiting satellites using GPS data, Recent results[END_REF], there remain significant errors compared to the dual-frequency approach wherein the delay is fully removed to first order. Further complicating the interpretation of these results is the absence of L1 PCV maps for the GPS transmitters. (The GRACE-based maps adopted for this study were constructed from LC phase data, and the L1 phase center could depart significantly from its ionosphere-free counterpart.) Despite these caveats, the estimated T/P phase-center offsets show good stability. The estimates X and Y offset corrections are centered close to zero while the radial (R) offset averages 20 cm. The principal effect of the mismodeled ionosphere and GPS s/c L1 phase-center location is expected to be in the vertical (Z).

Applying DORIS phase center offsets

Method used

We recomputed DORIS weekly solutions of stations coordinates and daily Earth Orientation Parameters (EOPs) after adopting the estimated phase center corrections derived earlier (Table 2). These solutions were obtained in a real multi-satellite adjustment at the data level [START_REF] Willis | TOPEX/Jason combined GPS/DORIS orbit determination in the tandem phase[END_REF]. We did not add up normal matrices from individual satellite solutions as it looses some information when some common parameters are eliminated beforehand, such as vertical tropospheric corrections and station clocks. It is very easy with the GIPSY/OASIS II software to process data with or without an additional empirical phase center correction. Only one Fortran namelist needs to be changed, insuring that DORIS data will be processed exactly in the same manner, except for this additional correction. To avoid problems related to the SAA, no DORIS/Jason data were used in the estimation, as it is currently the case for the IGN/JPL operational DORIS solutions to IDS.

Terrestrial Reference Frame parameters

We did not notice any significant differences in the estimated geocenter variation, even in the TZ-component. Results are indistinguishable. However, the TRF scale decreased as expected from a mean value of almost -2.5 ppb to almost 0.

Station coordinates

As shown in Table 3, station coordinates results improved only marginally, when compared to the DORIS cumulative solution IGN04D02 (Willis et al., 2005a).

(Table 3) In our opinion, this shows that most of the estimated DORIS phase correction absorbs systematic errors coming from some other source. It does not seem reasonable at this point to suggest the adoption of any empirical correction of this type as it does not really seem to provide much better geodetic results.

It could be worthwhile for IDS to launch an evaluation study, asking each DORIS AC to derive similar results, using their own software and analysis strategy. In our opinion, this could help us distinguish between technique-related and software-related systematic errors.

Conclusions

In conclusion, we estimated mean values of phase center variations for all DORIS antennas as well as for all GPS antennas on satellites also carrying DORIS receivers (T/P and Jason). All estimated DORIS phase center corrections possess a systematic bias of about 15 mm in direction opposite to the Earth when fixing stations coordinates to IGN04D02 terrestrial reference frame, aligned to ITRF2000. This bias almost totally disappears when fixing DORIS station coordinates to the preliminary ITRF2005P solution.

SPOT satellite show small cross-track phase center bias (under 20 mm), creating potential errors in the TZ-geocenter component. They also present small annual signals that are probably related to current weaknesses in the orbit determination models or estimation strategies.

ENVISAT estimated radial phase center offset possesses a clear discontinuity on October 12, 2004 (flight software update) requiring further investigation.

Results obtained for GPS and DORIS estimated phase center offsets are different for common satellites (T/P and Jason). However, we also demonstrated that the estimated values depend strongly on the reference frame used in the case of DORIS and in the PCV model adopted for GPS.

Geodetic results derived from DORIS data reprocessing using the previously estimated phase center correction show very little improvement in weekly station coordinates. How it could be interesting to continue this study and estimate discontinuities in the center of mass of the satellite toward the center of phase of the DORIS antenna for each SPOT satellite after each satellite maneuver, as these information are currently not available from CNES for these satellites. Estimated geocenter variations were totally the same while the TRF scale could be found to significantly decrease from -2.5 ppb to -0.7 ppb.

At this point, we do not recommend the adoption of these corrections for DORIS but we recommend that the other IDS analysis centers could do a similar study to verify if the estimated corrections have a physical meaning or are just systematic errors relative to analysis software and data processing techniques.

Figure captions

Figure 1 :

 1 Figure 1: Daily estimation of SPOT satellites radial phase offset using DORIS data in 2004.

Figure 2 :

 2 Figure 2: Daily estimation of SPOT2 radial phase center offset using either ITRF2000 or ITRF2005P reference frame in 2004.

Figure 3 :

 3 Figure 3: Daily estimation of ENVISAT satellite radial phase center offset using DORIS data in 2004. Changes in flight software occurred on October 12, 2004.

Figure 4 :

 4 Figure 4: Estimated GPS antenna phase center offsets for the Jason satellite, using phase center variation model derived from anechoic measurements (pre-launch data) from 2004.

Figure 5 :

 5 Figure 5: Estimated GPS antenna phase center offsets for the Jason satellite, using phase center variation model derived from maps developed with in-flight data from 2004.

Figure 6 :

 6 Figure 6: Estimated GPS antenna phase center offsets for the TOPEX/Poseidon satellite, using phase center variation model derived from anechoic measurements (pre-launch data) from 2004.

Acknowledgments

This research was carried out at the Jet Propulsion Laboratory, California Institute of Technology, under a contract with the National Aeronautics and Space Administration.