Tristan Ninet
email: tristan.ninet@inria.fr

Axel Legay
email: axel.legay@uclouvain.be

Romaric Maillard
email: romaric.maillard@thalesgroup.com

Louis-Marie Traonouez
email: louis-marie.traonouez@inria.fr

Olivier Zendra
email: olivier.zendra@inria.fr

Model Checking the IKEv2 Protocol Using Spin

Previous analyses of IKEv2 concluded that the protocol was suffering from two authentication vulnerabilities: the penultimate authentication flaw and a vulnerability that leads to a reflection attack. In this paper we analyze the IKEv2 protocol specification using the Spin model checker. To do so we extend and improve an existing modeling method that allows analyzing security protocols using Spin. For completeness we indicate each abstraction we make when writing the model. As a result we show that the reflection attack is actually not applicable. We further discuss two modifications of the protocol and prove that both of them do overcome the vulnerability the penultimate authentication flaw.

I. Introduction

Internet Key Exchange version 2 (IKEv2) is the authenticated key-exchange protocol used in the Internet Protocol security architecture (IPsec). A security protocol such as IKEv2 can suffer from two types of vulnerabilities: specification vulnerabilities and implementation vulnerabilities.

An appropriate approach to avoid implementation vulnerabilities is to use modern automated testing techniques like fuzzing. As a matter of fact, the developers of the strongSwan IKEv2 implementation have recently announced [1] that part of their code base is now fuzzed using Google's OSS-Fuzz [16] infrastructure. Fuzzing is an active research field in which a lot of progress has been made, e.g. by embracing additional techniques such as symbolic execution.

A specification vulnerability is inherent to the protocol itself and cannot be fixed by any change in the implementation. An efficient way to find specification vulnerabilities is to use automated techniques, such as model checking. Model checking allows to detect specification flaws in early stages of the development process, which in turn reduces total cost of solving the flaws. Furthermore, model checking is an exhaustive technique: it can formally prove that a protocol specification model meets its goals. Finally, security protocols are often too complex to rely only upon human understanding: IKEv2 is made of sixteen different payloads and even more substructures and fields. IKEv2 contains a mechanism of rekeying, which negotiates the secret keys periodically. It is designed so as to work even in the presence of Network Address Translation (NAT) between the peers. IKEv2 specifies not less than twentynine types of notification and error messages. Facing such a complexity, it seems sound to use an automated process to verify IKEv2.

Model checking has been used, to our knowledge, twice to analyze IKEv1 [START_REF] Meadows | Analysis of the Internet Key Exchange protocol using the NRL Protocol Analyzer[END_REF][START_REF] Cremers | Key exchange in IPsec revisited: Formal analysis of IKEv1 and IKEv2[END_REF] and three times to analyze IKEv2 [START_REF]Deliverable D6.2: Specification of the Problems in the High-Level Specification Language[END_REF][START_REF] Küsters | Using ProVerif to Analyze Protocols with Diffie-Hellman Exponentiation[END_REF][START_REF] Cremers | Key exchange in IPsec revisited: Formal analysis of IKEv1 and IKEv2[END_REF]. Tools that were used are NRL [START_REF] Meadows | The NRL Protocol Analyzer: An Overview[END_REF], OFMC [START_REF] Basin | An On-the-Fly Model-Checker for Security Protocol Analysis[END_REF], Scyther [START_REF] Joseph | Scyther: Semantics and verification of security protocols[END_REF] and DH-ProVerif [START_REF] Küsters | Using ProVerif to Analyze Protocols with Diffie-Hellman Exponentiation[END_REF]. It revealed two authentication vulnerabilities that were found in both IKEv1 and IKEv2: the penultimate authentication flaw and the reflection attack.

In this paper, we start by formally describing IKEv2's payloads in Section II. We further give some background on model checking security protocols, previous analyses of IKEv2, and the Spin model checker in Section III. We then analyze IKEv2 using Spin. To our knowledge it is the first time that Spin is used to analyze such a complex protocol. To do so, we extend and improve the method of Ben Henda [START_REF] Ben | Generic and efficient attacker models in spin[END_REF] for modeling protocols in Promela (Spin's modeling language). We present our IKEv2 model in section IV, and provide its source code so that it can be reused. We explain that Spin is not the most appropriate tool for analyzing security protocols. Other tools such as ProVerif [START_REF] Blanchet | An efficient cryptographic protocol verifier based on prolog rules[END_REF] and Tamarin [START_REF] Meier | The TAMARIN Prover for the Symbolic Analysis of Security Protocols[END_REF] offer more realistic models.

Our results, detailed in Section V, confirm the penultimate authentication flaw, but show that the reflection attack has no practical existence against IKEv2. The model of [START_REF] Cremers | Key exchange in IPsec revisited: Formal analysis of IKEv1 and IKEv2[END_REF], which reported the vulnerability, was missing some payloads that actually prevent the attack. Finally, we discuss in Section VI two possible modifications of the protocol, and formally prove using model checking that each of them eliminates the penultimate authentication flaw.

II. The IKEv2 protocol

The IKEv2 specification [START_REF] Kaufman | Internet key exchange protocol version 2 (IKEv2)[END_REF] is managed by the Internet Engineering Task Force (IETF). The goal of IKEv2 is to allow two peers to dynamically negotiate cryptographic algorithms and material in order to set up an IPsec [START_REF] Kent | Security Architecture for the Internet Protocol[END_REF] security association (SA). A security association is a set of security parameters and keys which enables two peers to exchange protected traffic. IKEv2 consists of three main exchanges: IKE_SA_INIT, IKE_AUTH and CRE-ATE_CHILD_SA. During the IKE_SA_INIT exchange the two peers negotiate cryptographic algorithms and run a Diffie-Hellman protocol to generate a shared secret. Keying material derived from this secret will be used with the algorithms agreed upon to encrypt subsequent IKEv2 messages. The result of an IKE_SA_INIT is called an IKE SA. Once the IKE SA is initiated, the two peers perform

Initiator(i, r) Responder(r) hdr i1 , ke i , n i hdr r1 , ke r , n r {hdr i2 , {i, auth i } e k } c k {hdr r2 , {r, auth r } e k } c k msc IKEv2-Sig ke i = g xi hdr il = (rf il , if il , mid il ) ke r = g xr hdr rl = (rf rl , if rl , mid rl ) keymat = k auth r = {ke r , n r , n i , k, r} s prk(r) k = (ke i ) xr = (ke r ) xi auth i = {ke i , n i , n r , k, i} s prk(i)
Fig. 1. The IKEv2-Sig protocol. This is the first phase of IKEv2, using signature authentication method.

Initiator(i, r) Responder(i, r) mutual authentication using the IKE_AUTH exchange to deter Man-in-the-Middle attacks. This authentication can be based on either pre-shared keys or digital certificates. This IKE_AUTH exchange is also used to establish an initial IPsec SA. Subsequent IPsec SAs and IKE SAs will be created through the CREATE_CHILD_SA exchange (possibly replacing existing SAs for the purpose of rekeying). IKEv2 aims to guarantee mostly two security properties. First, that the keying material generated by the IKE_SA_INIT and CREATE_CHILD_SA exchanges is secret, i.e. is only known to the two parties involved. Second, that the parties involved are mutually authenticated: each party must prove that it really has the identity it pretends to have. In this paper, we use model checking to verify that IKEv2 actually satisfies these two properties.

{hdr i , {ke i , n i } e k } c k {hdr r , {ke r , n r } e k } c k msc IKEv2-Child hdr i = (rf i , if i , mid i ) hdr r = (rf r , if r , mid r ) keymat = (ke i ) xr = (ke r ) xi ke i = g xi ke r = g xr
To simplify the model checking process, we target specific parts of IKEv2. These parts constitute protocols on their own, so we call them subprotocols. We define the following ones: IKEv2-Sig consists of one IKE_SA_INIT exchange and one IKE_AUTH exchange. It uses digital signature authentication. IKEv2-PSK consists of one IKE_SA_INIT exchange and one IKE_AUTH exchange. It uses pre-shared key authentication. IKEv2-Child consists of one CREATE_CHILD_SA exchange, where key-exchange payloads are included (hence where a Diffie-Hellman protocol is run). For an agent a, we write prk(a) its private key and pbk(a) its public key. For two agents a and b, we write psk(a, b) their pre-shared key. We write g the Diffie-Hellman generator. For an agent a performing an IKEv2 subprotocol, we use the following notation for payloads that it sends: (hdr al ) l∈N>0 denotes its IKEv2 headers, ke a denotes its key-exchange payload, n a denotes its nonce payload and auth a denotes its authentication payload. We also write x a its Diffie-Hellman secret number, which is not sent.

For an agent a performing an IKEv2 subprotocol, we write rf al , if al and mid al , where l is an integer, to respectively denote the Response flag, Initiator flag and message ID fields of the IKEv2 headers that it sends. We simply note them rf a , if a and mid a when the subprotocol contains only one exchange. The Response flag is set to 1 when the message it is in is a response, and the Initiator flag is set to 1 when the message it is in is sent by the IKE SA original initiator. The message ID is an integer that starts with value 0 and is incremented at every new exchange. Its role is to prevent replay attacks.

For a given message msg, we write {msg} e k the symmetric encryption of msg using key k, {msg} s k the digital signature of msg using key k (or keyed hash if k is a pre-shared key), and {msg} c k the message msg in plain text but integrity protected by a checksum using key k. For q, r ∈ N >0 , we write q r the modular exponentiation (exponentiation in a finite field) of q by r.

Figure 1 shows the message sequence charts (MSC) of the IKEv2-Sig protocol. The IKEv2-PSK MSC can be obtained from it by replacing prk(i) and prk(r) with psk(i, r). Figure 2 shows the IKEv2-Child MSC. These MSCs contain several simplifications compared to IKEv2's RFC. For example, we do not show all IKEv2 payloads and fields. We show only those that we think have an effect on whether IKEv2 satisfies our properties or not. We explain these simplifications in Section IV.

On these figures, Initiator(i, r) means that agent i is taking the role of initiator and wants to perform the protocol with agent r. Responder(r) means that agent r is taking the role of responder and can perform the protocol with whatever agent correctly authenticates itself and is trusted by r. Finally, Responder(i, r) means that agent r is taking the role of responder and can only perform the protocol with agent i.

Furthermore, in the IKEv2-Child MSC, the term k denotes a key that is shared by the initiator and the responder before running the subprotocol. It represents the set of keys SK_ai, SK_ar, SK_ei, SK_er defined in the IKEv2 RFC, which are used to protect the IKE SA in which the subprotocol is performed. Finally, the term keymat represents the term KEY M AT defined in the IKEv2 RFC, which is a cryptographic value from which are derived all keys protecting the traffic SA negotiated through the subprotocol. It is the keying material of which IKEv2 aims to guarantee the secrecy.

III. Background

A. Model checking security protocols

Formal verification is the act of proving or disproving that a system satisfies some property using a mathematically based technique. Model checking is a formal verification technique in which we represent the system by a model, whose semantics is a transition system, and explore systematically and exhaustively all its states and transitions in order to prove that it satisfies the property. We focus on Linear Temporal Logic (LTL) [START_REF]Linear Temporal Logic[END_REF] properties.

LTL is built upon boolean logic with the addition of time indicators like always (denoted ) and eventually (denoted ♦). The linear-time property is verified on each and every execution trace of the model. The model is written in a specific modeling language, such as Applied Pi Calculus [START_REF] Abadi | The Applied Pi Calculus: Mobile Values, New Names, and Secure Communication[END_REF] or Promela [START_REF] Gerth | Concise Promela Reference[END_REF]. The model checker takes as input the system model, as well as a property over the model state variables, and either returns Yes, returns No, or does not give any response (e.g. by not terminating). When they return no and when they can, some model checkers also give a counter-example, i.e. an execution trace of the model that contradicts the property. Figure 3 sums up the steps of the model checking process. The principles of model checking are explained in great details in [START_REF] Baier | Principles of model checking[END_REF][START_REF] Edmund M Clarke | Model checking[END_REF].

We want a security protocol to be secure even in the presence of an adversary, that can intercept, drop, replay, learn from and build messages. To formalize this, Dolev and Yao first defined [START_REF] Dolev | On the security of public key protocols[END_REF] what is now called the symbolic model, or Dolev-Yao model. In this model, messages are abstracted away as entities, cryptography is supposed to be flawless and the intruder has full control over the network. The adversary's knowledge and the advancement of some agents in their execution of the protocol can be seen together as constituting a symbolic state. The actions "an agent sends a message", "an agent receives a message", "the adversary builds a message and sends it", etc., can be seen as actions modifying the state. Such a model thus lends itself well to model checking techniques.

Therefore, in our case, the system mentioned earlier is a protocol specification, played in some adversary model (capabilities given to the intruder), and the properties are security properties, like secrecy and authentication. Different techniques can be used to represent and explore the model, which model checkers abstract away: Models can be explored in a forward or backward manner. One can allow a finite or infinite number of runs (i.e. protocol executions). States can be represented explicitly or symbolically. Finally, abstractions can be used to trade completeness for efficiency. A thorough state-of-the-art of model checking security protocols is depicted in [START_REF] Basin | Model checking security protocols[END_REF].

B. Related work

In 1999, Meadows finds two authentication weaknesses in IKEv1 [START_REF] Meadows | Analysis of the Internet Key Exchange protocol using the NRL Protocol Analyzer[END_REF], using the NRL protocol analyzer. The first one is a reflection attack, and the second one is called the penultimate authentication flaw. We explain these later.

In 2003, IKEv2 is formally verified in the context of the AVISPA project [START_REF]Deliverable D6.2: Specification of the Problems in the High-Level Specification Language[END_REF]. The authors find that IKEv2 also suffers from the penultimate authentication flaw. However, they say that it cannot be exploited for further purposes. They propose a counter-measure anyway: the key confirmation.

In 2009, Kusters and Truderung use their tool DH-ProVerif to verify IKEv2 [START_REF] Küsters | Using ProVerif to Analyze Protocols with Diffie-Hellman Exponentiation[END_REF]. Their analysis seems to confirm the penultimate authentication flaw.

In 2010, Cremers performs an extensive analysis of IKEv2 [START_REF] Cremers | Key exchange in IPsec revisited: Formal analysis of IKEv1 and IKEv2[END_REF] using the Scyther tool. He confirms that IKEv2 suffers from the penultimate authentication flaw and, like in the AVISPA project, concludes that this vulnerability is harmless. In addition, [START_REF] Cremers | Key exchange in IPsec revisited: Formal analysis of IKEv1 and IKEv2[END_REF] finds that the reflection attack that was noted for IKEv1 is also possible on IKEv2.

C. The Spin model checker

Spin [START_REF] Holzmann | The model checker SPIN[END_REF] is a general-purpose explicit-state model checker. It takes Promela [START_REF] Gerth | Concise Promela Reference[END_REF] as input language and was designed to check LTL properties on asynchronous process systems. Spin translates processes into finite-state automata (hence the adjective explicit-sate), performs an interleaving product on them and searches the resulting state space for a property violation. Since a protocol is an asynchronous process system, and since all the properties we want to verify are safety properties (which are LTL properties), Spin can be used for protocol verification. However, it lacks native support for cryptographic primitives and for an adversary model. To solve this, one can use the method introduced by Ben Henda in [START_REF] Ben | Generic and efficient attacker models in spin[END_REF]. We describe this method later in Section IV.

We observe that, even with the Ben Henda method and our improvements to this method, Spin remains not the most appropriate tool for model checking security protocols: Our model only allows up to two sessions in an execution trace, and a maximum number of tree agents running these sessions. Furthermore, intruder knowledge is bounded to one message and the complexity of messages that the intruder can send over the network is limited. Other tools that are specialized in security protocol model checking do not suffer from these limitations. Such tools include ProVerif [START_REF] Blanchet | An efficient cryptographic protocol verifier based on prolog rules[END_REF], DH-ProVerif [START_REF] Küsters | Using ProVerif to Analyze Protocols with Diffie-Hellman Exponentiation[END_REF], Scyther [START_REF] Joseph | Scyther: Semantics and verification of security protocols[END_REF] and Tamarin [START_REF] Meier | The TAMARIN Prover for the Symbolic Analysis of Security Protocols[END_REF].

IV. Modeling IKEv2 in Promela

As said in Section III, verifying IKEv2 using Spin involves modeling three different concepts in Promela: the protocol itself, the adversary model and the properties. The Promela code we wrote is available at [2].

A. Modeling the protocol in Promela

Ideally, we would like to write a Promela code that represents the exact behaviour of IKEv2 as defined in its RFC. However, as pointed out in Section II, IKEv2 is far too complex to be fully modeled. For this reason, we choose to model only a subset of IKEv2 that we think satisfies the same security properties as the full-blown protocol. We say that we model a reduced form of IKEv2. For example, we do not include the traffic selector (TS) payload in our model, because we think that it has no effect on whether IKEv2 satisfies our properties or not. Indeed, the TS payloads are not used in any cryptographic operation. They neither play a role in key generation nor in authentication. This abstraction is error prone and is the reason why [START_REF] Cremers | Key exchange in IPsec revisited: Formal analysis of IKEv1 and IKEv2[END_REF] finds an attack that does not exist (the reflection attack). We discuss this in Section V.

The MSCs of Section II represent the reduced protocols that we want to model in Promela. We make the following simplifications compared to the RFC of IKEv2. As said above, we do not include all payloads and fields, because only some of them are relevant to the properties we want to verify. In addition, in the IKEv2 RFC, we have k = prf (n i |n r , g xixr ), where prf a is pseudo-random function and | denotes concatenation. In our model, we simply have k = g xixr . Finally, we abstract away key derivation: In the RFC, the SK_d, ..., SK_pr keys are derived from SKEY SEED, and the KEY M AT value is derived from SK_d. In our model, those values are all represented by a single term k.

An other problem we face in IKEv2 modeling is that Promela was not designed to model security protocols, but rather more general asynchronous process systems. For example, it does not provide a simple way to model encryption. We thus use the method of Ben Henda, explained in [START_REF] Ben | Generic and efficient attacker models in spin[END_REF]. In this method, roles are implemented by processes, and the network by a synchronous channel. We define Promela mtype constants (a Promela type of variable) describing agents, keys and a small set of values that agents can use as nonces during the protocol. As an example, in the code below, taken from the initiator process in our model, the initiator sends an IKE_AUTH request. Just before, we execute the Inirunning(i, r) macro, which sets variable inirunningab to 1 if i = A and r = B, variable arunning to 1 if i = a and variable brunning to 1 if i = b. These variables are used in our properties expression, which we present later in this Section.

I n i r u n n i n g ( i , r , k ) ; Comm!M3, k , FR0, FI1 , MID1, k , i , authkeyi , k , i , k e i , ni , nr ;

Listing 1. The initiator sending an IKE_AUTH request

Comm is the name of the channel over which the message is sent. The M 3 term indicates the type of message (here IKE_AUTH request). The F R0 and F I1 terms denote Responder and Initiator flags respectively set to 0 and 1, and the M ID1 term represents a message ID set to 1. The other terms can easily be understood since they resemble the terms we define in Section II. On reception of the message, everything after k key is interpreted as encrypted by k, and everything after authkeyi key is interpreted as a signature computed with our Promela equivalent of prk(i), or a keyed hash computed with Promela equivalent of psk(i, r).

We improve the Ben Henda method in order to fit the needs of IKEv2. Ben Henda does not provide a way to model a Diffie-Hellman exchange, so we create it. It requires adding a deduction step when adding a message to the intruder's knowledge. Indeed, when the intruder learns a payload, we now need to check whether it can deduce a key by modular exponentiation.

Even with the Ben Henda method, the nature of Promela inherently adds a layer of abstraction to the modeling process. In particular, because Spin is bounded and because of the constraints in time and memory, we allow a maximum of two sessions in an execution trace and use three agents (A, B and C). Nevertheless, such a model can capture a large class of attacks. In the code below, taken from our model's init process, we instantiate two sessions: agent A taking the role of initiator and nondeterministically intending to speak with B or C, and agent B taking the role of responder.

B. Modeling the adversary model in Promela

The property we verify strongly depends on the capabilities given to the intruder, during verification. Consequently, Basin and Cremers decided in [START_REF] Basin | Modeling and analyzing security in the presence of compromising adversaries[END_REF] to split each security property into an adversary model and an atomic property. We follow the same principle in our model.

Basin and Cremers translate several adversary models from the literature into their own formalism. We implement two of them in our model: the external Dolev-Yao model (AdvEXT) and the internal Dolev-Yao model (AdvINT). AdvEXT is a minimalistic symbolic model. As explained in Section III, cryptography is supposed to be perfect, i.e. the intruder can only decrypt a message if it possesses the decryption key. In addition, the intruder has full control over the network: it learns from all messages that are sent and can inject its own forged messages into the network.

In AdvINT, the intruder has the same capabilities as in AdvEXT, plus the LKRothers capability. The latter allows it to compromise, at the beginning of the model execution, the long-term keys of any agent that is not mentioned in the property we are verifying. For example, in the Aliveness property defined later in this Section, agents A and B are mentioned. In AdvINT, the intruder thus learns the private key of agent C. AdvINT corresponds to the model used by Lowe to find his famous attack on the Needham-Schroeder protocol [START_REF] Lowe | Breaking and fixing the Needham-Schroeder Public-Key Protocol using FDR[END_REF]. A more precise definition of LKRothers is given in [START_REF] Basin | Modeling and analyzing security in the presence of compromising adversaries[END_REF].

In the Ben Henda method, the intruder is modeled by a process (just like the initiator and responder roles), that can non-deterministically receive from the channel, forge a new message and send it, or replay a saved message. The intruder's knowledge is modeled by a boolean vector (called Knows) indexed by all the protocol constants. A memory of exactly one message is given to the intruder. This is an abstraction of the adversary model. Unfortunately, increasing this memory quickly leads to a path explosion.

We improve the Ben Henda method concerning the adversary model. To allow the intruder forging messages, Ben Henda uses a general-purpose RandM essage macro that chooses one value among all mtype constants, followed by an IsV alidM essage macro that checks the forged message's validity in regard to the intruder knowledge. He proposes more efficient definitions of RandM essage, but none of them are efficient enough for our analysis. Our Randm1m2message macro (our equivalent of RandM essage but only for IKE_SA_INIT) directly chooses for each payload a value among mtype constants whose type fits the payload. This greatly limits path explosion, without losing any realistic behaviour. We provide the code of Randm1m2message below. Note that the range of messages that the intruder can send over the network is limited. In Tamarin and ProVerif adversary models, any payload in any message sent by the intruder may contain any constants known by the attacker, encrypted any number of times, using several encryption algorithms and any key known by the attacker. In our model, we restricted for each payload the range of constants that may be sent by the intruder to a pre-selected set of constants. For example, m1 and m2 messages' fifth payload may only contain constants KEA, KEB or KEC.

C. Modeling the properties in Promela

Ideally, we would like to verify the exact properties the protocol claims to guarantee. However, security properties can be quite vague. In particular, the "mutual authentication" mentioned in [START_REF] Kaufman | Internet key exchange protocol version 2 (IKEv2)[END_REF] is an unclear notion. For this reason, researchers have split it into several definitions [START_REF] Lowe | A hierarchy of authentication specifications[END_REF][START_REF] Cas | Injective synchronisation: an extension of the authentication hierarchy[END_REF]. We verify the following atomic properties: Secrecy of keymat This property states that whenever an agent has completed the protocol, the term keymat that it computes will never be known to the intruder. Aliveness This property states that whenever an agent A has completed the protocol, apparently with an agent B, then B has previously been running the protocol. Weak agreement This property states that whenever an agent A has completed the protocol, apparently with an agent B, then B has previously been running the protocol, apparently with A. Agreement This property states that whenever an agent A has completed the protocol, apparently with an agent B, then B has previously been running the protocol, endorsing the correct role, apparently with A, and A and B agree on some terms Aliveness, weak agreement and agreement are authentication properties and were first defined by Lowe in [START_REF] Lowe | A hierarchy of authentication specifications[END_REF]. For the initiator, "apparently with B" means that the i payload it received in the IKE_AUTH response equals B. For the responder, "apparently with A" means that the r payload it received in the IKE_AUTH request equals A. We consider our authentication properties satisfied if they are satisfied whatever role A is endorsing, i.e. if they are satisfied for both the initiator and the responder. "B has previously been running the protocol" means that B has at least sent its last message. Obviously, A cannot have any stronger guarantee: if B's last event is a "receive", then the protocol cannot prove to A that this event was triggered.

Note that agreement implies weak agreement, which in turn implies aliveness. There are stronger authentication properties that we could verify. The injective agreement property, for example, adds to agreement the condition that there is only one matching session. Our model allowing only one session per role in a trace, it would not be relevant to check injective properties.

For IKEv2-Sig and IKEv2-PSK, we make parties agree upon the term keymat. For IKEv2-Child, however, we cannot guarantee to the responder that the initiator has computed keymat since the initiator has already sent its last message when it computes keymat. Therefore, for agreement in IKEv2-Child, we only guarantee to the responder that the initiator has computed kei. To the initiator we guarantee that the responder has computed keymat

We make some improvements to the Ben Henda method in the definition of our properties as well. Ben Henda verifies only one variant of authentication that can be seen as weak agreement where the peer has the correct correct role. We implement aliveness, weak agreement and agreement. In addition, our model of secrecy is more faithful to the intuitive definition of secrecy: it is not enough to check that the mtype constant we create for keymat is not known to the intruder (as [START_REF] Ben | Generic and efficient attacker models in spin[END_REF] does), one needs to check that any constant that an agent having completed the protocol considers as its keymat value, is not known to the intruder.

The code below, taken from our model, defines the properties' invariants. If one of them becomes false during execution, then the corresponding property is violated. The values of the variables appearing in the invariants are set during protocol execution. Their goal is to keep track, for each agent, where it is at in its protocol execution, as well as to whom it believes it is talking and what value it has computed for keymat. We define the terms {ini, res}{running, commit}ab as in the work of Ben Henda [START_REF] Ben | Generic and efficient attacker models in spin[END_REF]: inicommitab (resp. rescommitab) means that A (resp. B) has completed the protocol as an initiator (resp. responder), apparently with B (resp. A). In the same way, inirunningab (resp. resrunningab) means that A (resp. B) has been running the protocol (in the sense defined earlier in this Section) as an initiator (resp. responder), apparently with B (resp. A). The term arunning (resp. brunning) means that A (resp. B) has been running the protocol. The value of the term ka (resp. kb) is the mtype constant that A (resp. B) considers as its keymat key. Finally, as explained earlier in this Section, if Knows[ka] is true, then the intruder knows the term ka. Listing 4. Definition of our properties's invariants in Promela

V. Analysis results

Our Promela code and the exact Spin commands we used are available at [2]. We present our analysis results in table 4. Allowing only two sessions in a trace, very few amount of time and memory was necessary to perform the verifications. For example, only 3s and 128 MB of memory were necessary to prove aliveness on IKEv2-Sig in AdvINT. Note that we used the bitstate hashing optimisation. Our analysis yields one notable result: it refutes the reflection attack that was found by previous analyses.

In [START_REF] Cremers | Key exchange in IPsec revisited: Formal analysis of IKEv1 and IKEv2[END_REF], Cremers claims that IKEv2-Child is vulnerable to a reflection attack against the initiator. In this attack, the intruder replays the initiator's CREATE_CHILD_SA request to itself. The initiator then responds to this request, and the intruder replays this response to the initiator. This would result in a violation of aliveness, since the initiator would have thought having set up a connection with an other agent, when in fact it would have set it up with itself, the other agent not even being alive.

However, [START_REF] Cremers | Key exchange in IPsec revisited: Formal analysis of IKEv1 and IKEv2[END_REF] does not include the two Initiator and Response flags of the IKEv2 header in his model. Their role is explained in Section II. By adding these flags, our analysis shows that IKEv2-Child satisfies aliveness, weak agreement and agreement. Indeed, because of these flags, during a reflection attack, the initiator will notice that the request it receives comes from the original initiator (which is itself). He will thus refuse to answer it. Furthermore, the flags are integrity-protected: the RFC of IKEv2 says (and we found through experiment that it was the case in the strongSwan implementation) that the "Integrity Checksum Data" field of the encrypted payload is "the cryptographic checksum of the entire message starting with the Fixed IKE header through the Pad Length". The intruder thus cannot successfully change these payloads without knowing key k. Since secrecy of k is satisfied, the reflection attack is not possible.

Cremers already pointed out the obvious defense against the reflection attack: "breaking the symmetry of the messages, e. g., by including distinct constants and checking their presence" [START_REF] Cremers | Key exchange in IPsec revisited: Formal analysis of IKEv1 and IKEv2[END_REF]. We have shown that this defense is already in place in the protocol. Furthermore, the defense involves more than simply including distinct constants: these constants need to be integrity protected.

Our analysis also confirms that IKEv2-Sig does not satisfy weak agreement. This vulnerability is called the penultimate authentication flaw and was already found in previous analyses. This vulnerability is not a full violation of the intuitive definition of authentication, because there is no actual impersonation and secrecy is still satisfied. Nevertheless, an important protocol such as IKEv2 should satisfy strong forms of authentication.

VI. Counter-measures

A way to fix the protocol is to make the IDr payload mandatory in IKE_AUTH request. The message sequence chart on figure 5 shows the modified protocol. The drawback of this modification is that now the initiator sends IDr to the responder before the responder has authenticated itself. Therefore if the responder is an attacker (we then speak of active attacker), the initiator identity is revealed.

To fix IKEv2-Sig without disclosing the responder ID to an active attacker, we add a third exchange, called key confirmation. The key confirmation exchange is made of an empty INFORMATIONAL request and an empty INFORMATIONAL response. INFORMATIONAL messages are a type of message in IKEv2 that are e.g. used as keep-alive messages. The message sequence chart on figure 6 shows the modified protocol. Key confirmation has already been proposed by Basin et al. in [START_REF]Deliverable D6.2: Specification of the Problems in the High-Level Specification Language[END_REF]. However this modification has the drawback of adding a whole exchange to the protocol and therefore increasing its cost in time, memory, and computation power.

To verify that these modifications remove the penultimate authentication flaw, we apply them to our Promela models. We define four new subprotocols: modified Promela models can be found with our other models at [2].

VII. Conclusion and future work

In this paper, we have performed a formal analysis of the IKEv2 specification using the Spin model checker. To do so we extended the method of Ben Henda [START_REF] Ben | Generic and efficient attacker models in spin[END_REF] with a model of Diffie-Hellman exponentiation, an implementation of aliveness, a better implementation of secrecy and a more efficient model of intruder message creation. We also pointed out the different abstractions we made when writing the model, showing that Spin is not state-of-theart for analyzing security protocols. Our analysis showed that the reflection attack is not possible, due to IKEv2's Initiator and Response flags. Future IKEv2 models should include these flags. Futhermore our analysis confirmed the penultimate authentication flaw. As a counter-measure we discussed two possible modifications of the protocol and proved that both of them do overcome the vulnerability. Although we have analyzed the ability of the specification to meet its security goals, this does not eliminate implementation-level flaws, like buffer overflows and memory leaks. As a consequence, a future work must be performed to detect these flaws on the current and future IKEv2 implementations, e.g. using modern techniques of static analysis and fuzzing.

Fig. 2 .

 2 Fig.2. The IKEv2-Child protocol. This is the second phase of IKEv2.

Fig. 3 .

 3 Fig.3. The model checking workflow. Either proves that a system satisfies a property, or returns a counter-example, or is unable to answer.

  I n i t i a t o r (A, B) : : run I n i t i a t o r (A, C) f i ; run Responder (B) ; Listing 2. Instantiation of two runs

Listing 3 .

 3 i n l i n e Randm1m2message ( p1 , p2 , p3 , p4 , p5 , p6 , p7 , p8 , p9 , p10 , p11 , p12 , p13 ) { /* The message i s M1 or M2. We s e t the Response and I n i t i a t o r f l a g s . */ i f : : p1 = M1; p2 = FR0 ; p3 = FI1 : : p1 = M2; p2 = FR1 ; p3 = FI0 f i ; /* The message ID i s 0 . */ p4 = MID0 ; /* We s e t the Key Exchange payload . */ i f : : Knows [KEA] -> p5 = KEA : : Knows [KEB] -> p5 = KEB : : Knows [KEC] -> p5 = KEC f i ; /* We s e t the Nonce payload . */ i f : : Knows [NA] -> p6 = NA : : Knows [NB] -> p6 = NB : : Knows [NC] -> p6 = NC f i ; /* A l l o t h e r payloads a r e empty : they a r e only used f o r the M3 and M4 messages . The Randm1m2message inline function makes the intruder forge an IKE_SA_INIT message

# d e f

  i n e I n v s e c r e c y ( \ ( ! inicommitab | | ! rescommitba | | \ s t a != NULL && ! Knows [ s t a ] ) && \ ( ! rescommitab | | ! inicommitba | | \ s t b != NULL && ! Knows [ s t b ] ) ) # d e f i n e I n v a l i v e n e s s ( \ ( ! inicommitab | | brunning ) && \ ( ! rescommitab | | arunning ) && \ ( ! inicommitba | | arunning ) && \ ( ! rescommitba | | brunning ) ) # d e f i n e Invweakagree ( \ ( ! inicommitab | | r e s r u n n i n g a b | | \ i n i r u n n i n g b a ) && \ ( ! rescommitab | | i n i r u n n i n g a b | | \ r e s r u n n i n g b a ) && \ ( ! inicommitba | | r e s r u n n i n g b a | | \ i n i r u n n i n g a b ) && \ ( ! rescommitba | | i n i r u n n i n g b a | | \ r e s r u n n i n g a b ) ) # d e f i n e I n v a g r e e ( \ ( ! inicommitab | | r e s r u n n i n g a b && \ a t c a != NULL && a t c a == a t r b ) && \ ( ! rescommitab | | i n i r u n n i n g a b && \ atcb != NULL && atcb == a t r a ) && \ ( ! inicommitba | | r e s r u n n i n g b a && \ atcb != NULL && atcb == a t r a ) && \ ( ! rescommitba | | i n i r u n n i n g b a && \ a t c a != NULL && a t c a == a t r b ) )

Fig. 5 .

 5 Fig.5. The IKEv2-Sig-IDr protocol. We make IDr (r in the figure above) payload mandatory in the IKE_AUTH request and modify its processing by Responder.

Fig. 6 .

 6 Fig.6. The IKEv2-Sig-conf protocol. We add the key confirmation exchange. Connections are installed only after this exchange.

  Conf consists of one IKE_SA_INIT exchange, one IKE_AUTH exchange and one KEY_CONF exchange. It uses Signature authentication and key confirmation. We apply the counter-measures to IKEv2-PSK as well, to verify that they do not make it lose any guarantee. With these modifications, we find that these four subprotocols satisfy all our properties in all our adversary models: IKEv2's current security properties are preserved and the protocol gains stronger authentication guarantees. The Analysis of IKEv2 using Spin. We write when a subprotocol satisfies a property in a specific adversary model, and when it does not. A subprotocol satisfies a property if and only if the property is satisfied for both the initiator and the responder. Our analysis refutes the reflection attack that was found by previous analyses. hdr i1 , ke i , n i hdr r1 , ke r , n r {hdr i2 , {i, r, auth i } s k } c

	IKEv2-PSK-IDr consists of one IKE_SA_INIT exchange and one IKE_AUTH exchange. It uses PSK authen-tication and the IDr counter-measure. IKEv2-Sig-IDr consists of one IKE_SA_INIT exchange and one IKE_AUTH exchange. It uses Signature authentication and the IDr counter-measure. IKEv2-PSK-conf consists of one IKE_SA_INIT exchan-ge, one IKE_AUTH exchange and one KEY_CONF exchange. It uses PSK authentication and key confir-mation. Adversary model IKEv2-Sig IKEv2-PSK IKEv2-Child AdvEXT AdvINT AdvEXT AdvINT AdvEXT AdvINT AdvEXT AdvINT k k } c {hdr r2 , {r, auth r } s Secrecy Aliveness Weak agreement Agreement k IKEv2-Sig-Property Responder(r) msc IKEv2-Sig-IDr Fig. 4. Initiator(i, r)

The ANSSI (Agence Nationale de la Sécurité des Systèmes d'Information) is the national cybersecurity agency of France

Acknowledgment

The authors would like to thank Thomas Given-Wilson for its help with proof-reading an early version of this paper, and Youcef Ech-Chergui for its IKEv2 expertise. In addition, the authors would like to thank the ANSSI 1 for their technical review of an early version of this paper.


R Zvan-Cristian Marin

Antoine Frappé

Andreas Kaiser

Andreia Cathelin

Considerations for High-Speed Configurablebandwidth Time-interleaved Digital Delta-Sigma Modulators and Synthesis in 28 nm UTBB FDSOI

Keywords: Delta Sigma Modulator (DSM), time-interleaving, critical path analysis, digital transmitter;

This paper presents the design and simulation of a time-interleaved delta-sigma modulator as part of a digital transmitter chain. The architecture is chosen based on a critical path analysis in order to reach very high frequency operation. The modulator's configurability allows it to target signal bandwidths from 20 MHz up to 160 MHz with a SNR greater than 67 dB. Finally, the modulator is synthesized using standard cells in 28nm FDSOI CMOS from STMicroelectronics and simulated for different numbers of time-interleaved channels, reaching a sample rate of up to 6 GS/s. An optimum number of channels can be found based on a trade-off between operating frequency, supply voltage, power consumption and area.

I. INTRODUCTION

The high demand of more and more performant mobile communication systems has determined a shift from analog to digital processing in transmitter architectures (Fig. 1), in order to overcome associated challenges, such as high data rates, configurability for multi-standard, area and power consumption reduction [START_REF] Zheng | A CMOS WCDMA/WLAN Digital Polar Transmitter With AM Replica Feedback Linearization[END_REF][START_REF] Ye | Design Considerations for a Direct Digitally Modulated WLAN Transmitter With Integrated Phase Path and Dynamic Impedance Modulation[END_REF].

Furthermore, [START_REF] Frappe | An All-Digital RF Signal Generator Using High-Speed Modulators[END_REF] introduces an all-digital signal generator based on single-bit error-feedback delta-sigma modulator (DSM) directly at RF frequencies, targeting UMTS standard. The advantages of this implementation are the 1-bit output which ensures high linearity and high efficiency of the succeeding power amplifier (PA) stage and the simplification of the mixer stage which allows a reduced working frequency for the DSM, namely twice the carrier frequency f c instead of 4 times f c . In order to be able to target more performant communication standards and to reduce the in-band quantization noise, the sampling frequency of the modulator should be increased. However, this would also mean increased timing constraints which are hard to meet in a traditional DSM.

A solution is to introduce time-interleaved (TI) operation, thus relaxing the timing constraints of the system [START_REF] Madoglio | A 2.5-GHz, 6.9-mW, 45-nm-LP CMOS, Modulator Based on Standard Cell Design With Time-Interleaving[END_REF][START_REF] Bhide | Critical Path Analysis of Two-channel Interleaved Digital MASH Modulators[END_REF][START_REF] Khoini-Poorfard | Time-interleaved oversampling converters[END_REF][START_REF] Kozak | Oversampled Delta-Sigma Modulators[END_REF]. A 2 nd order multi-stage noise shaping (MASH) architecture with 8 TI channels is presented to work at an effective sampling frequency of 2.5 GHz while consuming 6.9 mW [START_REF] Madoglio | A 2.5-GHz, 6.9-mW, 45-nm-LP CMOS, Modulator Based on Standard Cell Design With Time-Interleaving[END_REF]. An extended study of the critical path for a similar architecture is performed in [START_REF] Bhide | Critical Path Analysis of Two-channel Interleaved Digital MASH Modulators[END_REF] in order to increase the sampling frequency up to 8 GHz, though the power consumption is 10 times larger than in [START_REF] Madoglio | A 2.5-GHz, 6.9-mW, 45-nm-LP CMOS, Modulator Based on Standard Cell Design With Time-Interleaving[END_REF]. Nevertheless, the MASH architecture has a multi-bit output which requires the use of an additional Digital-to-Analog Converter (DAC) and doesn't allow bandwidth configurability, since all the zeros of the noise shaping function are located at DC. Hence, error feedback DSMs have been preferred and will be studied further.

This paper details the step-by-step design of a DSM, which has been synthesized for high-speed applications up to 6 GHz sampling frequency and signal bandwidths from 20 MHz up to 160 MHz with a SNR greater than 67 dB. Therefore, it is shown that the main advantage of time-interleaving is the possibility to increase the effective sampling frequency thanks to the relaxed timing constraints.

The remainder of this paper is organized as follows. Section II presents the critical path analysis of known error feedback DSM architectures using time-interleaving. Section III introduces the proposed implementation with added configurability for improved SNR performances. Section IV presents the synthesis and simulations of the designed modulator. Finally, conclusions are presented in Section V.

II. TIME INTERLEAVING IN ERROR-FEEDBACK DSM

A. 1 st order DSM

The diagram of a 1 st order DSM incorporating a single-bit quantizer along with a discrete-time integrator in negative feedback is displayed in Fig. 2. The output in z-domain is given by

Y(z) = X(z) . z -1 + E(z) . (1-z -1 ) (1)
where X(z), Y(z) and E(z) are the z-transforms of the input, output and the quantization error, respectively. It can be seen that the input signal is filtered by the signal transfer function STF(z) = z -1 , while the quantization error is high-pass filtered by the noise transfer function NTF(z) = (1-z -1 ). Thus, the quantization noise is pushed away from the in-band to the outof-band in order to improve the SNR. TI reduced complexity [START_REF] Kozak | Oversampled Delta-Sigma Modulators[END_REF] No. integrators

LM none

No. cross-connections

L(M 2 -M) (L+1)M No. delay elements M L No. two-input adders L(M 2 -M) LM B.

TI DSM methods

The architectures in [START_REF] Madoglio | A 2.5-GHz, 6.9-mW, 45-nm-LP CMOS, Modulator Based on Standard Cell Design With Time-Interleaving[END_REF][START_REF] Bhide | Critical Path Analysis of Two-channel Interleaved Digital MASH Modulators[END_REF] use the popular block digital filtering method for time-interleaving, introduced over 20 years ago in [START_REF] Khoini-Poorfard | Time-interleaved oversampling converters[END_REF]. This method is based on poly-phase components and results in an effective sampling frequency of Mf S , where M is the number of cross-coupled DSMs operating at the sampling frequency f S . However, [START_REF] Kozak | Oversampled Delta-Sigma Modulators[END_REF] has introduced a new method with reduced complexity in terms of hardware requirements which is based on the equations in each node of the modulator.

A comparison between these 2 methods is made in [START_REF] Kozak | Oversampled Delta-Sigma Modulators[END_REF] in terms of hardware requirements for a L th order M-channel DSM (Table I), showing a highly reduced complexity especially when increasing the number of channels. Nevertheless, this method has been used only recently in a 4channel TI DSM implementation on FPGA working at a maximum sampling frequency of 400 MHz with a narrow signal bandwidth of 1.25 MHz [START_REF] Podsiadlik | Time-Interleaved Modulators for FPGAs[END_REF].

C. Critical path analysis

The architectures of a 1 st order 2-channel DSM using the poly-phase and node equations methods are displayed in Fig. 3. Assuming that the addition between 2 n-bit signals introduces a delay proportional to n and an addition between a n-bit signal and a d a -bit signal (d a <= n) introduces a reduced delay, we can estimate the delay factor of the critical path for the two methods.

Therefore, in the case of a 1 st -order 2-channel modulator, a delay factor of D pf = 4n + 2d a is obtained for the poly-phase method and D neq = 2n + 2d a for the node equations method, respectively. The value d a depends on the value of the coefficient a.

Thus, if a = 2 0 , the summation will involve only the most significant bit (MSB) and in this case d a = 1, whereas in the worst case, when a = 2 -n+1 , the summation is performed on all n bits, hence d a = n. This means that D neq (1/2) . D pf in the best case (d a = 1) and D neq = (2/3) . D pf in the worst case (d a = n). Consequently, the node equations method is more suited for high-speed applications, since it employs less hardware with relaxed timing constraints.

Next, the node equations method has been applied for different number of channels to known architectures of errorfeedback DSMs, such as Cascade-of-integrators feedback form (CIFB) [START_REF] Frappe | An All-Digital RF Signal Generator Using High-Speed Modulators[END_REF], Cascade-of-integrators feedforward form (CIFF) [START_REF] Hatami | Single-Bit Pseudoparallel Processing Low-Oversampling Delta-Sigma Modulator Suitable for SDR Wireless Transmitters[END_REF], Cascade-of-resonators feedback form (CRFB) [START_REF] Ebrahimi | Time-Interleaved Delta-Sigma Modulator For Wideband Digital GHz Transmitters Design and SDR Applications[END_REF], Cascade-of-resonators feedforward form (CRFF) [START_REF] Silva | A Novel All-Digital Multichannel Multimode RF Transmitter Using Delta-Sigma Modulation[END_REF].

The critical path of the 4 architectures for 2 nd order with 2 channels is analyzed and estimated in Table II. It can be seen that the critical path of the CIFB architecture is almost half of the next best one, CIFF and almost a third of the poly-phase CRFB implementation in [START_REF] Ebrahimi | Time-Interleaved Delta-Sigma Modulator For Wideband Digital GHz Transmitters Design and SDR Applications[END_REF]. Hence, the study has been extended in Table III to a 3 rd order CIFB architecture with up to 8 channels time-interleaving.

The impact of optimizing zeros placement (not at DC), in order to target larger bandwidth signals, is also taken into account in this table. Thus, a trade-off has to be made between the signal bandwidth and the effective sampling frequency, since the architecture with zero placement optimization has a 50% larger critical path delay than the one of the architecture with all zeros at DC.

In addition, it is shown that increasing the modulator order in the case of the CIFB architecture doesn't affect the critical path length. This has been highlighted in Table II and III for 2 nd and 3 rd order, respectively. This study also indicates that doubling the number of channels determines an increase of the delay in the critical path by a factor of 2, except from 1 to 2 channels where the factor is about 1.5. Nevertheless, optimizations in the digital synthesis flow can be more efficient on long critical paths and highly-interleaved modulator can be beneficial for achieving high speed operation.

III. CIFB ARCHITECTURE

As it has been shown in the previous section, the implementation of the coefficients influences the delay factor of the critical path which in the end determines the maximum sampling frequency of the modulator. In order to obtain simplified operations, all the coefficients have been quantized to negative powers of 2, thus avoiding dedicated multipliers. Figure 4 details the implemented coefficients of a 3 rd order CIFB DSM with optimized zero placement, designed to target up to 160 MHz signal bandwidths. The d a value is computed as the average of all coefficients, leading to d a (1/3) n.

During the design phase, it has been observed that the optimized zero placement (g 1 0) is suited only for signal bandwidths larger than 80 MHz. Otherwise, the placement of zeros at DC (g 1 = 0) gives better results in terms of peak SNR in the case of signals with smaller bandwidth. This behavior is visible in Fig. 5, where the NTFs of the modulator with all the zeros at DC (curve "1") and with zero placement optimization (curve "2") are plotted. Therefore, the magnitude of the NTF for g 1 = 0 is optimal for signal bandwidths of 20 MHz up to 80 MHz, whereas for the 160 MHz case, the magnitude of the NTF for g 1 = 2 -7 becomes optimal. Consequently, using only a 1-bit control signal (ctrl) to activate or deactivate the g 1 coefficient, as shown in Fig. 4, the architecture can be easily configured and optimized depending on the signal bandwidth, thus improving the SNR in different scenarios with extremely low effort.

Table IV contains the values of peak SNR for the targeted signal bandwidths (BW) and corresponding oversampling ratios (OSR). The case ideal corresponds to ideal coefficients, quantized corresponds to quantized coefficients with g 1 activated for 20-160 MHz and optimized corresponds to quantized coefficients with g 1 activated for 160 MHz and g 1 deactivated for 20-80 MHz, respectively. First, when comparing the quantized and ideal cases, it can be noticed that the SNR is similar for the 160 MHz case and decreases by about 44 dB for the 20 MHz case. In addition, the deactivation of the g 1 coefficient confirms it to be a valuable feature of this implementation, especially for the 20 MHz bandwidth where the SNR is improved by up to 37 dB with respect to the quantized case.

IV. TI DSM SYNTHESIS

The proposed CIFB DSM has been synthesized for different number of TI-channels using standard cells in 28nm FDSOI CMOS from STMicroelectronics. The results in terms of critical path slack have been obtained for a set of three supply voltages, {0.8, 0.9, 1} V. Thus, the maximum effective sampling frequency of the modulators with respect to the supply voltage can be estimated, reaching up to 6 GHz for 5 TI-channels operating at 1 V (Fig. 6). It is first noticed that the maximum frequency for 3-channels TI DSM is ~30% higher than its non-TI counterpart, which confirms the critical path study. Furthermore, increasing the number of TI-channels will allow operation at increased frequency, since the optimization introduced by the synthesizer can be more efficient for longer critical paths. However, increasing the number of TI channels above 10 does not bring enhanced operating frequency while the complexity increases. Additionally, if the application requires lower operating frequency, the time-interleaved modulators can operate at a reduced supply voltage in order to improve the power consumption. For instance, in the case of a 10-channel TI DSM operating at 4.5 GHz, the supply voltage can be lowered down to 0.8 V.

The power consumption with respect to the number of TIchannels for the operating frequency of 4.5 GHz and different supply voltages is presented in Table V. It can be seen, that up to 5 channels the power consumption remains around 6-7 mW, whereas a further increase of the number of channels will lead to a much higher power consumption.

The 5-channel TI DSM synthesized with standard cells in 28nm FDSOI CMOS from STMicroelectronics occupies an 80 μm x 80 μm silicon area. It has been simulated for an input sinewave at 5 MHz, reaching an effective sampling frequency of 6 GHz with a power consumption of 11.4 mW at a 1 V supply voltage (Fig. 7). These results show an improvement in the maximum sampling frequency with a factor of 2 to 3 with respect to the non-TI CIFB DSM [START_REF] Frappe | An All-Digital RF Signal Generator Using High-Speed Modulators[END_REF] and 8-channel TI MASH [START_REF] Madoglio | A 2.5-GHz, 6.9-mW, 45-nm-LP CMOS, Modulator Based on Standard Cell Design With Time-Interleaving[END_REF]. In comparison with the 2-channel TI MASH [START_REF] Bhide | Critical Path Analysis of Two-channel Interleaved Digital MASH Modulators[END_REF], the proposed architecture doesn't require the use of an additional DAC, allows bandwidth configurability and consumes ~ 6 times less. V. CONCLUSION This paper presents an extended study of a delta-sigma modulator with time-interleaving that can be used as a part of a digital transmitter chain for high speed communications systems. The modulator is easily configurable in order to target large bandwidth signals up to 160 MHz, whereas the architecture choice, CIFB, is shown to be the best candidate for high frequency operation. Furthermore, time-interleaving is proven to be effective when increasing the number of channels in order to reach higher sampling frequencies up to 6 GHz, which is 1.5 times higher than in the case of the non-TI modulator.

Fig. 1 .

 1 Fig. 1. Traditional Transmitter (left); Digital Transmitter (right)

Fig. 3 .

 3 Fig. 3. 1 st order 2-channel DSM architecture: poly-phase method (left); node equations (right)

Fig. 4 .Fig. 5 .

 45 Fig. 4. 3 rd order CIFB DSM architecture with added control

Fig. 6 .

 6 Fig. 6. TI DSM maximum effective sampling frequency vs. supply voltage

Fig. 7 .

 7 Fig. 7. Simulated output spectrum 5 channels TI DSM at 6GHz

TABLE II .

 II CRITICAL PATH IN ERROR-FEEDBACK TI DSM

	Architecture TI Method	General	Critical path Worst case (da = n)
	CIFB 2 nd order 2 channels	Node equations	3n + 2d a	5n
	CIFF 2 nd order 2 channels	Node equations	6n + 2d a	8n
	CRFB 2 nd order 2 channels	Node equations	6n + 4d a	10n
	CRFF 2 nd order 2 channels	Node equations	8n + 2d a	10n
	CRFB 2 nd order 2 channels [10]	Poly-phase	9n + 2d a	11n
	TABLE III.	CRITICAL PATH IN CIFB DSM M-TI CHANNELS
	Architecture	M-TI Channels	Critical path Optimized zeros Zeros at DC
	CIFB 3 rd order	1	2n +2d a		n + d a
	CIFB 3 rd order	2	3n + 2d a	2n + 2d a
	CIFB 3 rd order	4	6n + 4d a		4n + 4d a
	CIFB 3 rd order	8	12n + 8d a	8n + 8d a

TABLE IV .

 IV PEAK SNR 3 RD ORDER CIFB DSM

	BW [MHz]	OSR	Peak SNR [dB] (ideal)	Peak SNR [dB] (quantized)	Peak SNR [dB] (optimized)
	20	240	134.1	89.9 a	127.4 b
	40	120	112.3	78.6 a	104 b
	80	60	91.4	71.7 a	82.4 b
	160	30	69.2	67.2 a	67.2 a
					a. g1 activated

b. g1 deactivated

TABLE V .

 V SIMULATED PERFORMANCES OF TI DSM AT 4.5 GHZ

	TI-channels	Supply voltage [V]	Power consumption [mW]	Total estimated Area [μm 2 ]
	1	1.05	6.8	1 700
	3	0.9	7.4	4 500
	5	0.85	6.1	6 400
	10	0.8	9.6	12 300
	15	0.8	18.3	17 600