Xavier Bultel

Pascal Lafourcade

Unlinkable and Strongly Accountable Sanitizable Signatures from Verifiable Ring Signatures

An Unlinkable Sanitizable Signature scheme (USS) allows a sanitizer to modify some parts of a signed message in such away that nobody can link the modified signature to the original one. A Verifiable Ring Signature scheme (VRS) allows the users to sign messages anonymously within a group where a user can prove a posteriori to a verifier that it is the author of a given signature. In this paper, we first revisit the notion of VRS: we improve the proof capabilities of the users, we give a complete security model for VRS and we give an efficient and secure scheme called EVeR. Our main contribution is GUSS, a Generic USS based on a VRS scheme and an unforgeable signature scheme. We show that GUSS instantiated with EVeR and Schnorr's signature is twice as efficient as the best USS scheme of the literature. Moreover, we propose a stronger definition of accountability: an USS is accountable when the signer can prove whether a signature is sanitized. We formally define the notion of strong accountability where the sanitizer can also prove the origin of a signature. We show that the notion of strong accountability is important in practice. Finally, we prove the security properties of GUSS (including strong accountability) and EVeR under the Decisional Diffie-Hellman (DDH) assumption in the random oracle model.

Introduction

Sanitizable Signatures (SS) were introduced by Ateniese et al. [START_REF] Ateniese | Sanitizable Signatures[END_REF], but similar primitives were independently proposed in [START_REF] Steinfeld | Content Extraction Signatures[END_REF]. In this primitive, a signer allows a proxy (called the sanitizer) to modify some parts of a signed message. For example, a magistrate wishes to delegate the power to summon someone to the court to his secretary. He signs the message "Franz is summoned to court for an interrogation on Monday" and gives the signature to his secretary, where "Franz" and "Monday" are sanitizable and the other parts are fixed. Thus, in order to summon Joseph K. on Saturday in the name of the magistrate, the secretary can change the signed message into "Joseph K. is summoned to the court for an interrogation on Saturday".

Ateniese et al. in [START_REF] Ateniese | Sanitizable Signatures[END_REF] proposed some applications of this primitive in privacy of health data, authenticated media streams and reliable routing information. They also introduced five security properties formalized by Brzuska et al. in [START_REF] Brzuska | Security of sanitizable signatures revisited[END_REF]: Unforgeability: no unauthorized user can generate a valid signature.

Immutability: the sanitizer cannot transform a signature from an unauthorized message. Privacy: no information about the original message is leaked by a sanitized signature. Transparency: nobody can say if a signature is sanitized or not. Accountability: the signer can prove whether a signature is sanitized.

Finally, in [START_REF] Brzuska | Unlinkability of sanitizable signatures[END_REF] the authors point out a non-studied but relevant property called unlinkability: a scheme is unlinkable when it is not possible to link a sanitized signature to the original one. The authors give a generic unlinkable scheme based on group signatures. In 2016, Fleischhacker et al. [START_REF] Fleischhacker | Efficient unlinkable sanitizable signatures from signatures with re-randomizable keys[END_REF] give a more efficient construction based on signatures with re-randomizable keys.

On the other hand, ring signature is a well-studied cryptographic primitive introduced by Rivest et al. in [START_REF] Rivest | How to leak a secret[END_REF], where some users can sign anonymously within a group of users. Such a scheme is verifiable [START_REF] Lv | Verifiable Ring Signature[END_REF] when any user can prove that he is the signer of a given message. In this paper, we improve the properties of VRS by increasing the proof capabilities of the users. We also give an efficient VRS scheme called EVeR and a generic unlinkable sanitizable signature scheme called GUSS that uses a verifiable ring signature. We also show that the definition of accountability is too weak for practical use and we propose a stronger definition.

Contributions: Existing VRS schemes allow any user to prove that he is the signer of a given message. We extend the definition of VRS to allow a user to prove that he is not the signer of a given message. We give a formal security model for VRS that takes into account this property. We first extend the classical security properties of ring signatures to verifiable ring signatures, namely the unforgeability (no unauthorized user can forge a valid signature) and the anonymity (nobody can distinguish who is the signer in the group). In addition we define the accountability (if a user signs a message then he cannot prove that he is not the signer) and the non-seizability (a user cannot prove that he is the signer of a message if it is not true, and a user cannot forge a message such that the other users cannot prove that they are not the signers). To the best of our knowledge, it is the first time that formal security models are proposed for VRS. We also design an efficient secure VRS scheme under the DDH assumption in the random oracle model.

The definition of accountability for SS given in [START_REF] Brzuska | Security of sanitizable signatures revisited[END_REF][START_REF] Brzuska | Unlinkability of sanitizable signatures[END_REF][START_REF] Fleischhacker | Efficient unlinkable sanitizable signatures from signatures with re-randomizable keys[END_REF] considers that the signer can prove the origin of a signature (signer or sanitizer) by using a proof algorithm such that:

1. The signer cannot forge a signature and a proof that the signature has been forged by the sanitizer. 2. The sanitizer cannot forge a signature such that the proof algorithm blames the signer. The proof algorithm requires the secret key of the signer. To show that this definition is too weak, we consider a signer who cannot prove the origin of a litigious signature. The signer claims that he lost his secret key because of problems with his hard drive. There is no way to verify whether the signer is lying. Unfortunately, without his secret key, the signer cannot generate the proof for the litigious signature, hence nobody can judge whether the signature is sanitized or not. Depending on whether the signer is lying, there is a risk of accusing the signer or the sanitizer wrongly. To solve this problem, we add a second proof algorithm that allows the sanitizer to prove the origin of a signature. To achieve strong accountability, the two following additional properties are required:

1. The sanitizer cannot sanitize a signature σ and prove that σ is not sanitized. 2. The signer cannot forge a signature such that the sanitizer proof algorithm accuses the sanitizer.

The main contribution of this paper is to propose an efficient and generic unlinkable SS scheme called GUSS. This scheme is instantiated by a VRS and an unforgeable signature scheme. It is the first SS scheme that achieves strong accountability. We compare GUSS with the other schemes of the literature: Brzuska et al. [START_REF] Brzuska | Unlinkability of sanitizable signatures[END_REF]. This scheme is based on group signatures. Our scheme is built on the same model, but it uses ring signatures instead of group signatures. The main advantage of group signatures is that the size of the signature is not proportional to the size of the group. However, for small groups, ring signatures are much more efficient than group signatures. Since the scheme of Brzuska et al. and GUSS uses group/ring signatures for groups of two users, GUSS is much more practical for an equivalent level of genericity. Fleischhacker et al. [START_REF] Fleischhacker | Efficient unlinkable sanitizable signatures from signatures with re-randomizable keys[END_REF]. This scheme is based on signatures with re-randomizable keys. It is generic, however it uses different tools that must have special properties to be compatible with each other. To the best of our knowledge, it is the most efficient scheme of the literature. GUSS instantiated with EVeR and Schnorr's signature is twice as efficient as the best instantiation of this scheme. In Fig. A, we compare the efficiency of each algorithm of our scheme and the scheme of Fleischhacker et al.. Lai et al. [START_REF] Russell | Efficient Sanitizable Signatures Without Random Oracles[END_REF]. Recently, Lai et al. proposed a USS that is secure in the standard model. This scheme uses pairings and is much less efficient than the scheme of Fleischhacker et al., so this scheme is much less efficient than our scheme. In their paper [START_REF] Russell | Efficient Sanitizable Signatures Without Random Oracles[END_REF], Lai et al. give a comparison of the efficiency of the three schemes of the literature. The first six columns give the number of exponentiations of each algorithms of both schemes, namely the key generation algorithm of the signer (SiGen) and the sanitizer (SaGen), the signature algorithm (Sig), the verification algorithm (Ver), the sanitize algorithm (San), the proof algorithm (SiProof) and the judge algorithm (SiJudge). The last six columns give respectively the size of the public key of the signer (pk) and the sanitizer (spk), the size of the secret key of the signer (sk) and the sanitizer (ssk), the size of a signature (σ) and the size of a proof (π) outputted by SiProof. This size is measured in elements of a group G of prime order. As in [START_REF] Fleischhacker | Efficient unlinkable sanitizable signatures from signatures with re-randomizable keys[END_REF], for the sake of clarity, we do not distinguish between elements of G and elements of Z * p . We consider the best instantiation of the scheme of Fleischhacker et al. given in [START_REF] Fleischhacker | Efficient unlinkable sanitizable signatures from signatures with re-randomizable keys[END_REF]. In Appendix A, we give a detailed complexity evaluation of our schemes.

Related works: Sanitizable Signatures (SS) was first introduced by Ateniese et al. [START_REF] Ateniese | Sanitizable Signatures[END_REF]. Later, Brzuska et al. gave formal security definitions [START_REF] Brzuska | Security of sanitizable signatures revisited[END_REF] for unforgeability, immutability, privacy, transparency and accountability. Unlinkability was introduced and formally defined by Brzuska et al. in [START_REF] Brzuska | Unlinkability of sanitizable signatures[END_REF]. In [START_REF] Brzuska | Non-interactive Public Accountability for Sanitizable Signatures[END_REF], Brzuska et al. introduce an alternative definition of accountability called non-interactive public accountability where the capability to prove the origin of a signature is given to a third party. One year later, the same authors propose a stronger definition of unlinkability [START_REF] Brzuska | Efficient and Perfectly Unlinkable Sanitizable Signatures without Group Signatures[END_REF] and design a scheme that is both strongly unlinkable and non-interactively public accountable. However, noninteractive public accountability is not compatible with transparency. In this paper, we focus on schemes that are unlinkable, transparent and interactively accountable. To the best of our knowledge, there are only 3 schemes with these 3 properties, i.e. [START_REF] Brzuska | Unlinkability of sanitizable signatures[END_REF][START_REF] Fleischhacker | Efficient unlinkable sanitizable signatures from signatures with re-randomizable keys[END_REF][START_REF] Russell | Efficient Sanitizable Signatures Without Random Oracles[END_REF].

Some works focus on other properties of SS that we do not consider here, such as SS with multiple sanitizers [START_REF] Canard | Sanitizable Signatures with Several Signers and Sanitizers[END_REF], or SS where the power of the sanitizer is limited [START_REF] Canard | On Extended Sanitizable Signature Schemes[END_REF]. Finally, there exist other primitives that solve related but different problems such as homomorphic signatures [START_REF] Johnson | Homomorphic Signature Schemes[END_REF], redactable signatures [START_REF] Brzuska | Redactable Signatures for Tree-Structured Data: Definitions and Constructions[END_REF] or proxy signatures [START_REF] Fuchsbauer | Anonymous Proxy Signatures[END_REF]. The differences between these primitives and sanitizable signatures are detailed in [START_REF] Fleischhacker | Efficient unlinkable sanitizable signatures from signatures with re-randomizable keys[END_REF].

On the other hand, Ring Signatures (RS) [START_REF] Rivest | How to leak a secret[END_REF] were introduced by Rivest et al. in 2003. Security models of this primitive were defined in [START_REF] Bender | Ring signatures: Stronger definitions, and constructions without random oracles[END_REF]. Verifiable Ring Signatures (VRS) [START_REF] Lv | Verifiable Ring Signature[END_REF] were introduced in 2003 by Lv. RS allow the users to sign anonymously within a group, and VRS allow a user to prove that it is the signer of a given message. The authors of [START_REF] Lv | Verifiable Ring Signature[END_REF] give a VRS construction that is based on the discrete logarithm problem. Two other VRS schemes were proposed by Wand et al. [START_REF] Wang | Ring signature scheme based on multivariate public key cryptosystems[END_REF] and by Changlung et al. [START_REF] Changlun | A new verifiable ring signature scheme based on nyberg-rueppel scheme[END_REF]. The first one is based on the Nyberg-Rueppel signature scheme and the second one is a generic construction based on multivariate public key cryptosystems. In these three schemes, a user can prove that he is the signer of a given signature, however, he has no way to prove that he is not the signer, and it seems to be non-trivial to add this property to these schemes. Convertible ring signatures [START_REF] Lee | Convertible ring signature[END_REF] are very close to verifiable ring signatures: they allow the signer of an anonymous (ring) signature to transform it into a standard signature (i.e. a deanonymized signature). It can be used as a verifiable ring signature because the deanonymized signature can be viewed as a proof that the user is the signer of a given message. However, in this paper we propose a stronger definition of VRS where a user also can prove that he is not the signer of a message, and this property cannot be achieved using convertible signatures.

A Revocable-iff-Linked Ring Signature (RLRS) [START_REF] Ho Au | Event-Oriented k-Times Revocable-iff-Linked Group Signatures[END_REF] (also called List Signature [START_REF] Canard | List signature schemes[END_REF]) is a kind of RS that has the following property: if a user signs two messages for the same event-id, then it is possible to link these signatures and the user's identity is publicly revealed. It can be used to design a VRS in our model: to prove whether he is the signer of a given message, the user signs a second message using the same event-id. If the two signatures are linked, then the judge is convinced that the user is the signer, else he is convinced that the user is not the signer. However, RLRS requires security properties that are too strong for VRS (linkability and traceability) and it would result in less efficient schemes.

Outline: In Section 2, we recall the standard cryptographic tools used in this paper. In Section 3 and Section 4, we present the formal definition and the security models for verifiable ring signatures and unlinkable sanitizable signatures. In Section 5, we present our scheme EvER. Finally, in Section 6, we present our scheme GUSS, before concluding in Section 7.

Cryptographic Tools

We present the cryptographic tools used throughout this paper. We first recall the DDH assumption.

Definition 1 (DDH [START_REF] Boneh | The decision Diffie-Hellman problem[END_REF]). Let G be a multiplicative group of prime order p and g ∈ G be a generator. Given an instance h = (g a , g b , g z ) for unknown a, b, z $ ← Z * p , the Decisional Diffie-Hellman (DDH) problem is to decide whether z = a • b or not. The DDH assumption states that there exists no polynomial time algorithm that solves the DDH problem with a non-negligible advantage.

In the following, we recall some notions about digital signatures. S is said to be deterministic when the algorithm D.Sig is deterministic. S is said to be correct when for any security parameter k ∈ N, any message m ∈ {0, 1} * , any set ← D.Init(1 k ) and any (pk, sk) ← D.Gen(set), D.Ver(pk, m, D.Sig(m, sk)) = 1. Moreover, such a scheme is unforgeable when no polynomial adversary wins the following experiment with non-negligible probability where D.Sig(•, sk) is a signature oracle, q S is the number of queries to this oracle and σ i is the i th signature computed by the signature oracle:

Exp unf S,A (k): set ← D.Init(1 k ) (pk, sk) ← D.Gen(set) (m * , σ * ) ← A D.Sig(•,sk) (pk) if (D.Ver(pk, m * , σ * ) = 1) and (∀ i ∈ 1, q S , σ i = σ * ) then return 1, else return 0
As it is mentioned in [START_REF] Fleischhacker | Efficient unlinkable sanitizable signatures from signatures with re-randomizable keys[END_REF], any DS scheme can be changed into a deterministic scheme without loss of security using a pseudo random function, that can be simulated by a hash function in the random oracle model. The following scheme is the deterministic version of the well-known Schnorr's Signature scheme [START_REF] Schnorr | Efficient identification and signatures for smart cards[END_REF].

Scheme 1 (Deterministic Schnorr's Signature [START_REF] Schnorr | Efficient identification and signatures for smart cards[END_REF]) This signature is defined by the following algorithms:

D.Init(1 k ): It returns a setup value set = (G, p, g, H) where G is a group of prime order p, g ∈ G and H : {0, 1} * → Z * p is a hash function. D.Gen(set): It picks sk $ ← Z *
p , computes pk = g sk and returns (pk, sk). D.Sig(m, sk):

It computes the r = H(m||sk), R = g r , z = r + sk • H(R||m) and returns σ = (R, z). D.Ver(pk, m, σ): It parses σ = (R, z), if g z = R • pk H(R||m) then it returns 1, else 0.
This DS scheme is deterministic and unforgeable under the DL assumption in the random oracle model.

A Zero-Knowledge Proof (ZKP) [START_REF] Goldwasser | The knowledge complexity of interactive proof systems[END_REF] allows a prover knowing a witness w to convince a verifier that a statement s is in a given language without leaking any information. Such a proof is a Proof of Knowledge (PoK) [START_REF] Bellare | On defining proofs of knowledge[END_REF] when the verifier is also convinced that the prover knows the witness w. We recall the definition of a non-interactive zeroknowledge proof of knowledge.

Definition 3 (NIZKP).

Let R be a binary relation and let L be a language such that s ∈ L ⇔ (∃w, (s, w) ∈ R). A non-interactive ZKP (NIZKP) for the language L is a couple of algorithms (Prove, Verify) such that:

Prove(s, w). This algorithm outputs a proof π. Verify(s, π). This algorithm outputs a bit b.

A NIZKP proof has the following properties:

Completeness. For any statement s ∈ L and the corresponding witness w, we have that Verify(s, Prove(s, w)) = 1. Soundness. There is no polynomial time adversary A such that A(L) outputs (s, π)

such that Verify(s, π) = 1 and s ∈ L with non-negligible probability. Zero-knowledge. A proof π leaks no information, i.e. there exists a polynomial time algorithm Sim (called the simulator) such that Prove(s, w) and Sim(s) follow the same probability distribution.

Moreover, such a proof is a proof of knowledge when for any s ∈ L and any algorithm A, there exists a polynomial time knowledge extractor E such that the probability that E A(s) (s) outputs a witness w such that (s, w) ∈ R given access to A(s) as an oracle is as high as the probability that A(s) outputs a proof π such that Verify(s, π) = 1.

Formal Model of Verifiable Ring Signatures

We formally define the Verifiable Ring Signatures (VRS) and the corresponding security notions. A VRS is a ring signature scheme where a user can prove to a judge whether he is the signer of a message or not. It is composed of six algorithms. V.Init, V.Gen, V.Sig and V.Ver are defined as in the usual ring signature definitions. V.Gen generates public and private keys. V.Sig anonymously signs a message according to a set of public keys. V.Ver verifies the soundness of a signature. A VRS has two additional algorithms: V.Proof allows a user to prove whether he is the signer of a message or not, and V.Judge allows anybody to verify the proofs outputted by V.Proof.

Definition 4 (Verifiable Ring Signature (VRS)). A Verifiable Ring Signature scheme is a tuple of six algorithms defined by: V.Init then π proves that σ was (resp. was not) generated by the signer corresponding to the public key pk. It outputs ⊥ when the proof is not well formed.

Unforgeability: We first adapt the unforgeability property of ring signatures [START_REF] Bender | Ring signatures: Stronger definitions, and constructions without random oracles[END_REF] to VRS. Informally, a VRS is unforgeable when no adversary is able to forge a signature for a ring of public keys without any corresponding secret key. In this model, the adversary has access to a signature oracle V.Sig(•, •, •) (that outputs signatures of chosen messages for chosen users in the ring) and a proof oracle V.Proof(•, •, •, •, •) (that outputs proofs as the algorithm V.Proof for chosen signatures and chosen users). The adversary succeeds when it outputs a valid signature that was not already generated by the signature oracle.

Definition 5 (Unforgeability). Let P be a VRS and n be an integer. Let the two following oracles be:

V.Sig(•, •, •): On input (L, l, m), if 1 ≤ l ≤ n then it runs σ ← V.Sig(L, sk l , m) and returns σ, else it returns ⊥. V.Proof(•, •, •, •, •): On input (L, m, σ, l), if 1 ≤ l ≤ n then this proof oracle runs π ← V.
Proof(L, m, σ, pk l , sk l ) and returns π, else it returns ⊥. P is n-unf secure when for any polynomial time adversary A, the probability that A wins the following experiment is negligible, where q S is the number of calls to the oracle V.Sig(•, •, •) and σ i is the i th signature outputted by the oracle V.Sig(•, •, •):

Exp n-unf P,A (k): set ← V.Init(1 k ) ∀1 ≤ i ≤ n, (pk i , ski) ← V.Gen(set) (L * , σ * , m * ) ← A V.Sig(•,•,•),V.Proof(•,•,•,•,•) ({pk i } 1≤i≤n ) if V.Ver(L * , σ * , m * ) = 1 and L * ⊆ {pk i } 1≤i≤n and ∀ i ∈ 1, qS , σi = σ * then return 1, else return 0
P is unforgeable when it is t(k)-unf secure for any polynomial t.

Annonymity: We adapt the anonymity property of ring signatures [START_REF] Bender | Ring signatures: Stronger definitions, and constructions without random oracles[END_REF] to VRS. Informally, a VRS is anonymous when no adversary is able to link a signature to the corresponding user. The adversary has access to the signature oracle and the proof oracle. During a first phase, it chooses two honest users in the ring, and in the second phase, it has access to a challenge oracle LRSO b (d 0 , d 1 , •, •) that outputs signatures of chosen messages using the secret key of one of the two chosen users. The adversary succeeds if he guesses which user is chosen by the challenge oracle. Note that if the adversary uses the proof oracle on the signatures generated by the challenge oracle then he loses the experiment. Definition 6 (Anonymity). Let P be a VRS and let n be an integer. Let the following oracle be:

LRSO b (d 0 , d 1 , •, •): On input (m, L), if {pk d0 , pk d1 } ⊆ L then this oracle runs σ ← V.Sig(L, sk d b , m
) and returns σ, else it returns ⊥. P is n-ano secure when for any polynomial time adversary A = (A 1 , A 2 ), the probability that A wins the following experiment is negligibly close to 1/2, where V.Sig(•, •, •) and V.Proof(•, •, •, •, •) are defined as in Def. 5 and where q S (resp. q P ) is the number of calls to the oracle

V.Sig(•, •, •) (resp. V.Proof(•, •, •, •, •)), (L i , m i , σ i , l i ) is the i th query sent to oracle V.Proof(•, •, •, •, •) and σ j is the j th signature outputted by the oracle LRSO b (d 0 , d 1 , •, •): Exp n-ano P,A (k): set ← V.Init(1 k ) ∀1 ≤ i ≤ n, (pk i , ski) ← V.Gen(set) (d0, d1) ← A ({pk i } 1≤i≤n ) b $ ← {0, 1} b * ← A V.Sig(•,•,•),V.Proof(•,•,•,•,•),LRSO b (d 0 ,d 1 ,•,•) 2 ({pk i } 1≤i≤n ) if (b = b * ) and (∀ i, j ∈ 1, max(qS, qP ) , (σi = σ j ) or (li = d0 and li = d1))
then return 1, else return 0 P is anonymous when it is t(k)-ano secure for any polynomial t.

Accountability:

We consider an adversary that has access to a proof oracle and a signature oracle. A VRS is accountable when no adversary is able to forge a signature σ (that was not outputted by the signature oracle) together with a proof that it is not the signer of σ. Note that the ring of σ must contain at most one public key that does not come from an honest user, thus the adversary knows at most one secret key that corresponds to a public key in the ring. Definition 7 (Accountability). Let P be a VRS and let n be an integer. P is n-acc secure when for any polynomial time adversary A, the probability that A wins the following experiment is negligible, where V.Sig(•, •, •) and V.Proof(•, •, •, •, •) are defined as in Def. 5 and where q S is the number of calls to the oracle V.Sig(•, •, •) and σ i is the i th signature outputted by the oracle V.Sig(•, •, •): P is accountable when it is t(k)-acc secure for any polynomial t.

Exp n-acc P,A (k): set ← V.Init(1 k ) ∀1 ≤ i ≤ n, (pk i , ski) ← V.Gen(set) (L * , m * , σ * , pk * , π * ) ← A V.Sig(•,•,•),V.Proof(•,•,•,•,•) ({pk i } 1≤i≤n ) if (L ⊆ {pk i } 1≤i≤n ∪ {pk * })
Non-seizability: We distinguish two experiments for this property: the first experiment, denoted non-sei-1, considers an adversary that has access to a proof oracle and a signature oracle. Its goal is to forge a valid signature with a proof that the signer is another user in the ring.

Definition 8 (n-non-sei-1 experiment). Let P be a SS. P is n-non-sei-1 secure when for any polynomial time adversary A, the probability that A wins the following experiment is negligible, where V.Sig(•, •, •) and V.Proof(•, •, •, •, •) and where q S is the number of calls to the oracle V.Sig(•, •, •) and (L i , l i , m i ) (resp. σ i ) is the i th query to the oracle V.Sig(•, •, •) (resp. signature outputted by this oracle):

Exp n-non-sei-1 P,A (k): set ← V.Init(1 k ) ∀1 ≤ i ≤ n, (pk i , sk i ) ← V.Gen(set) (L * , m * , σ * , l * , π * ) ← A V.Sig(•,•,•),V.Proof(•,•,•,•,•) ({pk i } 1≤i≤n ) π ← V.Proof(L * , m * , σ * , pk, sk) if (V.Ver(L * , σ * , m * ) = 1) and (V.Judge(L * , m * , σ * , pk l * , π * ) = 1)
and

(∀ i ∈ 1, q S , (L i , l i , m i , σ i ) = (L * , l * , m * , σ * )) then return 1, else return 0
The second experiment, denoted non-sei-2, considers an adversary that has access to a proof oracle and a signature oracle and that receives the public key of a honest user as input. The goal of the adversary is to forge a signature σ such that the proof algorithm ran by the honest user returns a proof that σ was computed by the honest user (i.e. the judge algorithm returns 1) or a non-valid proof (i.e. the judge algorithm returns ⊥). Moreover, the signature σ must not come from the signature orale.

Definition 9 (Non-seizability). Let P be a VRS and n be an integer. P is n-non-sei-2 secure when for any polynomial time adversary A, the probability that A wins the following experiment is negligible, where V.Sig(•, •, •) and V.Proof(•, •, •, •, •) are defined as in Def. 5 and where q S is the number of calls to the oracle V.Sig(•, •, •) and σ i is the i th signature outputted by the oracle V.Sig(•, •, •): P is non-seizable when it is both t(k)-non-sei-1 and t(k)-non-sei-2 secure for any polynomial t.

Exp n-non-sei-2 P,A (k): set ← V.Init(1 k ) (pk, sk) ← V.Gen(set) (L * , m * , σ * ) ← A V.Sig(•,•,•),V.Proof(•,•,•,•,•) (pk) π ← V.Proof(L * , m * , σ * , pk, sk) if (V.

Formal Model of Sanitizable Signature

We give the formal definition and security properties of the sanitizable signature primitive. Compared to the previous definitions where only the signer can prove the origin of a signature, our definition introduces algorithms that allow the sanitizer to prove the origin of a signature. Moreover, in addition to the usual security models of [START_REF] Brzuska | Security of sanitizable signatures revisited[END_REF], we present two new security experiments that improve the accountability definition.

A SS scheme contains 10 algorithms. Init outputs the setup values. SiGen and SaGen generate respectively the signer and the sanitizer public/private keys. As in classical signature schemes, the algorithms Sig and Ver allow the users to sign a message and to verify a signature. However, the signatures are computed using a sanitizer public key and an admissible function ADM. The algorithm San allows the sanitizer to transform a signature of a message m according to a modification function MOD: if MOD is admissible according to the admissible function (i.e. MOD(ADM) = 1) this algorithm returns a signature of the message m = MOD(m).

SiProof allows the signer to prove whether a signature is sanitized or not. Proofs outpoutted by this algorithm can be verified by anybody using the algorithm SiJudge. Finally, algorithms SaProof and SaJudge have the same functionalities as SiProof and SiJudge, but the proofs are computed from the secret parameters of the sanitizer instead of the signer.

Definition 10 (Sanitizable Signature (SS)). A Sanitizable Signature scheme is a tuple of 10 algorithms defined as follows:

Init(1 k ): It returns a setup value set. SiGen(set): It returns a pair of signer public/private keys (pk, sk). SaGen(set): It returns a pair of sanitizer public/private keys (spk, ssk). Sig(m, sk, spk, ADM): This algorithm computes a signature σ from the message m using the secret key sk, the sanitizer public key spk and the admissible function ADM. Note that we assume that ADM can be efficiently recovered from any signature as in the definition of Fleischhacker et al. [START_REF] Fleischhacker | Efficient unlinkable sanitizable signatures from signatures with re-randomizable keys[END_REF]. San(m, MOD, σ, pk, ssk): Let the admissible function ADM according to the signature σ. If ADM(MOD) = 1 then this algorithm returns a signature σ of the message m = MOD(m) using the signature σ, the signer public key pk and the sanitizer secret key ssk. Else it returns ⊥. Ver(m, σ, pk, spk): It returns a bit b: if the signature σ of m is valid for the two public keys pk and spk then b = 1, else b = 0. SiProof(sk, m, σ, spk): It returns a signer proof π si for the signature σ of m using the signer secret key sk and the sanitizer public key spk. SaProof(ssk, m, σ, pk): It returns a sanitizer proof π sa for the signature σ of m using the sanitizer secret key ssk and the signer public key pk. SiJudge(m, σ, pk, spk, π si ): It returns a bit d or the bottom symbol ⊥: if π si proves that σ comes from the signer corresponding to the public key pk then d = 1, else if π si proves that σ comes from the sanitizer corresponding to the public key spk then d = 0, else the algorithm outputs ⊥. SaJudge(m, σ, pk, spk, π sa ): It returns a bit d or the bottom symbol ⊥: if π sa proves that σ comes from the signer corresponding to the public key pk then d = 1, else if π sa proves that σ comes from the sanitizer corresponding to the public key spk then d = 0, else the algorithm outputs ⊥.

As it is mentioned in Introduction, SS schemes have the following security properties: unforgeability, immutability, privacy, transparency and accountability. In [START_REF] Brzuska | Security of sanitizable signatures revisited[END_REF] authors show that if a scheme has the immutability, the transparency and the accountability properties, then it has the unforgeability and the privacy properties. Hence we do not need to prove these two properties, so we do not recall their formal definitions.

Immutability: A SS is immutable when no adversary is able to sanitize a signature without the corresponding sanitizer secret key or to sanitize a signature using a modification function that is not admissible (i.e. ADM(MOD) = 0). To help him, the adversary has access to a signature oracle Sig(., sk, ., .) and a proof oracle SiProof(sk, ., ., .).

Definition 11 (Immutability [START_REF] Brzuska | Security of sanitizable signatures revisited[END_REF]). Let the following oracles be: Sig(., sk, ., .): On input (m, ADM, spk), this oracle returns Sig(m, sk, ADM, spk). SiProof(sk, ., ., .): On input (m, σ, spk), this oracle returns SiProof(sk, m, σ, spk). Let P be a SS. P is Immut secure (or immutable) when for any polynomial time adversary A, the probability that A wins the following experiment is negligible, where q Sig is the number of calls to the oracle Sig(., sk, ., .), (m i , ADM i , spk i ) is the i th query asked to the oracle Sig(., sk, ., .) and σ i is the corresponding response:

Exp Immut P,A (k): set ← Init(1 k ) (pk, sk) ← SiGen(set) (spk * , m * , σ * ) ← A Sig(.,
sk,.,.),SiProof(sk,.,.,.) (pk) if (Ver(m * , σ * , pk, spk * ) = 1) and (∀ i ∈ 1, q Sig , (spk * = spk i ) or (∀ MOD such that ADMi(MOD) = 1, m * = MOD(mi))) then return 1, else return 0 Transparency: The transparency property guarantees that no adversary is able to distinguish whether a signature is sanitized or not. In addition to the signature oracle and the signer proof oracle, the adversary has access to a sanitize oracle San(., ., ., ., ssk) that sanitizes chosen signatures and a sanitizer proof oracle SaProof(ssk, ., ., .) that computes sanitizer proofs for given signatures. Moreover the adversary has access to a challenge oracle Sa/Si(b, pk, spk, sk, ssk, ., ., .) that depends on a randomly chosen bit b: this oracle signs a given message and sanitizes it, if b = 0 then it outputs the original signature, otherwise it outputs the sanitized signature. The adversary cannot use the proof oracles on the signatures outputted by the challenge oracle. To succeed the experiment, the adversary must guess b. [START_REF] Brzuska | Security of sanitizable signatures revisited[END_REF]). Let the following oracles be: San(., ., ., ., ssk): On input (m, MOD, σ, pk), it returns San(m, MOD, σ, pk, ssk). SaProof(ssk, ., ., .): On input (m, σ, pk), this oracle returns SaProof(ssk, m, σ, pk). Sa/Si(b, pk, spk, sk, ssk, ., ., .): On input (m, ADM, MOD), if ADM(MOD) = 0, this oracle returns ⊥. Else if b = 0, this oracle returns Sig(MOD(m), sk, spk, ADM), else if b = 1, this oracle returns San(m, MOD, Sig(m, sk, spk, ADM), pk, ssk). Let P be a SS. P is Trans secure (or transparent) when for any polynomial time adversary A, the probability that A wins the following experiment is negligible, where Sig(., sk, ., .) and SiProof(sk, ., ., .) are defined as in Def. 11, and where S Sa/Si (resp. S SiProof and S SaProof ) corresponds to the set of all signatures outputted by the oracle Sa/Si (resp. sent to the oracles SiProof and SaProof):

Definition 12 (Transparency

Exp Trans P,A (k): set ← Init(1 k ) (pk, sk) ← SiGen(set) (spk, ssk) ← SaGen(set) b $ ← {0, 1} b ← A
Sig(.,sk,.,.),San(.,.,.,.,ssk),SiProof(sk,.,.,.) SaProof(ssk,.,.,.),Sa/Si(b,pk,spk,sk,ssk,.,.,.) (pk, spk)

if (b = b ) and (S Sa/Si ∩ (S SiProof ∪ S SaProof ) = ∅)
then return 1, else return 0 Unlinkablility: The unlinkablility property ensures that a sanitized signature cannot be linked with the original one. We consider an adversary that has access to the signature oracle, the sanitize oracle, and both the signer and the sanitizer proof oracles. Moreover, the adversary has access to a challenge oracle LRSan(b, pk, ssk, ., .) that depends to a bit b: this oracle takes as input two signatures σ 0 and σ 1 , the two corresponding messages m 0 and m 1 and two modification functions MOD 0 and MOD 1 chosen by the adversary. If the two signatures have the same admissible function ADM, if MOD 0 and MOD 1 are admissible according to ADM and if MOD 0 (m 0 ) = MOD 1 (m 1 ) then the challenge oracle sanitizes σ b using MOD b and returns it. The goal of the adversary is to guess the bit b.

Definition 13 (Unlinkability [START_REF] Brzuska | Security of sanitizable signatures revisited[END_REF]). Let the following oracles be: LRSan(b, pk, ssk, ., .):

On input ((m 0 , MOD 0 , σ 0 )(m 1 , MOD 1 , σ 1 )), if for i ∈ {0, 1},
Ver(m i , σ i , pk, spk) = 1 and ADM 0 = ADM 1 and ADM 0 (MOD 0 ) = 1 and ADM 1 (MOD 1 ) = 1 and MOD 0 (m 0 ) = MOD 1 (m 1 ), then this oracle returns San(m b , MOD b , σ b , pk, ssk), else it returns 0. Let P be a SS of security parameter k. P is Unlink secure (or unlinkable) when for any polynomial time adversary A, the probability that A wins the following experiment is negligibly close to 1/2, where Sig(., sk, ., .) and SiProof(sk, ., ., .) are defined as in Def. 11 and San(., ., ., ., ssk) and SaProof(ssk, ., ., .) are defined as in Def. 12:

Exp Unlink P,A (k): set ← Init(1 k ) (pk, sk) ← SiGen(set) (spk, ssk) ← SaGen(set) b $ ← {0, 1} b ← A
Sig(.,sk,.,.),San(.,.,.,.,ssk) SiProof(sk,.,.,.),SaProof(ssk,.,.,.),LRSan(b,pk,spk,.,.) (pk, spk) if (b = b ) then return 1, else return 0 Accountability: Standard defintion of accountability is shared into two security experiments: the sanitizer accountability and the signer accountability. In the sanitizer accountability experiment, the adversary has access to the signature oracle and the signer proof oracle. Its goal is to forge a signature such that the signer proof algorithm returns a proof that this signature is not sanitized. To succeed the experiment, this signature must not come from the signature oracle. Definition 14 (Sanitizer Accountability [START_REF] Brzuska | Security of sanitizable signatures revisited[END_REF]). Let P be a SS. P is SaAcc-1 secure (or sanitizer accountable) when for any polynomial time adversary A, the probability that A wins the following experiment is negligible, where the oracles Sig(., sk, ., .) and SiProof(sk, ., ., .) are defined as in Def. 11, q Sig is the number of calls to the oracle Sig(., sk, ., .), the tuple (m i , ADM i , spk i ) is the i th query asked to the oracle Sig(., sk, ., .) and σ i is the corresponding response:

Exp SaAcc-1 P,A (k): set ← Init(1 k ) (pk, sk) ← SiGen(set) (spk * , m * , σ * ) ← A Sig(.,
sk,.,.),SiProof(sk,.,.,.) (pk)

π * si ← SiProof(sk, m * , σ * , spk * ) if ∀ i ∈ 1, q Sig , (σ * = σi)
and (Ver(m * , σ * , pk, spk * ) = 1) and (SiJudge(m * , σ * , pk, spk * , π * si ) = 0) then return 1, else return 0

In the signer accountability experiment, the adversary knows the public key of the sanitizer and has access to the sanitize oracle and the sanitizer proof oracle. Its goal is to forge a signature together with a proof that this signature is sanitized. To succeed the experiment, this signature must not come from the sanitize oracle.

Definition 15 (Signer Accountability [START_REF] Brzuska | Security of sanitizable signatures revisited[END_REF]). Let P be a SS. P is SiAcc-1 secure (or signer accountable) when for any polynomial time adversary A, the probability that A wins the following experiment is negligible, where the oracle San(., ., ., ., ssk) and SaProof(ssk, ., ., .) are defined as in Def. 12 and where q San is the number of calls to the oracle San(., ., ., ., ssk), (m i , MOD i , σ i , pk i ) is the i th query asked to the oracle San(., ., ., ., ssk) and σ i is the corresponding response:

Exp SiAcc-1 P,A (k): set ← Init(1 k ) (spk, ssk) ← SaGen(set) (pk * , m * , σ * , π *
si ) ← A San(.,.,.,.,ssk),SaProof(ssk,.,.,.) (spk)

if ∀ i ∈ 1, q San , (σ * = σ i )
and (Ver(m * , σ * , pk * , spk) = 1) and (SiJudge(m * , σ * , pk * , spk, π * si ) = 0) then return 1, else return 0 Strong Accountability: Since our definition of sanitizable signature provides a second proof algorithm for the sanitizer, we define two additional security experiments (for signer and sanitizer accountability) to ensure the soundness of the proofs computed by this algorithm. We say that a scheme is strongly accountable when it is signer and sanitizer accountable for both the signer and the sanitizer proof algorithms.

Thus, in our second signer accountability experiment, we consider an adversary that has access to the sanitize oracle and the sanitizer proof oracle. Its goal is to forge a signature such that the sanitizer proof algorithm returns a proof that this signature is sanitized. To win the experiment, this signature must not come from the sanitize oracle.

Definition 16 (Strong Signer Accountability). Let P be a SS. P is SiAcc-2 secure when for any polynomial time adversary A, the probability that A wins the following experiment is negligible, where q San is the number of calls to the oracle San(., ., ., ., ssk), (m i , MOD i , σ i , pk i ) is the i th query asked to the oracle San(., ., ., ., ssk) and σ i is the corresponding response:

Exp SiAcc-2 P,A (k): set ← Init(1 k ) (spk, ssk) ← SaGen(set)
(pk * , m * , σ * ) ← A San(.,.,.,.,ssk),SaProof(ssk,.,.,.) (spk)

π * sa ← SaProof(ssk, m * , σ * , pk * ) if ∀ i ∈ 1, q San , (σ * = σ i )
and (Ver(m * , σ * , pk * , spk) = 1) and (SaJudge(m * , σ * , pk * , spk, π * sa ) = 1) then return 1, else return 0 P is strong signer accountable when it is both SiAcc-1 and SiAcc-2 secure.

Finally, in our second sanitizer accountability experiment, we consider an adversary that knows the public key of the signer and has access to the signer oracle and the signer proof oracle. Its goal is to sanitize a signature with a proof that this signature is not sanitized. To win the experiment, this signature must not come from the signer oracle.

Definition 17 (Strong Sanitizer Accountability). Let P be a SS. P is SaAcc-2 secure when for any polynomial time adversary A, the probability that A wins the following experiment is negligible, Sig(., sk, ., .) and SiProof(sk, ., ., .) are defined as in Def. 11, q Sig is the number of calls to the oracle Sig(., sk, ., .), (m i , ADM i , spk i ) is the i th query asked to the oracle Sig(., sk, ., .) and σ i is the corresponding response:

Exp SaAcc-2 P,A (k): set ← Init(1 k ) (pk, sk) ← SaGen(set) (spk * , m * , σ * , π * sa ) ← A Sig(.,sk,.,.),SiProof(sk,.,.,.) (spk) if ∀ i ∈ 1, q Sig , (σ * = σi) and (Ver(m * , σ * , pk, spk * ) = 1) and (SaJudge(m * , σ * , pk, spk * , π * sa ) = 1) then return 1, else return 0 P is strong sanitizer accountable when it is both SaAcc-1 and SaAcc-2 secure.

An Efficient Verifiable Ring Signature: EVeR

We present our VRS scheme called EVeR (for Efficient VErifiable Ring signature). EVeR works as follows: the signer produces an anonymous commitment from his secret key and the message (i.e. a commitment that leaks no information about the secret key), then he proves that this commitment was produced with a secret key corresponding to one of the public keys of the group members using a zero-knowledge proof system. Note that the same methodology was used to design several ring signature schemes of the literature [START_REF] Ho Au | Event-Oriented k-Times Revocable-iff-Linked Group Signatures[END_REF][START_REF] Canard | List signature schemes[END_REF][START_REF] Chase | On Signatures of Knowledge[END_REF][START_REF] Hoshino | Anonymizable Signature and Its Construction from Pairings[END_REF]. Moreover, to prove that he is (resp. he is not) the signer of a message, the user proves that the commitment was (resp. was not) produced from the secret key that corresponds to his public key using a zero-knowledge proof system. Our scheme is based on the DDH assumption and uses a NIZKP of equality of two discrete logarithms out of n elements. We show how to build this NIZKP: Let G be a group of prime order p, n be an integer and let the following binary relation be:

R n =    (s, w) : s = {(h i , z i , g i , y i )} 1≤i≤n ; ∃i ∈ 1, n , (((h i , z i , g i , y i ) ∈ G 4 ) ∧(w = log gi (y i ) = log hi (z i )));    .
We denote by L n the language {s : ∃w, (s, w) ∈ R n }. Consider the case n = 1. In [START_REF] Chaum | Wallet databases with observers[END_REF], authors present an interactive zero-knowledge proof of knowledge system for the relation R 1 . It proves the equality of two discrete logarithms. For example using (h, z, g, y) ∈ L 1 , a prover convinces a verifier that log g (y) = log h (z). The witness used by the prover is w = log g (y). This proof system is a sigma protocol in the sense that there are only three interactions: the prover sends a commitment, the verifier sends a challenge, and the prover returns a response.

To transform the proof system of R 1 into a generic proof system of any R n , we use the generic transformation given in [START_REF] Cramer | Proofs of partial knowledge and simplified design of witness hiding protocols[END_REF]. For any integer n and any relation R, the authors show how to transform a zero-knowledge proof of knowledge of a witness w such that (s, w) ∈ R for a given statement s into a zero-knowledge proof of knowledge of a witness w such that there exists s ∈ S such that (s, w) ∈ R for a given set of n statements S, under the condition that the proof is a sigma protocol. Note that the resulting proof system is also a sigma protocol.

The final step is to transform it into a non-interactive proof system. We use the wellknown Fiat-Shamir transformation [START_REF] Fiat | Advances in Cryptology -CRYPTO' 86: Proceedings, chapter How To Prove Yourself: Practical Solutions to Identification and Signature Problems[END_REF]. This transformation changes any interactive proof system that is a sigma protocol into a non interactive one. The resulting proof system is complete, sound and zero-knowledge in the random oracle model. Finally, we obtain the following scheme.

Scheme 2 (LogEq n ) Let G be a group of prime order p, H : {0, 1} → Z * p be a hash function and n be an integer. We define the NIZKP LogEq n = (LEprove n , LEverif n ) for R n by: LEprove n ({(h i , z i , g i , y i )} 1≤i≤n , x). Let x = log gj (y j ) = log hj (z j ), this algorithm picks r j

$ ← Z * p , computes R j = g rj j and S j = h rj j . For all i ∈ 1, n and i = j, it picks c i $ ← Z * p and γ i $ ← Z * p , and computes R i = g γi i /y ci i and S i = h γi i /z ci i . It computes c = H(R 1 ||S 1 || . . . ||R n ||S n ). It then computes c j = c/( n i=1;i =j c i ) and γ j = r j + c j • x. It outputs π = {(R i , S i , c i , γ i )} 1≤i≤n . LEverif n ({(h i , z i , g i , y i )} 1≤i≤n , π). It parses π = {(R i , S i , c i , γ i )} 1≤i≤n . If H(R 1 || S 1 || . . . ||R n ||S n ) = n i=1;i =j c i then it returns 0. Else if there exists i ∈ 1, n such that g γi i = R i • y ci i or h γi i = S i • z ci i then it returns 0, else 1.
Theorem 1. The NIZKP LogEq n is a proof of knowledge, moreover it is complete, sound, and zero-knowledge in the random oracle model.

The proof of this theorem is a direct implication of [START_REF] Chaum | Wallet databases with observers[END_REF], [START_REF] Cramer | Proofs of partial knowledge and simplified design of witness hiding protocols[END_REF] and [START_REF] Fiat | Advances in Cryptology -CRYPTO' 86: Proceedings, chapter How To Prove Yourself: Practical Solutions to Identification and Signature Problems[END_REF]. Using this proof system, we build our VRS scheme called EVeR: Theorem 2. EVeR is unforgeable, anonymous, accountable and non-seizable under the DDH assumption in the random oracle model.

We give the intuition of these properties, the proof of the theorem is given in the full version of this paper [START_REF] Bultel | Unlinkable and strongly accountable sanitizable signatures from verifiable ring signatures[END_REF]: Unforgeability: The scheme is unforgeable since nobody can prove that log g (pk l ) = log h (z) without the knowledge of sk = log h (z). Anonymity: Breaking the anonymity of such a signature is equivalent to breaking the DDH assumption. Indeed, to link a signature z = h sk with the corresponding public key of Alice pk = g sk , an attacker must solve the DDH problem on the instance (pk, h, z). Moreover, note that since the value r randomizes the signature, it is not possible to link two signatures of the same message produced by Alice. Accountability: To break the accountability, an adversary must forge a valid signature (i.e. to prove that there exists pk l in the group such that log g (pk l ) = log h (z)) and to prove that he is not the signer (i.e. log g (pk) = log h (z) where pk is the public key chosen by the adversary). However, since the adversary does not know the secret keys of the other members of the group, he would have to break the soundness of LogEq to win the experiment, which is not possible. Non-seizable: (non-sei-1) no adversary is able to forge a proof that it is the signer of a signature produced by another user since it is equivalent to proving a false statement using a sound NIZKP. (non-sei-2) the proof algorithm run by a honest user with the public key pk returns a proof that this user is the signer of a given signature only if log g (pk) = log h (z). Since no adversary is able to compute z such that log g (pk) = log h (z) without the corresponding secret key, no adversary is able to break the non-seizability of EvER.

To sanitize this signature σ = (σ 1 , σ 2 ), the sanitizer chooses an admissible message m according to ADM (i.e. m and m have the same fixed part). Then he anonymously signs m together with σ 1 using the VRS for the group L = {pk v , spk} using the secret key ssk. We denote by σ 2 this signature. The final sanitized signature is σ = (σ 1 , σ 2 ). Theorem 3. For any deterministic and unforgeable DS scheme D and any unforgeable, anonymous, accountable and non-seizable VRS scheme V , GUSS instantiated with (D, V ) is immutable, transparent, strongly accountable and unlinkable.

We give the intuition of these properties, the proof of the theorem is given in the full version of this paper [START_REF] Bultel | Unlinkable and strongly accountable sanitizable signatures from verifiable ring signatures[END_REF]: Transparency: According to the anonymity of σ 2 and σ 2 , nobody can guess if a signature comes from the signer or the sanitizer, and since both signatures have the same structure, nobody can guess whether a signature is sanitized or not. Immutability: Since it is produced by a unforgeable DS scheme, nobody can forge the signature σ 1 of the fixed part M without the signer secret key. Thus the sanitizer cannot change the fixed part of the signatures. Moreover, since σ 1 signs the public key of the sanitizer in addition to M , the other users cannot forge a signature of an admissible message using σ 1 . Unlinkability: An adversary knows (i) two signatures σ 0 and σ 1 that have the same fixed part M according to the same function ADM for the same sanitizer and (ii) the sanitized signature σ = (σ 1 , σ 2 ) computed from σ b for a given admissible message m and an unknown bit b. To achieve unlinkability, it must be hard to guess b. Since the DS scheme is deterministic, the two signatures σ 0 = (σ 0 1 , σ 0 2 ) and σ 1 = (σ 1 1 , σ 1 2 ) have the same first part (i.e. σ 0 1 = σ 1 1 ). As it was shown before, the σ has the same first part σ 1 as the original one, thus σ 1 = σ 0 1 = σ 1 1 and σ 1 leaks no information about b. On the other hand, the second part of the sanitized signature σ 2 is computed from the modified message m and the first part of the original signature. Since σ 0 1 = σ 1 1 , we deduce that σ 2 leaks no information about b. Finally, the best strategy of the adversary is to randomly guess b. (Strong) Accountability: the signer must be able to prove the provenance of a signature.

It is equivalent to breaking the anonymity of the second parts σ 2 of this signature: if it was created by the signer then it is the original signature, else it was created by the sanitizer and it is a sanitized signature. By definition, the VRS scheme used to generate σ 2 provides a way to prove whether a user is the author of a signature or not. GUSS uses it in its proof algorithm to achieve accountability. Note that since the sanitizer uses the same VRS scheme to sanitize a signature, he also can prove the origin of a given signature to achieve the strong accountability.

Conclusion

In this paper, we revisit the notion of verifiable ring signatures. We improve its properties of verifiability, we give a security model for this primitive and we design a simple, efficient and secure scheme named EvER. We extend the security model of sanitizable signatures in order to allow the sanitizer to prove the origin of a signature. Finally, we design a generic unlinkable sanitizable signature scheme named GUSS based on verifiable ring signatures. This scheme is twice as efficient as the best scheme of the literature. In the future, we aim at finding other applications for the verifiable ring signatures that require our security properties.

Acknowledgement

We acknowledge Dominique Schröder for his helpful comments and feedback on our paper. the signer and the sanitize sk, pk, ssk and spk, the size of a signature σ and the size of a proof π (second table). We ommit the complexity of the algorithms SaProof and SaJudge since these algorithms are similar to SiProof and SiJudge. The first line corresponds to the generic case, where the values depend on the chosen signature scheme and the chosen verifiable ring signature scheme. The second line corresponds to the case where GUSS is instantiated with Schnorr and EVeR.

GUSS

Fig. 1 .

 1 Fig. 1. Comparison of GUSS and the scheme of Fleischhacker et al.:The first six columns give the number of exponentiations of each algorithms of both schemes, namely the key generation algorithm of the signer (SiGen) and the sanitizer (SaGen), the signature algorithm (Sig), the verification algorithm (Ver), the sanitize algorithm (San), the proof algorithm (SiProof) and the judge algorithm (SiJudge). The last six columns give respectively the size of the public key of the signer (pk) and the sanitizer (spk), the size of the secret key of the signer (sk) and the sanitizer (ssk), the size of a signature (σ) and the size of a proof (π) outputted by SiProof. This size is measured in elements of a group G of prime order. As in[START_REF] Fleischhacker | Efficient unlinkable sanitizable signatures from signatures with re-randomizable keys[END_REF], for the sake of clarity, we do not distinguish between elements of G and elements of Z * p . We consider the best instantiation of the scheme of Fleischhacker et al. given in[START_REF] Fleischhacker | Efficient unlinkable sanitizable signatures from signatures with re-randomizable keys[END_REF]. In Appendix A, we give a detailed complexity evaluation of our schemes.

Definition 2 (

 2 (Deterministic) Digital Signature (DS)). A Digital Signature scheme S = (D.Init, D.Gen, D.Sig, D.Ver) is a tuple of four algorithms defined as follows: D.Init(1 k ): It returns a setup value set. D.Gen(set): It returns a pair of signer public/private keys (pk, sk). D.Sig(m, sk): It returns a signature σ of m using the key sk. D.Ver(pk, m, σ): It returns a bit b.

  (1 k ): It returns a setup value set. V.Gen(set): It returns a pair of signer public/private keys (pk, sk). V.Sig(L, m, sk): This algorithm computes a signature σ using the key sk for the message m according to the set of public keys L. V.Ver(L, m, σ): It returns a bit b: if the signature σ of m is valid according to the set of public key L then b = 1, else b = 0. V.Proof(L, m, σ, pk, sk): It returns a proof π for the signature σ of m according to the set of public key L. V.Judge(L, m, σ, pk, π): It returns a bit b or the bottom symbol ⊥: if b = 1 (resp. 0)

  and (V.Ver(L * , σ * , m * ) = 1) and (V.Judge(L * , m * , σ * , pk * , π * ) = 0) and (∀ i ∈ 1, qS , σi = σ * ) then return 1, else return 0

  Ver(L * , σ * , m * ) = 1) and (V.Judge(L * , m * , σ * , pk * , π * ) = 0) and (∀ i ∈ 1, qS , σi = σ * ) then return 1, else return 0

Scheme 3 (

 3 Scheme 3 (Efficient Verifiable Ring Signature (EVeR)) EVeR is a VRS defined by: V.Init(1 k ): It generates a prime order group setup (G, p, g) and a hash function H : {0, 1} * → G. It returns the setup set = (G, p, g, H). V.Gen(set): It picks sk $ ← Z * p , computes pk = g sk and returns a pair of signer public/private keys (pk, sk). V.Sig(L, m, sk): It picks r $ ← Z * p , it computes h = H(m||r) and z = h sk , it runs P ← LEprove |L| ({(h, z, g, pk l )} pk l ∈L , sk) and returns σ = (r, z, P ). V.Ver(L, m, σ): It parses σ = (r, z, P ), computes h = H(m||r) and returns b ← LEverif |L| ({(h, z, g, pk l )} pk l ∈L , P ). V.Proof(L, m, σ, pk, sk): It parses σ = (r, z, P ), computes h = H(m||r) and z = h sk , runs P ← LEprove 1 ({(h, z, g, pk)}, sk) and returns π = (z, P ). V.Judge(L, m, σ, pk, π): It parses σ = (r, z, P ) and π = (z, P ), computes h = H(m||r) and runs b ← LEverif 1 ({(h, z, g, pk)}, π). If b = 1 then it returns ⊥. Else, if z = z then it returns 1, else it returns 0.

  Gen + V.Gen V.Gen D.Sig + V.Sig 2 V.Sig 2 D.Ver + V.Ver2 V.Proof Judge skEV + sk Sh pk EV + pk Sh skEV pk EV σ EV Fig.5. Complexity analysis of GUSS (Scheme 4).

		SiGen	SaGen	Sig	San	Ver	SiProof
	generic D.EvER and Schnorr	2	1	8	7	10	3
	GUSS	SiJudge	sk	pk	ssk spk	σ	π
	generic	V.2	+ σ Sc π EV 2
	EvER and Schnorr	4	2	2	1	1	12	5

This research was conducted with the support of the "Digital Trust" Chair from the University of Auvergne Foundation.

6 Our Unlinkable Sanitizable Signature Scheme: GUSS We present our USS instantiated by a digital signature (DS) scheme and a VRS. Scheme 4 (Generic Unlinkable Sanitizable Signature (GUSS)) Let D be a deterministic digital signature scheme such that D = (D.Init, D.Gen, D.Sig, D.Ver) and V be a verifiable ring signature scheme such that V = (V.Init, V.Gen, V.Sig, V.Ver, V.Proof, V.Judge). GUSS instantiated with (D, V ) is a sanitizable signature scheme defined by the following algorithms: The signer secret key sk = (sk d , sk v ) contains a secret key sk d compatible with the DS scheme and a secret key sk v compatible with the VRS scheme. The signer public key pk = (pk d , pk v ) contains the two corresponding public keys. The sanitizer public/secret key pair (spk, ssk) is generated as in the VRS scheme.

Let m be a message and M be the fixed part chosen by the signer according to the admissible function ADM. To sign m, the signer first signs M together with the public key of the sanitizer spk and the admissible function ADM using the DS scheme. We denote this signature by σ 1 . The signer then signs in σ 2 the full message m together with σ 1 using the VRS scheme for the set of public keys L = {pk v , spk}. Informally, he anonymously signs (σ 1 ||m) within a group of two users: the signer and the sanitizer. The final sanitizable signature is σ = (σ 1 , σ 2 ). The verification algorithm works in two steps: it verifies the signature σ 1 and it verifies the anonymous signature σ 2 .

A Algorithms Complexity

In this section, we detail the complexity of the algorithms of our schemes. More precisely, we give the number of exponentiations in a prime order group for each algorithm. Since our schemes are pairing free, this is the main operation. Moreover, we give the size of some values outputted by these algorithms (keys, signatures and proofs). This size is given in the number of elements of a group of prime order p. For the sake of clarity, we do not distinguish between elements of a group G of prime order p where the DDH assumption is hard and elements of Z * p . In Figure 2, we give the number of exponentiations of each algorithm of Schnorr's signature, and we give the size of the secret/public keys sk Sh and pk Sh and the size of a signature σ Sh . In Figure 3, we give the number of exponentiations of each algorithm of the LogEq n proof system and the size of a proof π LE n depending to the number n. The first line corresponds to the general case, the two other lines correspond to the case where n = 1 and n = 2.

Fig. 3. Complexity analysis of LogEq (Scheme 2).

Fig. 4. Complexity analysis of EVeR (Scheme 3).

In Figure 4, we give the number of exponentiations of each algorithm of the EVeR verifiable ring signature scheme (first table) and the size the secret/public keys sk EV and pk EV , the size of a signature σ EV n and the size of a proof π EV n (second table ). These values depend on the size of the ring n. The first line corresponds to the generic case, where the values depend on the chosen proof system. The second line corresponds to the case where n = 2 and where the proof system is LogEq 2 .

In Figure 5, we give the number of exponentiations of each algorithm of the GUSS verifiable ring signature scheme (first table) and the size of the secret/public keys of


Noudjoud Kahya

Nacira Ghoualmi

Pascal Lafourcade

Formal Analysis of Key Management in mobile Wimax

Keywords: mobile Wimax, PKM, TEK, attack, analyze formal

The Mobile WiMAX IEEE 802.16e is a new technology supporting broadband wireless communication with fixed and mobile access. The standard offers high throughput broadband connections, supporting handover and roaming capabilities, and provides a security sub layer, which is responsible for secrecy, authentication and secure key exchange. In the area of security aspects, Mobile WiMAX exhibits vulnerabilities while adopting improved security architecture. Several versions of 802.16 networks were released. While the first versions have shown some security weaknesses that were later corrected by the recently released versions, the security mechanisms of 802.16 still remain vulnerable and the limited deployment of such technology is insufficient to satisfy the demands of security. This paper focuses on reducing the security vulnerabilities in the authorization protocol PKM and the generation of traffic encryption keys (TEKs). We propose the usage of 1. A formal analysis of the PKM protocol (authorization phase and exchange of TEKs phase) and 2.Device certificate for key exchange process to provide secure authentication and 3. Give a formal analysis of our new PKM protocol (authorization phase and exchange of TEKs phase). The formal analysis has been conducted using a specialized model checker Scyther, which provides formal proofs of the security protocol. The revised authentication protocol is expected to provide better secure platform for all process of PKM.

INTRODUCTION IEEE 802.16, commonly known as Worldwide

Interoperability for Microwave Access (WiMAX), is a recent wireless broadband standard that has promised high bandwidth over long-range transmission. In the past few years, the IEEE 802. [START_REF] Sebastian M¨odersheim | Ofmc: A symbolic modelchecker for security protocols[END_REF] working group has developed a number of standards for WiMAX. First published in 2001, the IEEE 802.16 standard specified a frequency range of 10-66 GHz with a theoretical maximum bandwidth of 120 Mb/s and maximum transmission range of 50 km. However, the initial standard only supports line-ofsight (LOS) transmission and thus does not seem to favor deployment in urban areas. A variant of the standard, IEEE 802.16a-2003, approved in April 2003, can support non-LOS (NLOS) transmission and adopts OFDM at the PHY layer. It also adds support for the 2-11GHz range. These two standards were further revised in 2004 (IEEE 802. . Recently, IEEE 802.16e has also been approved as the official standard for mobile applications.

In the IEEE 802.16 technology, security has been considered as the main issue during the design of the protocol. However, several design and security vulnerabilities were found in this technology. These vulnerabilities are the main cause to introduce unauthenticated messages which are susceptible to forgery, the unencrypted management communication which reveals important management information and it does not have perfect mechanism for mutual authentication; Previous works have addressed the necessity of mutual authentication as well as mechanisms to counter attacks on 802. [START_REF] Sebastian M¨odersheim | Ofmc: A symbolic modelchecker for security protocols[END_REF]. However, there are still some flaws in their protocols. Our paper analyzes those possible attacks to both BS (base station) and MS (mobile station), and proposes revised authentication protocol to solve those problems.

WIMAX OVERVIEW

In order to understand Wimax security issues, we first need to understand his architecture and how securities specifications are addressed in this technology.

A. Wimax Architecture IEEE 802.16 standard protocol stack consist of two layers: MAC (Medium Access Control) layer and PHY (Physical) layer. The MAC layer is subdivided into three sub-layer that is Convergence Sub-layer (CS), Common Part Sub-layer (CPS) and Security Sub-layer (SS) [START_REF]IEEE Standard for Local and Metropolitan Area Networks, Part 16: Air for Fixed and Mobile Broadband Wireless Access Systems, Amendment 2: Physical and Medium Access Control Layers for Combined Fixed and Mobile Operation in Licensed Bands and Amendment and Corrigendum to IEEE Std 802[END_REF].

Security Sub-layer lies between MAC CPS and Philae. This sub-layer is responsible for encryption and decryption of data traveling to and from the PHY layer, and it is also used for authentication and secure key exchange [START_REF] Rengaraju | Analysis on Mobile WiMAX Security[END_REF].

B. Security Scheme

In WIMAX, security has been included in the design of systems at the very start. To provide secure distribution of sensitive data from the BS to the MS and protect network services from attacks, Wimax applies strong support for authentication, key management, encryption and decryption, control and management of plain text protection and security protocol optimization. This sub layer performs three functions:

1-Authentication:Authentication is achieved using a public key interchange protocol that ensures not only authentication but also the establishment of encryption keys. Wimax defines Privacy Key Management (PKM) protocol in security sub-layer, which allows three types of authentication: The first type is RSA based authentication: RSA based authentication applies X.509 digital certificates together with RSA encryption. In this authentication mode, a BS authenticates the MS through its unique X.509 digital certificate that has been issued by the MS manufacturer. The X.509 certificate contains the MS's Public Key (PK) and its MAC address. When requesting an Authorization Key (AK), the MS sends its digital certificate to the BS, and then BS validates the certificate, uses the verified Public Key (PK) to encrypt an AK and sends back to the MS. All MSs that use RSA authentication have factory installed private/public key pairs together with factory installed X.509 certificates [START_REF] Xu | Attacks on PKM Protocols of IEEE 802.16 and Its Later Versions[END_REF]. The second type is EAP (Extensible Authentication Protocol) based authentication: In the case of EAP based authentication, the MS is authenticated either by an X.509 certificate or by a unique operatorissued credential such as a SIM or by username/password. There are three types of EAP: the first type is EAP-AKA (Authentication and Key Agreement) for SIM based authentication; the second type is EAP-TLS (Transport Layer Security) for X.509 based authentication; the third type is EAP-TTLS (Tunneled Transport Layer Security) for SS-CHAPv2 (Microsoft-Challenge Handshake Authentication Protocol) [START_REF] Xu | Attacks on PKM Protocols of IEEE 802.16 and Its Later Versions[END_REF]. The third type is RSA based authentication followed by EAP authentication.

2-Authorization:

This process follows the authentication process. MS requests for an AK and a SAID (Security Association ID) from BS by sending an Authorization Request message. This message includes the MS X.509 certificate, encryption algorithms and cryptographic ID. In response, the BS interacts with an AAA (Authentication, Authorization and Accounting) server to validate the request from the MS, and sends back an Authorization Reply which includes the AK encrypted with the MS's public key and a lifetime key and an SAID [3] [4].

3-Encryption:

The previous authentication and authorization process results in the assignment of and Authorization Key (AK), which is 160 bits long. The Key Encryption Key (KEK) derived directly from the AK and it is 128 bits long. The KEK are not used for encrypting traffic data; so MS require the Traffic Encryption Key (TEK) from BS. TEK is generated as a random number generating in the BS using the TEK encryption algorithm where KEK is used as the encryption key. TEK is then used for encrypting the data traffic. Many attacks are identified on authentication protocols PKM during mutual authentication. The potential attacks that can be carried out are man-inthe-middle, replay, interleaving and DoS attacks.

LITERATURE REVIEW

Few of relevant papers tackle the security issues of WIMAX network. T.Han and all [START_REF] Han | Analysis of Mobile WiMAX Security: Vulnerabilities and Solutions[END_REF], M.Rahman and M.Kowsar [START_REF] Sakibur Rahman | WiMAX Security Analysis and Enhancement[END_REF], M.Barbeau [START_REF] Barbeau | Wimax /802.16 Threat analysis[END_REF], M.Nasreldin and all [START_REF] Nasreldin | Wimax Security[END_REF], they give the most complete analysis of WIMAX security; they focused on the problem of IEEE 802. [START_REF] Sebastian M¨odersheim | Ofmc: A symbolic modelchecker for security protocols[END_REF].The purpose of this literature review is to study the literature of WiMAX/802.16. The review is of security mechanisms for this technology and his security threats, which are described in certain papers by different authors. [START_REF] Han | Potential Denial of Service Attacks in IEEE802.16e-2005 Networks[END_REF] This paper presents one of the possible attacks namely the denial of service attacks on the IEEE 802.16e-2005 mobile wimax networks.

-DoS attacks on IEEE 802.16e.

The authors Simulation of DoS attacks and they show that a DoS attack exploiting the design of RNG-RSP messages is devastating the overall service levels of the wimax network.

Fang-Yie Leu, Yi-Fung Huang, Chao-Hong Chiu 2010 [START_REF] Leu | Improving security levels of IEEE802.16e authentication by Involving Diffie-Hellman PKDS[END_REF] The authors propose an authentication key management approach, called Diffie-Hellman-PKDS-based authentication method (DiHam) to improve current security level of facility authentication between IEEE802.16e's BS and SS by using a secret door asymmetric one-way function, PKDS. Dos/DDoS attack and a man-in-the-middle attack launched by a fake BS or SS during the network authentication phase.

In this article, the authors focus on the lift of the security level of the WiMax authentication, and develop an authentication mechanism to improve WiMax facility authentication by employing an integrated system that integrates the DH-PKDS and the DiHam, and in which a two-way authentication instead of the unidirectional authentication of PKMv1 is used. Ramanpreet Singh, Sukhwinder Singh 2011 [START_REF] Singh | Detection of Rogue Base Station Using MATLAB[END_REF] Ramanpreet Singh and Sukhwinder Singh have thought of the problem of detecting rogue base station in WiMAX/802.16 networks. A rogue base station duplicates a legitimate base station and so it is considered as attacker station. The rogue base station puzzles a collection of subscribers who attempt to get service that they believe to be a legitimate base station and it may lead to disturbance in service. The strategy of attack depends on the kind of network.

Attack of The rogue base station.

Their approach was based on the received signal strength (RSS) reports received by mobile stations and inconsistencies in sensitivity can be seen if a rogue Base Station (BS) is present in a network. These reports are assessed by the legitimate base stations, for example, when a mobile station undertakes a handover towards another BS. A new algorithm for detecting a rogue base station was described in this paper [START_REF] Leu | Improving security levels of IEEE802.16e authentication by Involving Diffie-Hellman PKDS[END_REF].

Shahid

Hussain, Muhammad Naeem Khan, Muhammad Ibrahim 2012 [START_REF] Hussain | A Security Architecture for Wimax Networks[END_REF] They The version of the PKM protocol, which will be described below, is that defined for use in the IEEE 802. standard. This version was later extended to cope with mobility in the IEEE 802.16e standard.

PKM is a three-phase based protocol. The remaining part of this section describes each of these phases [START_REF] Tang | Sharif[END_REF] [START_REF] Prasad L Fernando | WiMAX Networks, Techno-Economic Vision and Challenges[END_REF].

A-PKM Authorization [14][15]

The first phase of the PKM is the process of authorizing the MS by the BS.

To connect with the BS, the MS sends an authentication message (AuthenticationInfMess) containing the certificate of MS vendor. Immediately after that, the MS sends an authorization Request Message (AuthorizationReqMess) to the attached BS, requesting an Authorization Key (AK). This information will be used as a shared secret. The message contains the following information:

• The MS certificate.• A description of the cryptographic capabilities supported by the MS. • The security association identifier (SAID) of the MS's primary SA. This value is equal to the primary 16-bit Connection Identifier (CID) that the MS receives from the BS during the network entry and the initialization phase.

The MS will be authorized based on the verification of its certificate. The public key contained in the certificate will be used for constructing the third message. The BS verifies also whether it supports one or more of the cryptographic capabilities of the MS. The response of the BS to the MS is described by message 3 (AuthorizationRepMess). It contains:

• The Authorization Key (AK) generated by the BS and encrypted using the MS public key contained in its certificate. A proper use of this AK shows an authorization regarding the access of the WiMAX channel. • A 4-bit AK sequence number to differentiate between the consecutive Authorization Keys.• The AK life time value.• The SAIDs descriptor(s) as the identity and properties of the primary SA and zero or more existing static SAs for which the MS may be authorized to get the keying information. B-Exchange of TEKs [START_REF] Tang | Sharif[END_REF] [START_REF] Prasad L Fernando | WiMAX Networks, Techno-Economic Vision and Challenges[END_REF] The aim of the second phase of the PKM protocol is to initiate the exchange of TEKs, and establish a data SA. The TEKs will be later used for encryption. As stated previously, the authorizationRepMess message contains, in addition to the SAID and properties of the SA, from zero to several static SAs for which the MS is authorized to obtain the key material. Therefore, the MS starts, in this phase, a separate state machine for each of the SAID identified in the authorizationRepMess message.

Last message is from BS in reply to MS containing the Authorization Key (AK) encrypted with MS's public key along with sequence number, life time of AK and Security Association Identity List (SAID list).

Every state machine is responsible for managing the keying material associated with the related SAIDs.

Every MS sends periodically a Key Request Message (KReqMess) to the BS, asking it for the renewal of the TEK. This message is composed of:

• the AK sequence number which allows the BS to determine the Uplink HMAC Key used by the SS to generate the HMAC digest of this message;• the SAID related to the SA whose keying material is requested. This SAID is related to the started TEK state machine; • the HMAC digest produced by the application of the HMAC function on the message payload using the Uplink HMAC Key.

After making sure that the received SAID matches the SA at the MS and verifying the authenticity and the integrity of the KReqMess message by checking the HMAC digest, the BS responds to that message. It sends a key Reply Message (KRepMess) containing the new key material needed by the TEK state machine. At any time, the BS maintains two active key materials per SAID, which are denoted by TEK-Parameters in the KRepMess. A keying material includes:

• TEK encrypted with the KEKs using either the 3DES in EDE mode with 128 bits, RSA PKCS#1, or AES in ECB mode with 128 bits;• the remaining lifetime of the TEK;• the TEK sequence number;• a 64-bit initialization vector. The KRepMess message contains an AK sequence number, the SAID, the parameters related to the old TEK and the new TEK and an HMAC digest to ensure the MS that the message is sent by the BS without being tampered with. Note that the validity durations of the two TEKs overlap. In fact, the new TEK is being activated before the old TEK expires and the old TEK is destroyed after the activation of the new TEK. The lifetime of a TEK is also used by the MS to estimate when the BS will invalidate a previous TEK or request a new TEK.

C-Data Encryption [14][15]

After achieving the SA authorization and the TEK exchange, transmitted data between the MS and BS starts to be encrypted using the TEK. An encryption algorithm is used to encipher the MAC PDU. Note that, neither the CRC nor the MAC header is involved in encryption in order to guarantee the forwarding of the MAC PDU and support diverse services. In the MAC header, an Encryption Control (EC) field is set to 1 as an indication regarding the availability of an encrypted MPDS. In addition, the 2-bits Encryption Key Sequence (EKS) field indicates the used TEK. Encryption can be done by means of the Data Encryption Standard (DES) using Cipher Block Chaining (CBC) mode with 56 bits.

FORMAL ANALYSIS OF PKM USING SCYTHER TOOL

There are numerous robust tools available for formal security protocol analysis such as OFMC [START_REF] Sebastian M¨odersheim | Ofmc: A symbolic modelchecker for security protocols[END_REF], Scyther [START_REF] Cremers | The Scyther Tool: Verification, falsification, and analysis ofsecurity protocols[END_REF], and ProVerif [START_REF] Blanchet | An efficient cryptographic protocol verifier based on Prologrules[END_REF].

Scyther is a formal protocol analysis tool, for the symbolic automatic analysis of the security properties of cryptographic protocols (typically confidentiality or variants of authenticity). It assumes perfect cryptography, meaning that an attacker gains no information from an encrypted message unless she knows the decryption key. Scyther takes as input a role-based description of a protocol in which the intended security properties are specified using claims. Claims are of the form claim (Principal, Claim, Parameter), where Principal is the user's name, Claim is a security property (such as 'secret'), and Parameter is the term for which the security property is checked. This section describes the main security weakness related the PKM standard, showing potential attacks in authorization phase and exchange of TEKs phase.

Similar to the approach taken by our analysis of PKM v1/v2 [START_REF] Kahya | Secure key management protocol in wimax[END_REF] [20], we contains the retrace and we formally verify our analysis on different phases of PKM protocols using scyther. In the end of this section we describe the proposed protocol and we discuss the obtained results.

D-Properties Specifications

Authenticity, confidentiality, access control, secrecy and uniqueness of the keys and freshly of message are selected for formal verification.

1) Authenticity:

The principals (MS/BS) verify the authenticity of received messages (by verifying signatures or MACs). In order to fulfill authenticity the MAC address of the Meshach identifies it must remain secret. The MAC address is included in the MS's certificate (SsCert). The formal definition of authenticity is given below [20] [21].

Property 1: 𝑐𝑙𝑎𝑖𝑚(𝑆𝑆, 𝑆𝑒𝑐𝑟𝑒𝑡, 𝑆𝑆𝐶𝑒𝑟𝑡)

2) Confidentiality: Expresses that certain information is not revealed to an intruder. The security satisfied if the MS has the guarantee that all exchanged user data to BS is secret. The formalization of information confidentiality is given below [20] [21].

Property 2:∀∝∈ 𝑀𝑠𝑔(𝑐𝑙𝑎𝑖𝑚 𝑆𝑆, 𝑆𝑒𝑐𝑟𝑒𝑡, ∝ )

3) Access control: This claim is fulfilled if the BS has the guarantee that, neither an unauthenticated user should gain access to the services provided, nor should an unauthenticated user be able to impersonate another user. A service should always be bound to an authenticated user. Its formal definition is given as follows [START_REF] Kahya | Key management protocol in wimax revisited[END_REF] [21]:

Property 3: ∀∝∈ 𝑀𝑠𝑔(𝑐𝑙𝑎𝑖𝑚 𝐵𝑆, 𝑆𝑒𝑐𝑟𝑒𝑡, ∝ )

4) Secrecy and uniqueness of the session keys:

This claim is fulfilled if the BS and the MS have the guarantee that all exchanged keys (AK and TEK) are secret and unique.

Property 4:∀𝑘𝑒𝑦(𝑐𝑙𝑎𝑖𝑚 𝐵𝑆 𝑆𝑆, 𝑆𝑒𝑐𝑟𝑒𝑡, 𝑘𝑒𝑦 )

5) Freshly of messages: An important part of security protocols is the generation of fresh values which are used for challenge-response mechanisms (often called nonce's), or as session keys. This claim is fulfilled if the BS and MS have the guarantee that the session key is fresh [START_REF] Kahya | Key management protocol in wimax revisited[END_REF] [START_REF] Taha1 | Sofiène Tahar Formal Verification of IEEE 802.16 Security Sublayer Using Scyther Tool 2009 ESR Groups France[END_REF].

Property 5: (𝑐𝑙𝑎𝑖𝑚 𝐵𝑆 𝑆𝑆, 𝐹𝑟𝑒𝑠ℎ, 𝑘𝑒𝑦 )

A. Formal Verification

Pseudonymity, information confidentiality, no theft of service and secrecy and uniqueness of the session keys are selected for formal verification, we apply Scyther tool to verify if this properties are proved or not in PKM protocol.

Our analysis reveals that the phases of Key Management Protocol PKM are vulnerable into many attacks; these attacks fall into the following categories: replay, DoS, Man-in-the middle attacks.

1. Property 1: Scyther detected a possible attack, as an intruder eavesdrops the second message and obtains the MS's certificate (MsCert). 2. Property 2: Scyther detected a possible Authenticity attack. Message2 is sent in plaintext so an intruder eavesdrop this message and obtains the SS's certificate (MsCert). BS may face a replay attack from a malicious SS who intercepts and saves or modified the authentication messages sent by a legal MS previously.

Property 3:

It is proved that unauthenticated user cannot access the services provided, and cannot impersonate another user. The BS uses the certificate of the MS to determine if the MS is authorized, then sends the AK encrypted with the public key of the MS. This guarantees that only the specific MS can decrypt the AK. 4. Property and 5: It is proved that an adversary cannot obtain the unique AK as it is encrypted with the public key of the MS. AK is proved to be unique using synchronization claim and the fact that AK is a constant in one of the roles appearing only in one send event.

After the MS authentication procedure has been done, the AK is used to derive KEK and HMACkey. TEK is then generated by BS randomly. The TEK is the key actually used to encrypt data traffic exchanged between the BS and MS. A key exchange message is authenticated by HMAC-SHA1 to provide message integrity and AK confirmation. It is proved that an adversary cannot obtain the unique TEK.

Similar to the authorization protocol, the exchange of TEKs phase of the PKM is vulnerable to the replay attack. If an attacker replays the first message, the BS will assign and send new keying material using a KRepMess message. The legitimate MS, which is not aware of the attack, will think that it is the BS which requested the rekeying and sent the first optional message. As a consequence, this attack causes both the MS and BS to exchange keying material without intending to.

As seen in the formal analysis, the secrecy and uniqueness of the keying material distributed and the no theft of service possible claims are valid in both phases of PKM. However, pseudonymity and information confidentiality are broken.

THE PROPOSED REVISED AUTHENTICATIONPROTOCOL

As discussed in the previous section, the existing protocol does not fulfill the claims pseudonymity and information confidentiality because it still vulnerable to replay, DoS and Man-in-the-middle. Some solutions are introduced to solve those problems in our new revised protocol. To prevent replay and man-in-the-middle attacks we add timestamp. The problem with timestamp is that it requires time synchronization between MS and BS. In the wireless scenario, time synchronization is considered to be difficult (particularly under mobility). But In IEEE 802.16(e), it is assumed that time synchronization is done between MS and BS.

Nonce is a possible alternative to timestamps for use in the authentication protocols. Nonce shows that the request queued were not used before. Timestamp identifies which request are the newer one and also the time sent by the MS and BS. Nonce will not give any information about the time that was sent. Nonce is also not sufficient to tell the BS that it is the current message received from the MS. There are two problems with the protocol that has timestamps only. An adversary can easily capture the timestamp of MS by listening to message 2. The time adjustment can be done by the adversary accordingly. Hence the scope of man in middle attack is persists with timestamp added protocol. To prevent security threats like replay attacks, DoS attack and Man-in the-middle attack, both nonce and time stamp are needed. So the revised protocol has the timestamp attached with the MS message to the BS along with the nonce.

The protocol is shown as follows:

-SS/MS and BS send a message to find an X.509 certificate and it own public key information onto the server CA.

Formal analysis of the revised authentication protocol

In this section, we formally verify our analysis on all phases of PKM protocols, and the correctness of our reversion. The revised authentication protocol is going to be challenged with the following requirements using the Scyther tool.

1. Property 1: In the formal analysis, it is proved that an intruder cannot obtain the MS certificate (MsCert).

Property 2:

In the formal analysis it is proved that the authorization key exchanged in the authentication protocol is secret and not broken. 3. Property 3: It is proved that unauthenticated user cannot access the services provided, and cannot impersonate another user. Also, it is not possible to modify the data by an unauthorized individual. 4. Property 4 and 5: It is proved that an adversary cannot obtain the unique pre-PAK and the TEK is secured Timestamp and nonce are used in the revised protocol to prevent replay and man-in-themiddle attack. The MS appends the time stamp and nonce. This helps the BS to identify the request as a newer one. The nonce will wipe out the possibility of replay attack.

The nonce helps the BS to identify successive requests and it enhances the BS capacity to reject those requests which was sent by the intruders or adversaries. BS, thus, can identify the latest requests and it is able to filter out samples of replay attacks. In stapes authorization reply message, the BS sends the time stamp and nonce of MS. That helps in preventing an adversary from forging a BS. This protocol also provides mutual authentication. The nonce value sent by the BS helps in preventing the man-in-the middle attack.

The timestamp helps the BS in identifying the latest requests, which prevents reply attacks. It also helps the MS to identify the recent messages, and hence it can identify the AK used by the MS as new or not. The addition of nonce from the BS helps the MS to identify whether the message which he received with pre AK is a newer one or not. It is better to add more buffers to carry the used nonce values in the previous sessions. This gives more security to the BS and user MS.

Similar to the authorization phase, the nonce and timestamp helps the MS and BS to prevent replay attacks in the exchange of TEKs phase. However, several design and security vulnerabilities were found in this technology. In this paper we focused on the PKM protocol which is directly associated with the key management procedures of IEEE 802.16. Concentrating on PKMv2, several aspects of PKM functionality were examined including initial authorization /authentication between a BS and MS, key derivation. As discussed in this paper, PKM protocol vulnerable to replay, DoS and Man-in-the-middle attacks. Some solutions are introduced to solve those problems in our new protocol by using nonce and timestamp together. The revised authentication protocol ensures secure end-to-end data transmissions for all process of PKM.

  4. PKM PROTOCOLSecurity of connections access in WiMAX is done with respect to the Privacy Key Management (PKM) protocol. The protocol is responsible for the normal and periodical authorization of SSs and distribution of key material to them, as well as reauthorization and key refresh. It also manages the application of the supported encryption and authentication algorithms to the exchanged MAC Protocol Data Units (MPDUs).

Fig 1 :Fig 2 :

 12 Fig 1 : PKM Authorization [14]

  In the IEEE 802.16 technology, security has been considered as the main issue during the design of the protocol.

Table 1 contains the tabular format of a summarized review of the literature. What are the challenges to the WiMAX? And what are the solutions for these challenges. Every author has its own view.

 1

	Author		Summary	Problems/Challenges		Solution
	Michel	Barbeau	An analysis of the security attacks on	-	Jamming,	-	Communication keys should be secure
	2005[7]			the wimax and architecture has been	Screambling, -DDOS, -	mutual authentication needed.
				conducted. Focus is on the threats	Rouge BS, -X.509 digital
				analysis of physical and Mac layer.	certificate compromised.
	M. Nasreldin, H.	An analysis of threats according to the	-	Eavesdropping	of	Strong authentication technique for SS
	Aslan,	M.	El-	level of risk to IEEE 802.16. These	management message. -	and mutual authentication for BS.
	Hennawy, A. El-	threats were classified.	Rouge BS. -DOS, -	Spread spectrum scheme. Intrusion
	Hennawy. 2008 [8]		Jamming attack.		Prevention System.
	Tao Han, Ning	The paper is an overview of security	-	Man-in-the-middle	Propose Secure Initial Nenvork Entry
	Zhang,	Kaiming	architecture of mobile WiMAX	attacks. -RNG-RSP DoS	Protocol	(SINEP)	based	on
	Liu, Bihua Tang,	network. He investigates man-in-the-	attack. -DoS attacks.		DiffieHellman (DB) key exchange
	Yuan'an Liu2009 [5]	middle attacks and Denial of Service				protocol to enhance the security level
				(DoS) attacks toward 802.16e-based