Gilles Barthe

Sonia Belaïd

Gaëtan Cassiers

Pierre-Alain Fouque

Benjamin Grégoire

Francois-Xavier Standaert

Automated Verification of Higher-Order Masking in Presence of Physical Defaults

Keywords: Side-Channel Attacks, Masking Countermeasure, Physical Defaults, Glitches, Automated verification, Composability, maskverif

Power and electromagnetic based side-channel attacks are serious threats against the security of cryptographic embedded devices. In order to mitigate these attacks, implementations use countermeasures, among which masking is currently the most investigated and deployed choice. Unfortunately, commonly studied forms of masking rely on underlying assumptions that are difficult to satisfy in practice. This is due to physical defaults, such as glitches or transitions, which can recombine the masked data in a way that concretely reduces an implementation's security. We develop and implement an automated approach for verifying security of masked implementations in presence of physical defaults (glitches or transitions). Our approach helps to recover the main strengths of masking: rigorous foundations, composability guarantees, automated verification under more realistic assumptions. Our work follows the approach of (Barthe et al, EUROCRYPT 2015) and thus contributes to demonstrate the benefits of language-based approaches (specifically probabilistic information flow) for masking.

Introduction

While the design of cryptographic algorithms such as block ciphers is a relatively well-understood problem [START_REF] Knudsen | The Block Cipher Companion[END_REF], the secure implementation of such algorithms is still a quite open topic. For example, the last two decades have shown that a wide range of side-channel attacks can be performed against cryptographic implementations, exploiting physical sources of leakage such as timing [START_REF] Kocher | Timing attacks on implementations of Diffie-Hellman, RSA, DSS, and other systems[END_REF], power consumption [START_REF] Kocher | Differential power analysis[END_REF] or electromagnetic radiation [START_REF] Gandolfi | Electromagnetic analysis: Concrete results[END_REF]. If no attention is paid, measuring such physical information enables retrieving cryptographic keys extremely efficiently. As a result, various types of countermeasures have been introduced to mitigate side-channel leakages, ranging from heuristic to more formal.

In general, checking that an implementation is protected against side-channel attacks is a complex and error-prone process (see [START_REF] Mangard | Power analysis attacks -revealing the secrets of smart cards[END_REF] for an overview). As a result, countermeasures relying on a more established theory have gained in relevance over the last years, in order to simplify both the design and the evaluation of protected implementations. The masking countermeasure (which consists in performing the sensitive computations on secret-shared data) has been shown to be a particularly interesting candidate in this landscape [START_REF] Chari | Towards sound approaches to counteract power-analysis attacks[END_REF]. The main reason is that practical security against physical leakages via masking can be reduced (under some noise and independence assumptions) to a much simpler (and abstract) security model, where the adversary just observes intermediate values during execution of the implementation [START_REF] Duc | Unifying leakage models: From probing attacks to noisy leakage[END_REF]. We will next refer to this simpler abstract model as ISW model, after its inventors [START_REF] Ishai | Private circuits: Securing hardware against probing attacks[END_REF].

One advantage of the ISW model is that its conceptual simplicity makes it amenable to formal verification. This has been demonstrated in a series of works, including [START_REF] Moss | Compiler assisted masking[END_REF][START_REF] Bayrak | Sleuth: Automated verification of software power analysis countermeasures[END_REF][START_REF] Eldib | Formal verification of software countermeasures against side-channel attacks[END_REF][START_REF] Barthe | Verified proofs of higher-order masking[END_REF][START_REF] Barthe | Strong non-interference and type-directed higher-order masking[END_REF][START_REF] Coron | Formal verification of side-channel countermeasures via elementary circuit transformations[END_REF][START_REF] Zhang | Scinfer: Refinement-based verification of software countermeasures against side-channel attacks[END_REF][START_REF] Bloem | Formal verification of masked hardware implementations in the presence of glitches[END_REF][START_REF] Bloem | Sharing independence & relabeling: Efficient formal verification of higher-order masking[END_REF]. The most immediate benefit of formal verification is its automation, allowing to deal with the combinatorial complexity of proving masked implementations secure. This complexity is specially significant for implementations where secrets are split into a large number of shares; we call such implementations higher-order. Perhaps more importantly, formal verification has also been instrumental for advancing the state-of-the-art in masking. First, formal verification tools have been used to reduce the randomness cost of existing schemes. Second, strong non-interference, which solves a long-standing problem of compositional reasoning for masking, has first emerged in the context of formal verification, before being adopted in the literature on masking.

However, and to the exception of [START_REF] Bloem | Formal verification of masked hardware implementations in the presence of glitches[END_REF][START_REF] Bloem | Sharing independence & relabeling: Efficient formal verification of higher-order masking[END_REF], the abstractions in these tools still do not prevent the risks due to specific physical defaults that may happen when trying to implement masking in hardware or software devices. In fact, many masking schemes that are secure in the abstract ISW model become insecure (or at least less secure) when concretely implemented. This is usually due to physical defaults which contradict the independence assumption required for secure masking. For instance, glitches are a form of physical default occurring when the information does not propagate simultaneously throughout execution. They introduce dependencies between the leakage of an instruction and of its predecessors (in the sense of dataflow analysis). These dependencies may cause hardware implementations proved secure in the ISW model to be practically vulnerable against side-channel attacks [START_REF] Mangard | Side-channel leakage of masked CMOS gates[END_REF]. Transitions are another example of physical default which more typically happen in software implementations, where the value in a register is overwritten by another value and leads the leakages to depend on both [START_REF] Coron | Conversion of security proofs from one leakage model to another: A new issue[END_REF][START_REF] Balasch | On the cost of lazy engineering for masked software implementations[END_REF].

As a consequence, it is necessary to develop models and verification methods for proving security in presence of physical defaults. Bloem et al. [START_REF] Bloem | Formal verification of masked hardware implementations in the presence of glitches[END_REF] and Faust et al. [START_REF] Faust | Composable masking schemes in the presence of physical defaults & the robust probing model[END_REF] independently extend the ISW model in order to capture physical defaults such as glitches -we will next denote this model as the ISW model with glitches. In addition, Bloem et al. propose an automated method based on an estimation of Fourier coefficients for proving that an implementation is secure in their model. They also use their verification method on a set of examples, including the S-Boxes of the AES and Keccak. Due to the computational cost of their approach, the tool primarily applies to the first-order setting, where secrets are split into two shares. Moreover, their method does not consider strong non-interference, which is key to verify complete implementations. By contrast, Faust et al. provide a hand-made analysis of some masking gadgets and prove their strong non-interference with glitches for arbitrary number of shares (at the cost of higher randomness requirements), and discuss simple conditions under which the composabiliy rules from [START_REF] Barthe | Strong non-interference and type-directed higher-order masking[END_REF] apply to implementations with glitches.

As for [START_REF] Bloem | Sharing independence & relabeling: Efficient formal verification of higher-order masking[END_REF], it is built on top of this submission (from on an earlier version of the current paper) and is still restricted to the verification of probing security only.

Contributions. We implement an efficient method for reasoning about security of higher-order masked implementations in presence of physical defaults. Our method follows a language-based approach based on probabilistic information flow for proving security of masked implementations [START_REF] Barthe | Verified proofs of higher-order masking[END_REF], and so provides further evidence of the benefits of language-based approaches.

As in [START_REF] Barthe | Verified proofs of higher-order masking[END_REF], our method follows a divide-and-conquer approach, embodied in two algorithms. Our first algorithm checks if leakages are independent of secrets for a fixed admissible set of observations. The algorithm repeatedly applies semanticpreserving simplifications to the symbolic representation of the leakages, until it does not depend on secrets or it fails. One significant improvement over [START_REF] Barthe | Verified proofs of higher-order masking[END_REF] is that our algorithm (i) is sound and complete (no attack missed and no false negative) for linear systems of equations; (ii) it minimizes false negatives for non-linear cases. Our second algorithm explores all admissible observation sets, calling the first algorithm on each of them. This algorithm is carefully designed to minimize the number of sets to explore, using the idea of large sets from [START_REF] Barthe | Verified proofs of higher-order masking[END_REF]. One significant improvement over [START_REF] Barthe | Verified proofs of higher-order masking[END_REF] is that our algorithm (i) minimizes the number of large sets (ii) uses more sophisticated data structures that improve overall efficiency.

In addition, both algorithms are specifically tailored to a rich programming model, which we introduce to maximize applicability. The critical feature of our new programming model is that all instructions are annotated with a symbolic representation of leakage. Our programming model neatly subsumes several models from the literature, including the ISW model, the recently proposed ISW model with glitches, and a version of the ISW model with transitions. Moreover, our tool applies to three main security notions: probing security, threshold noninterference, and strong non-interference (which is essential for compositional reasoning). Our coverage of models and properties is displayed in Table 1.

We implement our method on top of maskVerif and evaluate our tool on existing benchmarks. Our tool is able to verify programs efficiently for security notions that bring stronger compositional guarantees than [START_REF] Bloem | Formal verification of masked hardware implementations in the presence of glitches[END_REF] and faster than state-of-the-art tools. For instance, checking probing security for the ISW multiplication at order 4 (resp. order 5) takes 1 (resp. 45) second using [START_REF] Barthe | Verified proofs of higher-order masking[END_REF], while it takes only 0.1 (resp. 2.6) second with our tool. And checking probing security with glitches for DOM Keccak S-box at order 3 takes only 0.49s when it takes (2)

(3) (1) (2) (3) (1) (2)
(3) maskVerif [2, 3] Bloem et al. [START_REF] Bloem | Formal verification of masked hardware implementations in the presence of glitches[END_REF] this work more than 25min in [START_REF] Bloem | Formal verification of masked hardware implementations in the presence of glitches[END_REF] Note that we do not compare our results with [START_REF] Bloem | Sharing independence & relabeling: Efficient formal verification of higher-order masking[END_REF] as the authors based their method on an earlier version of this submission.

Motivating Examples

Consider the logical and, which takes as input bits a and b and produces as output a bit c such that c = a × b (we use arithmetic notation). A (first-order) masked implementation of this algorithm takes as input bits a[0], a [START_REF] Balasch | On the cost of lazy engineering for masked software implementations[END_REF], b[0] and b [START_REF] Balasch | On the cost of lazy engineering for masked software implementations[END_REF], called input shares, and outputs bits c[0] and c [START_REF] Balasch | On the cost of lazy engineering for masked software implementations[END_REF], called output shares. We consider two families of masked implementations and outline their verification. The first family is intended to provide protection against glitches. The second family is intended to provide protection against transitions.

Glitches

Figure 1 introduces a first-order masked implementation of logical and from [START_REF] Groß | An efficient side-channel protected AES implementation with arbitrary protection order[END_REF] in an idealized hardware language. The program is given as a sequence of assignments. The instruction r ← $ {0, 1} is a random assignment, i.e. r is sampled uniformly from {0, 1}. The assignments t 2 ← ff t 1 and t 6 ← ff t 5 are flip-flop assignments; they are used to store stable computations (so have no computational content), and stop the propagation of leakage. The remaining instructions are standard arithmetic assignments. The masked implementation must satisfy: correctness: the masked implementation coincides with the original algorithm, i.e. c = a × b, with a = a

[0] + a[1], b = b[0] + b[1], c = c[0] + c[1]
; security: leakage does not reveal information about secrets. We make the definition of leakage precise below and sketch a proof of security.

We first consider correctness. We symbolically execute the program to compute for each program point an expression over input shares a[0], a [START_REF] Balasch | On the cost of lazy engineering for masked software implementations[END_REF], b[0], b [START_REF] Balasch | On the cost of lazy engineering for masked software implementations[END_REF] and probabilistic variable r, see the middle column of Figure 1. We use b

[i] × a as shorthand for b[i] × a[0] + b[i] × a[1].
We now turn to security. We first define a symbolic representation of leakage, shown in the third column of Figure 1. The representation assigns to each program point a tuple of expressions over input shares a[0], a [START_REF] Balasch | On the cost of lazy engineering for masked software implementations[END_REF], b[0], b [START_REF] Balasch | On the cost of lazy engineering for masked software implementations[END_REF] and probabilistic variable r. Random assignment r ← $ {0, 1} leaks singleton {r}.

Flip-flop assignments t 2 ← ff t 1 and t 6 ← ff t 5 leak singletons {b [START_REF] Balasch | On the cost of lazy engineering for masked software implementations[END_REF] × a[0] + r} and {b[0]×a [START_REF] Balasch | On the cost of lazy engineering for masked software implementations[END_REF]+r}, i.e. the expressions they compute. Arithmetic assignments propagate transient leakages (due to glitches). For instance, assignment t 1 ← t 0 + r leaks the union of the leakage of the first two assignments. More generally, the leakage of an arithmetic assignment is defined as the leakage of its two operands (with the convention that an input share a

[i] leaks {a[i]}).
The symbolic representation of leakage can be simplified by applying rules that preserve their semantics (defined formally in later sections). One commonly used rule is optimistic sampling, which replaces an expression of the form e + r, where r only occurs once in the tuple, by r. We show the simplified leakage on the last column of Figure 1. Note that (simplified) leakage at each program point depends on at most one share of a (either a[0] or a [START_REF] Balasch | On the cost of lazy engineering for masked software implementations[END_REF]) and one share of b (either b[0] or b [START_REF] Balasch | On the cost of lazy engineering for masked software implementations[END_REF]). This suffices to conclude that the implementation is thus secure. We will make this claim precise in the next sections. For now, it suffices to get the following intuition: assume that a and b are the secrets, and (a[0], a [START_REF] Balasch | On the cost of lazy engineering for masked software implementations[END_REF]) is a secret sharing of a, i.e. a[0] and a [START_REF] Balasch | On the cost of lazy engineering for masked software implementations[END_REF] taken individually are uniformly distributed, and

a[0] + a[1] = a.
Then knowledge of a[0] or a [START_REF] Balasch | On the cost of lazy engineering for masked software implementations[END_REF] does not reveal any information about a. The situation is similar for b. Thus, knowledge of a single share of a and a single share of b does not reveal anything about them. Now consider the variant of the algorithm that omits the second flip-flop assignment in Figure 2. The leakage at the last program point is no longer independent of a, since both a[0] and a [START_REF] Balasch | On the cost of lazy engineering for masked software implementations[END_REF] appear in the tuple. Concretely, an attacker with access to the joint distribution {b[0], a[0], a [START_REF] Balasch | On the cost of lazy engineering for masked software implementations[END_REF], r} can retrieve the second and third components and add them to obtain a.

Instruction Symbolic value Symbolic leakage Simplified t0 ← b[1] × a[0] b[1] × a[0] {b[1], a[0]} {b[1], a[0]} r ← $ {0, 1} r {r} {r} t1 ← t0 + r b[1] × a[0] + r {b[1], a[0], r} {b[1], a[0], r} t2 ← ff t1 b[1] × a[0] + r {b[1] × a[0] + r} {r} t3 ← b[1] × a[1] b[1] × a[1] {b[1], a[1]} {b[1], a[1]} c[1] ← t3 + t2 b[1] × a + r {b[1], a[1], b[1] × a[0] + r} {b[1], a[1], r} t4 ← b[0] × a[1] b[0] × a[1] {b[0], a[1]} {b[0], a[1]} t5 ← t4 + r b[0] × a[1] + r {b[0], a[1], r} {b[0], a[1], r} t6 ← ff t5 b[0] × a[1] + r {b[0] × a[1] + r} {r} t7 ← b[0] × a[0] b[0] × a[0] {b[0], a[0]} {b[0], a[0]} c[0] ← t7 + t6 b[0] × a + r {b[0], a[0], b[0] × a[1] + r} {b[0], a[0], r}
We next describe how these examples are handled in our tool. The user provides a masked Verilog implementation of these algorithms and sets various parameters, including a security property (explained later). We first use an off-the-shelf tool (yosis) which generates an implementation in the ilang intermediate format (.ilang). The .ilang implementation is manually annotated to specify the public variables, the secret input variables, the secret output variables, and the random variables. Next, our tool generates from the annotated .ilang implementation an internal representation with a symbolic representation of leakage at each program point. At this point, verification starts. Our implementation exploits the fact that tuples of expressions are naturally ordered w.r.t the subset relation, e.g. the tuple {b [START_REF] Balasch | On the cost of lazy engineering for masked software implementations[END_REF], a[0], r} leaks more than the singleton {b [START_REF] Balasch | On the cost of lazy engineering for masked software implementations[END_REF], a[0]}. Thus, it suffices to consider maximal leakage sets, which appear in bold in Figure 1. Whenever verification fails, i.e. a potentially flawed tuple is detected, our tool computes the joint distribution of this tuple, so as to verify exactly whether this tuple is an attack for the weakest security notion considered. This step is exact, therefore all false negatives are removed. Our tool successfully concludes for the secure examples, and outputs and checks the flawed tuple of intermediate computations for the insecure examples.

Instruction Symbolic value Symbolic leakage Simplified t0 ← b[1] × a[0] b[1] × a[0] {b[1], a[0]} {b[1], a[0]} r ← $ {0, 1} r {r} {r} t1 ← t0 + r b[1] × a[0] + r {b[1], a[0], r} {b[1], a[0], r} t2 ← ff t1 b[1] × a[0] + r {b[1] × a[0] + r} {r} t3 ← b[1] × a[1] b[1] × a[1] {b[1], a[1]} {b[1], a[1]} c[1] ← t3 + t2 b[1] × a + r {b[1], a[1], b[1] × a[0] + r} {b[1], a[1], r} t4 ← b[0] × a[1] b[0] × a[1] {b[0], a[1]} {b[0], a[1]} t5 ← t4 + r b[0] × a[1] + r {b[0], a[1], r} {b[0], a[1], r} t6 ← b[0] × a[0] b[0] × a[0] {b[0], a[0]} {b[0], a[0]} c[0] ← t5 + t6 b[0] × a + r {b[0], a[0], a[1], r} {b[0], a[0], a[1], r}

Transitions

For simplicity of exposition, we consider a model with transitions but no glitches (and thus do not use flip-flop gates). Figure 3 introduces another first-order masked implementation of logical and. The difference with the previous implementation is that variable t 0 is reused in the last but one instruction. As a consequence, observing the last but one instruction reveals both values of t 0 , and depend on b. This is easily fixed by using a fresh variable t 5 in place of t 0 . Interestingly, replacing t 0 with t 5 places us in a model in which every instruction leaks its symbolic expression, i.e. the abstract ISW model. In both cases, verification with our tool then proceeds as described in the previous subsection.

Instruction Symbolic value Leakage t0 ← b[1] × a[0] b[1] × a[0] {b[1] × a[0]} r ← $ {0, 1} r {r} t1 ← t0 + r b[1] × a[0] + r {b[1] × a[0] + r} t2 ← b[1] × a[1] b[1] × a[1] {b[1] × a[1]} c[1] ← t1 + t2 b[1] × a + r {b[1] × a + r} t3 ← b[0] × a[1] b[0] × a[1] {b[0] × a[1]} t4 ← t3 + r b[0] × a[1] + r {b[0] × a[1] + r} t0 ← b[0] × a[0] b[0] × a[0] {b[1] × a[0], b[0] × a[0]} c[0] ← t4 + t0 b[0] × a + r {b[0] × a + r}

Programming model and security definitions

This section introduces an intermediate representation which captures different security models and notions, and presents algorithmic tools for checking that programs are secure. For the clarity of exposition, we focus on a simple setting without public variables. Adding public variables poses no technical difficulty, but clutters presentation.

Syntax and semantics of programs

Our intermediate representation abstracts away from the specifics of a particular security model, by requiring that all leakage is made explicit through program annotations. This eliminates the need to consider flip-flop assignments. We assume throughout this paper that programs operate over Booleans. Figure 4 presents the syntax of programs as sequences of annotated instructions. An annotated instruction is an instruction annotated with a unique program point p ∈ P, and a tuple of expressions which model its leakage. Instructions are probabilistic or deterministic assignments. We assume code to be written in 3-address form, i.e. the right-hand side of a deterministic assignment is of the form v 1 + v 2 or v 1 × v 2 , where v i is either a share a[i], a deterministic variable x, or a probabilistic variable r. The left-hand side of an deterministic assignment is either a share a[i] or a deterministic variable x. A probabilistic assignment is of the form r ← $ K, where r is drawn from a set R of probabilistic variables.

We now define the leakage. Let L = i K i . For every discrete set X, Distr(X) denotes the set of distributions over X. A memory is a map that assigns to every share a[i] a value in K. We let M denote the set of memories. Now consider an observation set O, i.e. a subset of P such that |O| ≤ t. We define the function:

Security notions

We recall three increasingly strong notions of security from the literature: probing security, threshold non-interference, and threshold strong non-interference. All notions capture some form of probabilistic non-interference.

Probing security is a notion of non-interference under uniform inputs. Formally, we define a set of universally uniform distributions and say that a command s is t-probing secure iff for every observation set O such that |O| ≤ t and universally uniform distributions µ and µ , we have s O (µ) = s O (µ ). Probing security considers a scenario where secret sharing is used to encode secret inputs, and the masked program is executed on encoded inputs. Since encodings are universally uniform, probing security entails that leakage does not depend on secrets. For a concrete definition of universal uniformity, we consider the case of memories over inputs a[0], a [START_REF] Balasch | On the cost of lazy engineering for masked software implementations[END_REF], b[0], and b [START_REF] Balasch | On the cost of lazy engineering for masked software implementations[END_REF]. In this setting, a distribution over memories is universally uniform iff it is the image of the function mapping pairs (a, b) to the distribution

a 0 ← $ K; b 0 ← $ K; return a[0] → a 0 , a[1] → a + a 0 , b[0] → b 0 , b 1 → b + b 0
Probing security guarantees that leakage does not depend on secrets. Indeed, it is always possible to simulate leakage by generating an encoding of arbitrary values a and b , and then executing the command on this encoding. This will result in an identical leakage.

(Threshold) non-interference can be understood as a notion of non-interference under cardinality constraints. A command s is t-non-interfering (t-NI) if and only if any set of at most t intermediate variables can be perfectly simulated from at most t shares of each input. Concretely, a command s is (threshold) non-interfering at order t iff for every observation set O such that |O| ≤ t, there exists an indexed family of sets (I a ) a∈A ⊆ {0, . . . , t} such that |I a | ≤ t and for every initial memories m and m ,

m (Ia) a∈A m =⇒ s O (m) = s O (m )
where m (Ia) a∈A m iff for every a ∈ A and i ∈ I a , we have m(a[i]) = m (a[i]). The intuition behind threshold non-interference is similar to the one behind probing security. In particular, threshold non-interference entails probing security.

For a realization of threshold non-interference, consider a masked implementation that takes as inputs a[0], a [START_REF] Balasch | On the cost of lazy engineering for masked software implementations[END_REF], b[0], and b [START_REF] Balasch | On the cost of lazy engineering for masked software implementations[END_REF]. Threshold non-interference ensures that leakage only depends on one of the sets {a[i], b[j]}. Given that the secret a is independent from a[i] and similarly for b, it follows that leakage does not give any information about the secrets.

(Threshold) strong non-interference [START_REF] Barthe | Strong non-interference and type-directed higher-order masking[END_REF] is a very technical strengthening of (threshold) non-interference. It brings very strong composability guarantees that do not hold for (threshold) non-interference. Technically, strong non-interference imposes more stringent cardinality constraints. For every observation set O, we distinguish between internal observations O in (program points where the lhs of the assignment is a variable) and output observations O out (program points where the left-hand side of the assignment is a share a[i]). We say that a command s is t-strong non-interfering (t-SNI) iff for every observation set O such that |O| ≤ t, there exists an indexed family of sets (I a ) a∈A ⊆ {0, . . . , t}, such that |I a | ≤ |O in | and for every initial memories m and m ,

m (Ia) a∈A m =⇒ s O (m) = s O (m ).
It is put forward in [START_REF] Faust | Composable masking schemes in the presence of physical defaults & the robust probing model[END_REF] that if a gadget is strongly non-interfering with glitches (which requires storing its outputs in flip flops so that they are stable and cannot propagate glitches), then the general composition rules introduced in [START_REF] Barthe | Strong non-interference and type-directed higher-order masking[END_REF] apply to hardware implementations with glitches. Being able to verify such stronger security notions is therefore helpful to analyze full ciphers and high number of shares, since it allows analyzing smaller (computationally tractable) parts of them independently, with global security guarantees thanks to composition.

Algorithmic verification

Checking probing or (S)NI security requires to verify a probabilistic non-interference property for all observation sets of size t. We define a generic verification parameterized by a test specific to each security property. The algorithm follows the same overall structure as maskVerif and relies on two functions. The first function Check is a verification algorithm for proving the probabilistic noninterference property of a fixed observation set. The function CheckAll is an exploration algorithm which (adaptively) scans all the possible sets of observations. Verification succeeds if the algorithm proves absence of leakage for all observation sets.

To verify that an observation set O (a tuple of expressions) is independent from some secret, the key idea is to apply successive transformation on O into O , preserving its distribution, until a termination condition Test is able to syntactically decide the independence. The Test function depends on the property:

-For probing security, we check if the tuple is independent from the initial mapping by checking syntactically if the secret inputs do not appear in O . -For non-interference, we check if for each input parameter a, at most t shares a[i] occur in the tuple O . -For strong non-interference, the condition is similar: for each parameter a,

at most |O in | shares a[i] should occur in O .
The transformation of O is based on optimistic sampling rule: if r ∈ e then r and e + r follow the same distribution, as well as O and O where r is replaced by e + r (O{r ← e + r}). The condition r ∈ e (i.e r is not a variable of e) ensures that the distributions of r and e are independent. The critical step is to select a substitution that will guarantee that the method terminates. Take for example O = (r, x + r). If we replace r by x + r, we obtain after simplification (x + r, r) on which we could apply the same transformation again and again. If the algorithm cannot exhibit such a context, it tries to apply the general optimistic sampling rule (removing the condition r ∈ C). The resulting expression is the simplification of O{r ← e + r}. For the simplification, we basically use the ring laws but the distributivity makes harder the detection of new simplifications. Notice that this time the size of the resulting O = O{r ← e + r} does not necessarily decrease. To ensure termination, we add a set R of random variables on which the general rule has already been used. The application of the rule is conditioned by the fact that r ∈ R. The termination of the Check algorithm is ensured since either R increases or the size of O decreases (lexicographic order).

Verification of single observation set. The Check verification algorithm is summarized in

When more than one r allow to apply the rules (i.e for the selection of the context), we define the multiplicative depth of a random variable and we rewrite in increasing order of multiplicative depth. For instance, in the expression r + (r + e) × e we assign multiplicative depth 0 to r and 1 to r . tuples in X and was not done in [START_REF] Barthe | Verified proofs of higher-order masking[END_REF]. Then, the algorithm chooses an element O in X and tries to check it. If O is successfully verified, the result B is a list of optimistic sampling transformations that can be applied to prove independence of O. Next, the algorithm selects all the elements of X that can be checked using the transformation B using Extend6 . At this point all elements in X 0 are known to satisfy the desired properties. Finally the algorithm needs to check the remaining tuples X \ X 0 .

Initially, X represents the set of all tuples of t elements that can be generated within the set of m possible observations. Its size is m t . A naive implementation would thus be exponential in t and it is crucial to have efficient data structures to represent X and to implement the functions OptSampling, Extend, and X \X 0 . We use the data structures presented in [START_REF] Barthe | Verified proofs of higher-order masking[END_REF] (worklist base space splitting).

Moreover, we use a representation of expressions as imperative graphs. This allows to detect easily if the simplest version of optimistic sampling rule can be applied (used in the first conditional of Select and OptSampling), and to compute efficiently the resulting expression.

Experiments

This section reports on experimental evaluation of our approach.

Examples. Our examples are mainly extracted from the available database provided by the authors of [START_REF] Bloem | Formal verification of masked hardware implementations in the presence of glitches[END_REF]. It gathers four different Verilog implementations of a masked multiplication. Three of them are implemented at the first masking order only, while DOM AND, designed in [START_REF] Groß | An efficient side-channel protected AES implementation with arbitrary protection order[END_REF], is available up to order t = 4, i.e. when sensitive data is split into t + 1 = 5 shares. For the latter, we also consider modified versions that achieve non-interference and strong non-interference. Larger implementations are also provided, namely three S-boxes. AES S-box as designed in [START_REF] Groß | An efficient side-channel protected AES implementation with arbitrary protection order[END_REF] and both versions of FIDES S-box as designed in [START_REF] Bilgin | Fides: Lightweight authenticated cipher with side-channel resistance for constrained hardware[END_REF] are implemented at the first order. We also consider a second-order and third-order AES S-box [START_REF] Groß | Second and third order verilog implementations of AES s-box[END_REF], and a Keccak S-box as designed in [START_REF] Gross | Higher-order side-channel protected implementations of keccak[END_REF] and implemented from the first to the third order. In addition to this existing set of examples, Keccak S-box is analyzed at two extra orders, namely t = 4 and t = 5, and two versions of a different multiplication PARA AND [START_REF] Barthe | Parallel implementations of masking schemes and the bounded moment leakage model[END_REF] are verified from the first to the fourth order.

Benchmarks. First of all, we compare our tool with [START_REF] Barthe | Verified proofs of higher-order masking[END_REF] which can only check probing security without glitches. While our tool is a variant, the resulting implementation is much more efficient. For example, checking probing security for the ISW multiplication at order 4 (resp. order 5) takes 1 (resp. 45) second using [START_REF] Barthe | Verified proofs of higher-order masking[END_REF], while it takes only 0.1 (resp. 2.6) second with our tool.

Table 2 summarizes the verification outcome of the examples7 . We use a 2.6 GHz Intel Core i7 with 16 GB of RAM running on macOS High Sierra, while Bloem et al. [START_REF] Bloem | Formal verification of masked hardware implementations in the presence of glitches[END_REF] use a Intel Xeon E5-2699v4 CPU with a clock frequency of 3.6 GHz and 512 GB of RAM running in a 64-bit Linux OS environment. The table reports on verification for the three main security properties, namely SNI, NI, and probing security, and for two scenarios: a hardware scenario (HW) with glitches, and a software scenario (SW) without physical defaults. While the tool can also take into account transitions, we omit such examples as most of our implementations come from hardware where each wire is assigned only once (and so do not have transition).

The first column of the table (# obs) indicates the number of possible observations in the targeted implementation. In the software scenario, it corresponds to the number of intermediate variables. In the hardware scenario with glitches, it corresponds to the number of optimal observations. Note the latter is much lower than in the software scenario since non-maximal observation sets are ignored. Also note that while this first column displays the number of observations n that will be further treated, verification at order t requires the analysis of n t tuples. For instance, the verification of Keccak S-box in the software scenario at order 4 requires the analysis of 450 4 ≈ 2 31 tuples. The second, third, and fourth columns report on the verification times in the 6 modes. We report 0.01s when the result is instantaneous and ∞ when the computations take more than 10 hours. When an implementation is insecure in a weaker model, then its verification time is equal for the stronger model. To report the outcome, a cross is displayed when a concrete attack is exhibited. Otherwise, the verification ends up successfully, indicating that the implementation is secure.

Comparison with Bloem et al (EUROCRYPT 2018). Bloem et al. [START_REF] Bloem | Formal verification of masked hardware implementations in the presence of glitches[END_REF] present a formal technique for proving security of implementations in the ISW model with glitches. Their method is based on Xiao-Massey lemma, which provides a necessary and sufficient condition for a boolean function to be statistically independent from a subset of its variables. Informally, the lemma states that a boolean function f is statistically independent of a set of variables X iff the socalled Fourier coefficients of every non-empty subset of X is null. However, since the computation of Fourier coefficients is computationally expensive, they use instead an approximation method whose correctness is established in their paper. By encoding their approximation in logical form, they are able to instantiate their approach using SAT-based solvers. Their tool can verify implementations of AES, Keccak and FIDES S-Boxes, but the verification cost is significant.

The last column indicates the timings from [START_REF] Bloem | Formal verification of masked hardware implementations in the presence of glitches[END_REF] which are only available for probing security with and without glitches8 . A dash is displayed when the example is not tested in [START_REF] Bloem | Formal verification of masked hardware implementations in the presence of glitches[END_REF]. The results show that our tool performs significantly better than the algorithm provided in [START_REF] Bloem | Formal verification of masked hardware implementations in the presence of glitches[END_REF]. For instance, the verification of the hardware first-order masked implementation of AES S-box is at the very least 7826 times much faster with our tool. In particular, note that some of the benchmarks provided for the tool of Bloem et al. only concern the verification of one secret (the ranking corresponds to the fastest and the lowest verification of the secrets). They are highlighted with a symbol * . As a consequence, without par-allelization, these timings would probably be significantly higher. Our algorithm can also be parallelized (it is an option of our tool), but we only use this option for Keccak at order 5 since it makes the timing measurement less accurate.

Related work

This section reviews the state-of-the-art verification tools for software (without physical defaults but transitions) and hardware masked implementations.

Software implementations. Moss et al. [START_REF] Moss | Compiler assisted masking[END_REF] were the first to consider the use of automated methods to build or verify masked implementations. Specifically, they implement a type-based masking compiler that tracks which variables are masked by random values and iteratively modifies an unprotected program until all secrets are masked. This strategy ensures security against first-order DPA.

While type-based verification is generally efficient and scalable, it is also often overly conservative, i.e. it rejects secure programs. Logic-based verification often strikes interesting trade-offs between efficiency and expressiveness. This possibility was first explored in the context of masked implementations by Bayrak et al. [START_REF] Bayrak | Sleuth: Automated verification of software power analysis countermeasures[END_REF]. Concretely, they propose a SMT-based method for analyzing the security of masked implementations against first-order DPA. Contrary to [START_REF] Moss | Compiler assisted masking[END_REF] which targets proving a stronger property of programs, their method directly targets proving statistical independence between secrets and leakage. While it is limited to first-order masking, it was extended to higher orders by Eldib, Wang and Schaumont [START_REF] Eldib | Formal verification of software countermeasures against side-channel attacks[END_REF]. Their approach is based on a logical characterization of security, akin to non-interference, and is based on model counting. While model counting incurs an exponential blow-up in the security order, and becomes infeasible even for relatively small orders, Eldib et al. circumvent the issue using incremental verification. Although such methods help, the scope of application of their methods remains limited. Recently, Zhang et al. [START_REF] Zhang | Scinfer: Refinement-based verification of software countermeasures against side-channel attacks[END_REF] show how abstraction-refinement techniques provide significant improvement in terms of precision and scalability. Their tool, called SCInfer, alternates between fast and moderately precise approaches (partly inspired from [START_REF] Barthe | Verified proofs of higher-order masking[END_REF] below) and computationally expensive but precise approaches.

Independently, Barthe et al. [START_REF] Barthe | Verified proofs of higher-order masking[END_REF] propose a different approach for proving probing security. They establish and leverage a tight connection between the security of masked implementations and probabilistic non-interference, for which they propose efficient verification methods. Specifically, they show how a relational program logic previously used for mechanizing proofs of provable security can be specialized into an efficient procedure for proving probabilistic non-interference, and develop techniques that overcome the combinatorial explosion of observation sets for high orders. The concrete outcome of their work is the maskVerif framework, which achieves practicality at reasonably high orders, and prove security in all introduced non-interference security notions. A tweaked version additionally handles verification in presence of transitions, but hardware physical defaults (e.g., glitches) are not supported. This work remains also permissive to false negatives. In the same line of work, Coron [START_REF] Coron | Formal verification of side-channel countermeasures via elementary circuit transformations[END_REF] presents an alternative tool, called checkMasks, which achieves similar functionalities as maskVerif, but exploits a more extensive set of transformations for operating on tuples of expressions. This is useful to achieve better verification times on selected examples.

A follow-up work by Barthe et al. [START_REF] Barthe | Strong non-interference and type-directed higher-order masking[END_REF] addresses the problem of compositional reasoning by introducing the notion of strong non-interference (SNI), and adapts maskVerif to check SNI. The adaptation achieves similar coverage as the original tool, i.e. it achieves practicality at reasonably high-orders. In addition, [START_REF] Barthe | Strong non-interference and type-directed higher-order masking[END_REF] proposes an information flow type system with cardinality constraints, which forms the basis of a compiler, called maskComp. This compiler transforms an unprotected implementation into an implementation that is protected at any desired order. Somewhat similar to the masking compiler of [START_REF] Moss | Compiler assisted masking[END_REF], maskComp uses typing information to control and to minimize the insertion of mask refreshing gadgets. In the same line of work, Belaïd, Goudarzi, and Rivain recently propose tightPROVE [START_REF] Belaïd | Tight private circuits: Achieving probing security with the least refreshing[END_REF] which exactly and directly verifies the software probing security of a circuit based on standard gadgets at any order.

Hardware implementations. As recalled in the previous section, Bloem et al. [START_REF] Bloem | Formal verification of masked hardware implementations in the presence of glitches[END_REF] provide a tool for proving probing security of masked implementations in the ISW model with glitches. While this tool benefits from the new treatment of physical defaults, it faces efficiency issues and handle classical higher-order examples. Recently Bloem, Iusupov, Krenn, and Mangard [START_REF] Bloem | Sharing independence & relabeling: Efficient formal verification of higher-order masking[END_REF] provide some technical optimizations based on an earlier version of this submission (using our same tool), but that are still restricted to proofs on probing security. Namely, proven implementations thus cannot be safely composed to achieve larger secure ones. The work of Faust et al. follows the alternative approach of proving the strong non-intereference of some basic gadgets with glitches, which allows composing circuits at arbitrary orders (but less efficiently) [START_REF] Faust | Composable masking schemes in the presence of physical defaults & the robust probing model[END_REF].

Conclusions

We have developed and implemented an automated method for verifying masked implementations in presence of physical defaults. Our tool is based on novel and efficient algorithms for proving probabilistic non-interference for all admissible observation sets by an attacker. Our tool conveniently supports the three main notions of security (probing security, threshold non-interference and strong noninterference) and is able to verify efficiently implementations at high orders.

In the future, it would be interesting to extend our work beyond purely qualitative security definitions, and to consider quantitative definitions that upper bound how much leakage reveals about secrets -using total variation distance [START_REF] Eldib | Quantitative masking strength: Quantifying the power side-channel resistance of software code[END_REF] or more recent metrics that directly or indirectly relate to noisy leakage security [START_REF] Duc | Unifying leakage models: From probing attacks to noisy leakage[END_REF][START_REF] Duc | Making masking security proofs concrete -or how to evaluate the security of any leaking device[END_REF]. More speculatively, it would also be interesting to extend our framework and verification methodologies to active adversaries, who can tamper with computations [START_REF] Ishai | Private circuits II: Keeping secrets in tamperable circuits[END_REF]. A first step would be to extend the correspondence between information flow and simulation-based security to the case of active adversaries. An appealing possibility would be to exploit the well-known dual view of information flow security for confidentiality and integrity. It would also be interesting to build tools based on our algorithms to synthesize masked implementations.

Fig. 1 .

 1 Fig. 1. Masked implementation of logical bit and against glitches. The second column contains the symbolic expression computed for each program point. The third and fourth columns are symbolic representations of leakage, before and after simplification. Maximal sets are written in bold. It is easy to check that c[0] + c[1] = a × b.

Fig. 2 .

 2 Fig. 2. Insecure masked implementation of logical bit and against glitches. The second column contains the symbolic expression computed for each program point. The third and fourth columns are symbolic representations of leakage, before and after simplification. Maximal sets are written in bold. It is easy to check that c[0] + c[1] = a × b.

Fig. 3 .

 3 Fig. 3. Masked implementation of logical bit and against transitions. The second column contains the symbolic expression computed for each program point. The third column contains leakage. It is easy to check that c[0] + c[1] = a × b.

sFig. 4 .

 4 Fig.[START_REF] Barthe | On the equality of probabilistic terms[END_REF]. Syntax of expressions, instructions and commands. • ranges over {+, ×}. x ranges over a set of deterministic variables V, r ranges over a set of probabilistic variables R. a[i] is called a share; a is drawn from a set A and i ∈ {0, . . . , t} for some fixed value t, generally called order.

Figure 5 :

 5 it takes as input an observation set represented as a tuple O of expressions. If Test is satisfied then Check succeeds. Otherwise, it uses the Select procedure to perform a transformation of O into O . To guarantee termination, the algorithm first attempts to check if O can be rewritten (modulo associativity and commutativity of +) as C[e + r] where C[•] is a context, and r ∈ e ∪ C, i.e. r does not occur in e and C). If it is the case, we apply the optimistic sampling rule and get C[e + r]{r ← e + r} = C[e + (e + r)] = C[r]. Notice that in that case the size of C[r] is less than the size of O (i.e the size of the resulting O decreases).

  0.01s 0.01s 0.01s 0.01s 0.01s DOM Keccak S-box[START_REF] Gross | Higher-order side-channel protected implementations of keccak[END_REF] 60 165 0

Table 1 .

 1 Verification of higher-order masked implementations in the ISW model (1), the ISW model with glitches[START_REF] Barthe | Verified proofs of higher-order masking[END_REF], and a version of the ISW model with transitions[START_REF] Barthe | Strong non-interference and type-directed higher-order masking[END_REF]

		probing	threshold	threshold strong
	Tools	security	non-interference	non-interference
	(1)

Table 2 .

 2 Overview of verification of masked hardware circuits

Missing tuples with Extend does not impact the correctness of the algorithm.

Programs/logs are available at https://sites.google.com/view/submission-cav/home

Note that the timings of[START_REF] Bloem | Formal verification of masked hardware implementations in the presence of glitches[END_REF] are obtained with a more powerful machine than ours.

We can prove that our new algorithm always terminates and is sound, i.e. it can detect all the attacks in our models. Note that considering only the first rule (first if statement of Select) makes our algorithm equivalent to the one of [START_REF] Barthe | Verified proofs of higher-order masking[END_REF]. When we apply both rules (the two if statements of Select), our algorithm is equivalent to the one of [START_REF] Barthe | On the equality of probabilistic terms[END_REF], inspired from Gaussian elimination: contrary to this last one, we do not require the expressions to be linear. An additional advantage is the absence of false negatives when all the expressions are linear (completeness), it is no more the case if we remove the second if in Select.

Both algorithms return the list B of optimistic sampling rules that have been applied: successive transformations in the exploration algorithm can be replayed.

Exploration. The exploration algorithm ensures that the verification algorithm analyzes all the possible sets of at most t intermediate variables. However, rather than verifying each set separately, the exploration algorithm recursively checks larger sets, as in [START_REF] Barthe | Verified proofs of higher-order masking[END_REF]. The idea behind the exploration algorithm is that if a tuple O is probabilistic non-interferent then all sub-tuples of O are. We present a very high level description of the algorithm to highlight the main differences with [START_REF] Barthe | Verified proofs of higher-order masking[END_REF].

The algorithm CheckAll is presented in figure 5. Let X be the set of all tuples that need to be checked. If X is empty all tuples are trivially checked and the algorithm returns true. Else, it first tries to simplify as much as possible the set X by applying the simple optimistic sampling rule, as in the first if of Select. This point is really crucial because it allows to share simplifications between all


Marc Fourmigué
email: marc.fourmigue@univ-rennes1.fr

Chalcogen bonding in crystalline diselenides and selenocyanates: from molecules of pharmaceutical interest to conducting materials

Keywords: diselenide, selenocyanate, σ-hole interaction, chalcogen bond, antioxidant, conducting materials, anion recognition

Chalcogen bonding in crystalline diselenides and selenocyanates: From molecules of pharmaceutical interest to conducting materials

M. Fourmigué, A.

Introduction

Selenium is recognized as an essential trace element involved in various physiological processes, and a deficiency of selenium in organisms can cause serious diseases. [START_REF]Selenium in Biology and Human Health[END_REF][START_REF] Braga | PATAI's Chemistry of Functional Groups, Organic Selenium and Tellurium (online version)[END_REF] As a consequence, there has been a continuing increased interest during the last few decades in developing new synthetic organoselenium compounds (Ebselen for example) [START_REF] Sarma | [END_REF] with antiinflammatory, anti-oxidant and cytoprotective activity. It has been found that in many compounds involving a divalent selenium, a non-bonding interaction with another heteroatom (O, N, ...) was taking place, in the prolongation of the C-Se bonds. These interactions were reviewed 4 in 2010 and were shown to provide many interesting advantages such as: (i) high bioactivity as well as specific redox activity, (ii) conformational rigidity toward chirality transfer, (iii) synthetic models for the glutathione peroxidase family of enzymes. They were described to derive from the interaction of nucleophiles with the low-lying antibonding orbital of the selenium moiety (σ* C-Se), providing the selenium atom an electrophilic character.

Paralleling these observations, a new theme has also emerged in the last twenty years, first in crystal engineering, the so-called σ-hole interactions. They were originally described in the heavier halogens (X) and characterized in halogenated molecules by a specific geometry of intermolecular X•••X contacts, 5,6 described as halogen bonding (XB). 7 These contacts where the halogen atom acts as an electrophile toward a Lewis base (LB) are characterized by short X•••LB distances (notably shorter than the sum of van der Waals radii) 8 and high directionality (C-X•••LB angles close to 180°). They are the consequence of polarization of the electron density around the halogen atom, with a charge depletion (the σ-hole) in the prolongation of the C-X bond. This charge-depleted area leads to an electrostatic interaction with LB. 9 Stronger interactions involve a higher degree of charge transfer, bringing then some covalency to the halogen bonding, as found for example in the reaction of I2 (XB donor) with I -(XB acceptor) to give I3 -, 10 or in the N-iodosaccharin adducts with pyridines. 11 Halogen bonding is now accepted as a general concept, 12,13 the term itself has been recognized by IUPAC 14 and the whole domain extensively reviewed. 15 XB has found today many applications, in crystal engineering, anion recognition and transport, organocatalysis, conducting and magnetic materials, luminescent molecules as well as in biochemistry. It was rapidly recognized that the concept of σ-hole was not restricted to halogen atoms but could be extended to other elements able to exhibit such an electron cloud polarization and σ-hole apparition, 16 leading to the concepts of chalcogen bonding (ChB), pnictogen bonding (PnB) and even tetrel bonding (TrB). 17 If one concentrates on the chalcogen bonding, the main difference with XB is the presence of now R e v i s e d m a n u s c r i p t 4 two σ-holes on the chalcogen atom, each of them in the prolongation of the covalent bonds to selenium atom, as illustrated in Figure 1 for the activated sulfur derivatives SCl2 and octafluorothiophane. 18,19 Among organoselenium compounds, organic diselenides R2Se2 have been extensively investigated, and especially those involved in similar intramolecular Se•••(O, N, S, …) nonbonding interactions, resulting in organoselenium species with increased hydrolytic and thermal stability, conformational rigidity and better specific properties, e.g. antioxidant activity. In order to highlight the trends observed in ChB interactions in such compounds, we have undertaken a systematic study, based on the reported X-ray crystal structures (CSD Version 5.40 November 2018), of organic diselenides and the analogous organic selenocyanates. Only organic Se (II) compounds were analyzed excluding all metallic complexes as well as Se (IV) species. Besides strong and recurrent intramolecular ChB in diselenides, intermolecular ChB was also specifically identified in cationic diselenides, whose positive charge is expected to enhance ChB toward the anionic counterions acting as ChB acceptors. Examples were found also in mixed-valence systems prepared for their conducting properties. Finally, this search has been extended to the much smaller family of structurally characterized organic selenocyanate derivatives. The strong electron-withdrawing character of the CN moiety induces a polarization of the selenium atom with the enhancement of one σ-hole (in the prolongation of the NC-Se R e v i s e d m a n u s c r i p t 5 bond) over the other, leading to even stronger intra-and intermolecular ChB interactions. In the following, the ChB interactions will be characterized by the so-called reduction ratio (RR), which is the ratio of the actual Se•••X distance over the sum of the van der Waals radii of interacting atoms, as taken from Bondi. 8

ChB interactions of diselenides with Lewis bases

Among the hundreds of organic diselenides structurally characterized, those involving only these selenium atoms as heteroatoms are often characterized by numerous Se•••Se intermolecular contacts, most often close to the normal van des Waals distance (2×1.90 Å = 3.80 Å). They will not be detailed here. Specific σ-hole interactions are more clearly identified in those molecules bearing functional groups with Lewis base character. Among them, we will mention few examples involving intermolecular interactions, followed by the extensive series that show intramolecular ChB interactions. The third series of compounds is found in cationic systems whose positive charge indeed activates the ChB interactions with neighboring counter ions.

Intermolecular ChB interactions in diselenides

The diselenocyanate molecule NCSe-SeCN provides a very good example of ChB in diselenides. The calculated electrostatic surface potential (Figure 2) clearly shows the four σholes one can anticipate, two in the prolongation of the Se-Se bond, and two in the prolongation of the C-Se bonds. 20 Its crystal structure (Figure 3, XUNHOF) 21 shows indeed that they are interacting all four with the nitrogen lone pair of neighboring molecules. As shown in Table 1, the interactions are short and highly directional. One co-crystal of NCSe-SeCN with the bromide salt PhNMe3 + , Br -has been also reported. 22 As shown in Figure 3, all four σ-holes are again interacting, with bromide anion or nitrogen atom, with very short distances (Table 1

XUNHOF

Se•••N (Å) RR Directionality (°) Se1•••N1 i 2.877 0.83 Se2-Se1•••N1 i 164.3 Se1•••N2 ii 2.937 0.85 C1-Se1•••N2 ii 172.9 Se2•••N1 iii 3.199 0.93 C2-Se2•••N1 iii 178.4 Se2•••N2 iv 3.157 0.91 Se1-Se2•••N2 iv 165.3 PEBPUH Se•••Br(N) (Å) RR Directionality (°) Se1•••N1 v 3.158 0.91 Se2-Se1•••N1 v 165.3 Se1•••Br1 vi 3.530 0.94 C1-Se1•••Br1 vi 163.2 Se2•••Br1 3.036 0.81 Se1-Se2•••Br1 174.2 Se2•••Br1 vii 3.289 0.88 C2-Se2•••Br1 vii 177.9
i -x, -0.5+y, -0.5-z. ii 0.5+x, -0.5-y, -1-z. iii 1+x, y, z. iv 0.5+x, 0.5-y, -1-z. v -0.5+x, 1-y, -z. vi -1+x, y, z. vii -0.5+x, 2-y, -z. Table 3. Structural characteristics of ChB in diaryl diselenides with 1,5 interaction (see Scheme The last series to be described here involves the cyclic diselenides based on the (1,2)diselenole core (Table 6). Compounds based on the diselenolodiselenole core (DOKXEI, CALZEX) were particularly investigated as organic semiconductors. 60,61 Indeed, the ChB interaction induced by the thienyl substituents favors a planarization of the molecules, at variance with the phenyl derivatives which exhibit a rotation of 53°. In the naphtho(1,8cd)(1,2)diselenole derivatives (Table 6), an extremely strong ChB interaction is observed (Figure 9), particularly with sp2 iminic nitrogen atoms (HATBOV, HATBUB) with reduction ratio (RR) down to 0.63. Note that the shortest ChB is indeed associated with a notable lengthening of the Se-Se bond when compared with the unsubstituted derivatives. These 6 for details.

1). X REFCODE Se•••X (Å) RR Se-Se•••X (°) Se-Se (Å) δ (°) (a) Ref. N sp2
X REFCODE Se•••X (Å) RR Se-Se•••X (°) Se-Se (Å) δ (°) (a)
REFCODE Se•••O (Å) RR Se-Se•••O (°) Se-Se (Å) Se•••N (Å) RR δ (°) (a) Ref

1,4 ChB interactions

We Another interesting series where these 1,4 ChB interactions are at work, is found in diselenides interacting with sulfur atoms as thiones or thiolates (or selenolates), as collected in Table 8.

Note that the negative charge beard by the Lewis base (in PAMKIX, PAMKET and PAMKOD)

does not lead to a stronger ChB interaction when compared with the neutral compound (SADQIA, Figure 10). We will see in the following that the opposite situation where the diselenide bears a positive charge will strongly enhance the ChB interaction.

Charge activation of ChB

Charge activation in halogen-bonded systems is a well-established process, which is observed either in cationic XB donors or using anionic Lewis bases as XB acceptors. Similarly, several cationic diselenides have been reported and structurally characterized, demonstrating indeed a notable activation of the σ-holes, both along the Se-Se bond and along the C-Se bonds in between the two Se atoms. We will first describe the purely cationic systems and then those found in radical cations obtained upon one-electron oxidation of 1,2-diselenole systems.

Charge activation in ionic systems

Most examples are found in series of bis(imidazolium), bis(formamidinium) or bis(anilinium) dications linked by a diselenide bridge, interacting with halide (Cl -, Br -, I -) or polyhalide (I3 -, IBr2 -) counterions acting as ChB acceptors. They are collected in Table 9 with a few examples shown in Figure 11. The most striking feature is in some instances the very short ChB interaction, with reduction ratio down to 0.83, illustrating the effectiveness of the charge activation, despite the competition with numerous hydrogen bond interactions which also take place around the halide anions. The shortest interactions involve the σ-holes in the prolongation of the Se-Se bond while interaction with the σ-holes in the prolongation of the C-Se bond are most often close to van der Waals contact distances (0.9 < RR < 1) but still with strong linearity.

Note also the significant lengthening of the intramolecular Se-Se bond, in the range 2.34-2.43 Å, at variance with "naked" diselenides where it amounts to 2.32-2.36 Å. These compounds R e v i s e d m a n u s c r i p t 20 were investigated in details as they derive from selenium analogs of anti-thyroid drugs, through inhibition of lactoperoxidase (LPO)-catalyzed iodination of L-tyrosine. 75,76,77 Table 9. Structural characteristics of ChB in cationic diselenides with ChB interactions with halides or polyhalides. 9 for details. Se atoms of each diselenole ring (Figure 13). The main difference lies in the actual degree of charge transfer (ρ) between the electron donor, molecule B, and the electron acceptor, BDTA-TCNQ. Based on the intramolecular bond lengths in BDTA-TCNQ and the conductivity behavior, this charge transfer is estimated to be close to 0 (ρ = 0.2 ± 0.3) in the insulating charge-transfer complex PEFGEM, while it is estimated to be close to 1 (ρ = 0.9 ± 0.2) in the conducting charge-transfer salt PEFCUC01. This striking difference is clearly seen in the characteristics of the ChB interaction. Indeed, the charged system exhibits stronger ChB (RR = 0.89) than the neutral one (RR =0.92-0.93), a convincing evidence of this charge activation process, already observed in comparable halogen-bonded charge transfer salts. 96

H 2 N H 2 N 2 Cl Se Se N NH 2 N H 2 N 2 Br TAJMEW Se Se NH 3 H 3 N 2 X X = Cl SIVPOF X = Br SIVQAS REFCODE Se•••X (Å) RR Se(C)-Se•••X (°)

Charge activation in cation radical salts

ChB interactions in selenocyanates

Organic selenocyanates R-SeCN constitutes a smaller group of around 30 reported crystal structures, but where ChB interactions proved to be present in all examples. In most diselenides described above, the preferred interaction site was, when sterically possible, the σ-hole located in the prolongation of the Se-Se bond. Organic selenocyanates are expected to exhibit a stronger dissymmetry, with a strongly electron withdrawing group nitrile group on one side, and accordingly a stronger σ-hole in the prolongation of the NC-Se bond. This dissymmetry might be very useful if one wants to use such ChB donors, for example in crystal engineering R e v i s e d m a n u s c r i p t 25 strategies, since the presence of one single (or predominant) σ-hole brings a strong element of predictability.

Intramolecular interactions in selenocyanates

A few examples of intramolecular ChB involving selenocyanates (Table 10) are found as in methyl 2-selenocyanatobenzoate (AHEQIN), 97 phenacyl selenocyanate (FAGGAV) 98 and 8-(dimethylamino)-1-naphthyl selenocyanate (GUYJUV). 99 They can be compared with analogous situations encountered above in diselenides. For example, the characteristic 1,5interaction found here in AHEQUI or HEPPIE parallels those reported in the numerous diaryldiselenides collected in Table 3. The interaction is actually stronger (RR = 0.75-0.77) here than those reported in Table 3 for comparable diselenides interacting with sp2 oxygen atoms (RRaver = 0.80), a first indication of the stronger ChB donor ability of selenocyanates. It is also indicated by the naphthalene derivative GIYJUV with RR = 0.71, while the corresponding diselenide (JOWXUO in Table 4) exhibits two Se•••N short contacts with RR values at 0.76-0.77. Besides the strongest intramolecular ChB in the prolongation of the NC-Se bond, one also often observes in these compounds a secondary, intermolecular ChB involving the second σ-hole on selenium, toward the nitrogen atom of the nitrile moiety of a neighboring molecule with RR values in the range 0.93-0.95 and a notable directionality. This is illustrated for example here in the structure adopted by the 2-nitrophenylselenocyanate (HEPPIE) in Figure 14.

Intermolecular interactions in selenocyanates

The recurrent Se•••NC motif

The vast majority of structurally characterized selenocyanates (Table 11) is characterized by recurrent intermolecular Se•••NC interactions which lead to the formation of infinite chain-like

motifs •••Se(R)-CN•••Se(R)-CN•••.

Other inter(intra)molecular interactions

In a few examples, the nitrogen atom of the selenocyanate group acting as ChB acceptor is actually displaced by other groups of stronger Lewis base character (Table 12). This is particularly observed in selenocyanates bearing a pyridinic nitrogen atom (WERYAT), a selenomethyl moiety (YUNSIK) or a nitro group (CIGGEE, HEPPUQ). As shown in Figure 16

Selenocyanate co-crystals with neutral Lewis bases

The ChB donor ability of organic selenocyanates observed above in Sections 3. As mentioned above in section 3.3, the chelating interaction with the oxygen atom of DMF found in SIZROL and PEYRIX let us infer that similar structures could be obtained upon association of such ortho bis(selenocyanatomethyl) benzenes with anionic Lewis bases such as halides (Cl -, Br -, I -). This has been realized with the 1,2-bis(selenocyanatomethyl)benzene as well as with the 1,2,4,5-tetrakis (selenocyanatomethyl)benzene. As shown in Figure 18, not only chelated µ2-X -structures are found as in SIZRIF, but also µ4-X -motifs as shown in SIZSIJ or SIZSOM. In the latter, the geometry around the halide anion was found to be intermediate between the tetrahedron and the so-called seesaw (C2v) model geometries, the latter being built from an octahedron with two vacant vertices. These compounds illustrate the concept of chargeinverted coordination chemistry of MLn species, where the metal is actually replaced by the halide anion and the ligands by ChB donors, as also discussed in XB systems. 118,119 R e v i s e d m a n u s c r i p t

Conclusions and perspectives

This comprehensive search on the crystal structures of organic diselenides with the C-Se-Se-C motif (> 300 in CSD) has shown that in the absence of specific Lewis-basic substituents and steric constraints, intermolecular interactions were often characterized by a complex set of

Figure 1 .

 1 Figure 1. Calculated B3PW91/6-31G** electrostatic potentials of SCl2 (left) and octafluorothiophane (right), computed on the 0.001 electron/bohr 3 contour of the electronic density. The extrema values VS,max of the electropositive (red) area on the sulfur atom are 25.1 and 41 kcal mol -1 in SCl2 and octafluorothiophane respectively. Adapted with permission from (i) ref. 18 (Copyright 2008 Springer) for SCl2, (ii) from ref. 19 (Copyright 2017 The Royal Society of Chemistry) for octafluorothiophane.

  ) and strong linearity. These two examples give us the essential tools to analyze the role of ChB in crystal structures of diselenides and selenocyanates.R e v i s e d m a n u s c r i p t

Figure 2 .

 2 Figure 2. Computed electrostatic potentials on the 0.001 au molecular surface of dicyanodiselenide. Reproduced from Ref 20, with authorization of ACS.

Figure 3 .

 3 Figure 3. Detail of the interaction network around NCSe-SeCN, in the molecule alone (XUNHOF) and in its co-crystal with PhNMe3 + Br -(PEBPUH). Only half of the surrounding NCSe-SeCN molecules are shown in grey.

Figure 4 . 24 Distances 2 . 2 . 27 R e v i s e d m a n u s c r i p t 9 Scheme 1 .Figure 5 .

 4242227915 Figure 4. Detail of the ChB interaction (orange dotted line) in the crystal structure of 2,5diethyl-7,8-diselenabicyclo[4.2.0]octa-1,3,5-triene-3,4-dicarbonitrile (HOGBOW).24Distances

  (a) δ (°) is the C-Se-Se-C torsion angle.(b) Two crystallographically independent molecules Another interesting feature within these series is the evolution of the Se-Se bond with the strength of the ChB interaction. The plot of this Se-Se distance vs. RR (Figure6) shows indeed a clear tendency for a Se-Se bond lengthening associated with the smallest RR values, i.e. the strongest ChB. This evolution confirms the partial charge-transfer character of such strong ChBs since this lengthening is directly correlated with the partial occupancy of the σ* Se-Se antibonding orbital.

Figure 6 .

 6 Figure 6. Evolution of the Se-Se distance with the reduction ratio associated with the ChB interaction in the series of diaryl diselenides with 1,5 interaction (See Table3 and Scheme 1)

  R e v i s e d m a n u s c r i p t 13 observed above, short Se•••X contacts and strong directionality characterize these series. On the other hand, the Se-Se bond lengths (2.32-2.38 Å) compare with that reported for the unsubstituted bis(α-naphtyl)diselenide (IGIXIH), 51 where it amounts to 2.355 Å. This linear motif in the all-chalcogen derivatives (VOLYUR, EVUMAL, ZONXUV) has been analyzed as extended hypervalent interaction by the σ(4c-6e) model within the framework of quantum theory of atoms-in-molecules (QTAIM) approach. Investigations of the electronic density characteristics at Bond Critical points (BCP) shows a shared-shell character for the Se•••SeR and Se•••SR associated with a partial degree of covalency. 52

Figure 7 .

 7 Figure 7. Two examples (with CCDC codes and RR values, see Table 4) of intramolecular ChB interactions in α-naphtyl diselenides

  (a) δ (°) is the C-Se-Se-C torsion angle. (b) Two crystallographically independent molecules R e v i s e d m a n u s c r i p t 14 Dipyridyldiselenides provide another series of 1,5 interactions involving as Lewis base the carbonyl oxygen atom of acids, esters and amides (Figure 8 & Table5) interacting with acyclic diselenides. Note that besides the 1,5 interaction, the pyridinic nitrogen atom also enters in a short N•••Se contact, which can be described as a 1,4 ChB interaction. The Se•••N distances amount to 84% of the van der Waals contact distance. These 1,4 interactions, most probably contribute to the planarization of these systems (see below Part 3.2.2.), at variance with the other derivatives described above where the absence of this extra interaction leaves the rotation around the Se-Se bond with a C-Se-Se-C torsion angle δ around ±90° as shown in Tables3 and 4.

Figure 8 .

 8 Figure 8. Two examples (with CCDC codes and RR values, see Table 5) of intramolecular ChB interactions in α-pyridyl diselenides. Se•••O interactions as bold dotted lines, Se•••N interactions as thin dotted lines.

  (a) δ (°) is the C-Se-Se-C torsion angle.(b) Two crystallographically independent molecules

  naphthalene series were investigated by Mugesh et al. as reagents for the deiodination of thyroid hormones and their decarboxylated metabolites, iodothyronamines. 62 R e v i s e d m a n u s c r i p t

R e v i s e d m a n u s c r i p tFigure 9 .

 9 Figure 9. Three examples (with CCDC codes and RR values) of intramolecular ChB interactions in diselenole systems. See Table6for details.

  have seen above that the σ-hole interactions with diselenides can develop either in the prolongation of the Se-Se bond, but also in the prolongation of the C-Se bonds, involving a diffuse positive area in between the two Se atoms, able to interact with Lewis bases through 1,4 ChB interactions. A striking consequence is then a full planarization of these acyclic diselenides (δ = ±180°), which are known otherwise to exhibit C-Se-Se-C torsion angles around ±90°. As shown in Figure 10 and Table 7, some dipyridyl diselenides provide a few examples of a fully planarized system with short Se•••N intramolecular contacts.

Figure 10 .

 10 Figure 10. Two examples of intramolecular 1,4 ChB interactions. See Tables7 and 8for details.

  (a) δ (°) is the C-Se-Se-C torsion angle.(b) Two crystallographically independent molecules

R e v i s e d m a n u s c r i p t

  (a) δ (°) is the C-Se-Se-C torsion angle.

Figure 11 .

 11 Figure 11. Representative examples of ChB interactions of dicationic diselenides. See Table9for details.

R e v i s e d m a n u s c r i p t 22 conductionScheme 2 .R e v i s e d m a n u s c r i p t 23 0

 22223 Scheme 2. Molecular structures of diselenides acting as electron donors and CCDC codes of the corresponding cation radical salts.

Figure 12 .e v i s e d m a n u s c r i p t 24

 1224 Figure 12. Detail of the chloride anion environment in the two cation radical salts (A)Cl (VAMZEO) and (B)2Cl (TSETCL10).

Figure 13 .

 13 Figure 13. Detail of the ChB in insulating (B)(BDTA-TCNQ)•PhCl (PEFGGEM) and conducting (B)(BDTA-TCNQ) (PEFGUC01).

Figure 14 .

 14 Figure 14. Intra-and intermolecular ChB in 2-nitrobenzeneselenocyanate.

  They are found in many aromatic as well as benzylic selenocyanates, and are characterized with strong and highly directional ChB interactions. We believe that such one-dimensional systems are also stabilized by cooperativity, as indeed theoretically demonstrated in model systems such as Se(CN)2.101 One representative example is shown in Figure 15 (benzylselenocyanate, CIGGOO) and structural characteristics of reported structures are collected in Table 11. It should be stressed also that in most structures, besides the shortest Se•••NC contact in the prolongation of the NC-Se bond, a secondary ChB interaction also takes place with the other selenium σ-hole, in an inversion centered motif involving a neighboring •••Se(R)-CN•••Se(R)-CN••• chain (see Figure 15 for an illustration).

Figure 15 .

 15 Figure 15. Illustration of the •••Se(R)-CN•••Se(R)-CN••• chains in benzylselenocyanate.

  , besides the strongest Se•••O or Se•••N ChB interaction in the prolongation of the NC-Se bond, we again note also the secondary Se•••NC interaction involving the second σ-hole of the selenium atom.

R e v i s e d m a n u s c r i p t 29 Table 12 .Figure 16 .

 291216 Figure 16. Detail of the selenium environment in three examples of selenocyanates interacting with nitro (HEPPUQ), selenomethyl (WEYRAT) groups or pyridinyl nitrogen atom (YUNSIK).

e v i s e d m a n u s c r i p t 30 shown in Figure 17 ,

 3017 1. and 3.2., either inter or intramolecularly, opens now the possibility for co-crystal formation, associating mono-or poly(selenocyanate) derivatives with other molecules potentially acting as ChB acceptors. For example, recrystallization of the ortho-bis(selenocyanatomethyl)benzene or the 1,2,4,5-tetrakis(selenocyanatomethyl)benzene in the presence of DMF afforded the mono-and bis DMF adducts respectively, SIZROL and PEYRIX, with short Se•••O ChB interactions. AsR they are characterized by a pincer motif where two neighboring SeCN groups actually chelate the oxygen atom of DMF. Another interesting feature of these two structures is the relative orientation of the two neighboring SeCN groups, anti in SIZROL but cis in PEYRIX which exhibits even shorter Se•••O distances and a more directional interaction.Electrostatic surface potential calculations have demonstrated the efficiency of this chelating ortho-bis(selenocyanatomethyl) motif,114 with Vs,max values reaching 50 kcal mol -1 , to be compared with the simplest benzyl selenocyanate (36.4 kcal mol -1 ) or the reference halogen bond donor F5C6-I (35.7 kcal mol -1 ) in the same conditions. We will see below in Part 3.4 that this chelating ability can be used to also efficiently interact with halide anions.

Figure 17 . 115 R e v i s e d m a n u s c r i p t

 17115 Figure 17. Detail of the ChB interaction in the chelating systems

R e v i s e d m a n u s c r i p t 32 observedFigure 17 .

 3217 Figure 17. Detail of the ChB interactions around halides with 1,4bis(selenocyanatomethyl)benzene as ChB donor.

Figure 18 .

 18 Figure 18. Details of the ChB interactions around halides with 1,2bis(selenocyanatomethyl)benzene and 1,2,4,5 tetrakis(selenocyanatomethyl)benzene as ChB donors.

  Se•••Se intermolecular contacts at distances close to the van der Waals contact distance (2× 1.90 = 3.80 Å). On the other hand, a restricted set of more hundred compounds exhibit very specific, short and highly directional interactions between the Se-Se moiety and Lewis-basic substituents (X = sp2 O, S or Se atoms, sp3, sp2 and sp N atoms, halogen atoms) or halide anions. Such interactions are well described as chalcogen bond interactions, and develop R e v i s e d m a n u s c r i p t preferentially in the prolongation of the covalent Se-Se bond, with weaker ones along the C-Se bond. The strongest intramolecular interactions lead to Se•••X distances much shorter than the van der Waals contact distance, with a reduction ratio down to 0.73 in the most favorable cases.In these situations, a partial charge transfer is deduced from the associated lengthening of the covalent Se-Se bond. Organic selenocyanates form a smaller group of around fifty reported crystal structures, with a notable strengthening of the ChB in the prolongation of the NC-Se bond. This well pronounced difference is exploited to engage poly(selenocyanato) derivatives in anion recognition processes. Albeit the current review is limited to the crystalline solid state, several studies demonstrate that the biochemical activity of diselenides is strongly influenced by the strength of such intramolecular interactions, actually maintained in solution. Similarly, intermolecular ChB, characterized by solid-state NMR, have been also confirmed by solution NMR studies. We show here that ChB interactions in diselenides and selenocyanates, often reported with the passing years every time such short contacts were (eventually) identified, are actually a very general trend, with a high degree of predictability. It should therefore allow everyone to consider it as a novel efficient tool in biochemistry, catalysis or crystal engineering strategies. s c r i p t

Table 1 .

 1 Structural characteristics of ChB in XUNHOF and PEBPUH.

Table 2 .

 2 cyclic diselenides shown in Table 2 provide evidence for a directional interaction between the sp2 O or N atoms, or the sp N atom, with the Se-Se motif. As shown in Table 2, the Se•••(O/N) distances are close to van der Waals contacts, indicating again that these intermolecular interactions, albeit present, are not very strong. Structural characteristics of intermolecular ChB

	7

  Ref.

	SPh	VOLYUR	2.950	0.80	179.2	2.356	-91.50 53
			3.012	0.84	169.0
	SeMe EVUMAL	3.030	0.80 173.3	2.386	+79.05 52
	SePh	ZONXUV	3.087	0.81	170.4	2.365	+90.98 54
			3.019	0.79	177.1
	NMe2 JOWXUO	2.651	0.77	175.3	2.384	-95.61 30
	Cl	2.629 TAWGIK (b) 2.967	0.76 0.81	177.8 172.9	2.327	+78.81	55
			2.992	0.82	174.2
			2.954	0.81	176.7	2.322	-69.45
			2.969	0.81	175.4
	Br	TAWGOQ	3.056	0.81	169.7	2.335	+90.81 55
			3.090	0.82	171.6

Table 5 .

 5 Structural characteristics of ChB in dipyridyldiselenides with 1,5 and 1,4 interactions

  .

	AHUVUV	2.703	0.79 166.7	2.388	2.874	0.83	+180	56
	MUTWOP	2.659	0.78 167.1	2.383	2.898	0.84	-180	57
	AHUWAC 2.710 NUQXUT (b) 2.671	0.79 165.8 0.78 166.4	2.379 2.388	2.874 2.875	0.83 0.83	+180 -180	56 58
		2.638	166.3	2.389	2.866	0.83	+180
	PAWDEZ	2.944	0.86 163.4	2.355	2.926	0.85	-180	59
	DECYUH	2.608	0.76 166.8	2.392	2.867	0.83	-180	26

Table 6 .

 6 Structural characteristics of ChB in (1,2)-diselenoles.

	X	REFCODE	Se•••X (Å) RR	Se-Se•••X (°) Se-Se	Ref.
						(Å)
	Diphenyl	DOKXAE	-	-	-	2.345	60
	diselenolodiselenole
	S	DOKXEI	3.036	0.82 172.1	2.328	60
	Se	CALZEX	3.076	0.81 174.2	2.329	61
	Unsubstituted	ZZZBKS01	-	-	-	2.364	63
	Naphtodiselenole
	O sp3	OSUQIE	2.818	0.82 161.4	2.348	62
	S sp3	LOJMEE	3.090	0.84 163.9	2.357	64
	N sp3	HATCEM (a) 2.560	0.74	166.0	2.426	65
			2.542	0.74	165.5	2.416
		OSUQOK	2.563	0.74 167.0	2.402	62
	N sp2	HATBOV	2.183	0.63 166.2	2.533	65
		HATBUB	2.287	0.66 166.9	2.470	65
	(a) Two crystallographically independent molecules

Table 7 .

 7 Structural characteristics of 1,4 ChB interactions in dipyridyl diselenides.

	GUPZOH	2.814	0.82 2.347	-180	66
	URUMAW	2.901	0.84 2.352	+180	67
	SUKZOP (b)	2.940, 2.925	0.85	2.344	-178.86	68
		2.888, 2.922	0.84	2.343	-178.08
	VOJHIM	2.883	0.84 2.344	-180	69
	ZEYBIQ	2.925	0.85 2.343	-180	70
	KICYAY	2.792	0.81 2.359	-180	71

REFCODE Se•••N (Å) RR Se-Se (Å) δ (°) (a)

Ref.

Table 8 .

 8 Structural characteristics of 1,4 ChB interactions with sulfur-based Lewis bases.

	SADQIA	3.070	0.83 2.358	-180 72
	VETBUS	3.082	0.83 2.343	+180 73
	PAMKIX	3.130	0.85 2.325	-180 74
	PAMKET	3.199	0.93 2.337	+180 74
	PAMKOD	3.194	0.84 2.328	-180 74

REFCODE

Se•••S(Se) (Å) RR Se-Se (Å) δ (°)

(a)

Ref.

Table 10 .

 10 Structural characteristics of selenocyanates exhibiting intramolecular ChB.

	REFCODE Se•••X (Å)	RR	C-Se•••Y (°) Ref
	AHEQIN	2.561 (X=O)	0.75	170.3	97
		3.271 (X=N)	0.95	167.3
	FAGGAV	2.723 (X=O)	0.80	152.0	98
		-	-	-
	HEPPIE	2.514 (X=O)	0.73	169.8	100
		3.259 (X=N)	0.94	175.5
	HEPPIE01	2.525 (X=O)	0.74	170.1	100
		3.222 (X=N)	0.93	178.9
	GIYJUV	2.456 (X=NMe2)	0.71	172.6	99
		-	-	-

Table 11 .

 11 ChB characteristics of •••Se(R)-CN•••Se(R)-CN••• chains formed by selenocyanates. Se•••O interaction with DMF not reported here. (b) Se•••O interaction with AcOEt not reported here

	SeCN			SeCN	SeCN
				SeCN		F 3 C	CF 3
		NCSe			F 5
	CIBFUP	SECNBZ	BATDIJ	KABTEN CF 3
						SeCN
	SeCN
			SeCN
			SeCN	NCSe	SeCN
						SeCN
	CIGGOO	NARBIR		FEDHUU
						POXYEH
	SeCN		SeCN
						SeCN
					NCSe
		NCSe
						SeCN
	PEYQIW SeCN	SeCN	SeCN PEYQUI (+ AcOEt) PEYQOC (+ DMF) PEYRAP	NCSe	PEYRIX (+ DMF) PEYRET
	REFCODE		Se•••N (Å)	RR	C-Se•••N (°)	Ref.
	CIBFUP		3.023 (a)		0.88	172.9	102
				3.065		0.89	166.1
	SECNBZ		3.06		0.89	162.32	103
	BATDIJ		2.958 (a)		0.86	175.6	104
				2.964		0.86	172.1
	KABTEN		2.883 (b)		0.84	173.1	105
				2.968		0.86	166.4
	CIGGOO		2.997		0.87	167.1	106
	NARBIR		2.985		0.86	172.9	107
				2.969		0.86	172.6
	FEDHUU		2.965 (a)		0.86	175.9	108
				3.017		0.87	175.7
				3.010		0.87	172.9
				3.015		0.87	174.1
	POXYEH		2.997 (a)		0.86	174.4	109
				3.022		0.88	171.8
	PEYQIW		3.023		0.88	168.5	110
				3.011		0.87	169.3
				3.243		0.94	134.8
	PEYRAP		2.986		0.86	171.4	110
				3.292		0.95	155.8
				3.188		0.92	177.4
				3.336		0.97	155.8
	PEYQOC (a)		2.960		0.86	175.4

Table 13 .

 13 ChB characteristics of selenocyanate adducts with neutral Lewis bases.

		CN				CN	CN
		Se		H	Me 2 N	Se	Se	H
		O			O		O
		Se		NMe 2	H	Se	Se	NMe 2
		CN				CN	CN
	SIZROL					PEYRIX
	Se			Se	N		N	FEDJEG
	CN			NC
	Se	CN	NC	Se	N		N	FEDJAC
	NCSe					N	N	XOBWET
					O	O	XOBWIX
	NCSe	NC	Se
					O 2 N	NO 2	XOBWOD
	Compound				Se•••X (Å) RR	C-Se•••X (°) Ref.
	SIZROL (X = O)		3.083	0.90	168.9	114
						3.076	0.90	168.4
	PEYRIX (X = O)		2.946	0.86	171.9	110
						2.937	0.86	175.2
	FEDJEG (X = NPy)	2.897	0.84 176.7	116
	FEDJAC (X = NPy)	2.830	0.82 177.2	116
	XOBWET (X = NPz) 3.171	0.92 172.6	115
	XOBWIX (X = O)		2.966	0.87 170.7	115
	XOBWOD (X = O) 3.231	0.94 161.9	115
	3.4. Selenocyanate adducts with halides
	Using halide anions as ChB acceptors toward such selenocyanate ChB donors was a natural
	evolution, in the continuation of the earlier report of interaction between diselenocyanate
	(NCSe)2 and PhNH3

+ ,Br -(see

Part 2.4

) and this has been first evaluated with the parasubstituted 1,4-bis(selenocyanatomethyl)benzene, co-crystallized with Bu4NCl, Bu4NBr and Bu4NI. As shown in Figure

17

structures with either µ1 or µ2 coordinated halide anions are

Table 14

 14 ChB characteristics of selenocyanate adducts with halides anions.

	Compound X -	Se•••X -	RR	C-Se•••X -	Ref.
			(Å)		(°)
	GIHCOS	µ1-I -	3.506	0.90	174.98	117
	GIHDAF	µ1-Br -	3.249	0.87	174.35	117
	GIHGIQ	µ2-Cl -	3.191	0.87	174.3	117
	SIZTAZ	µ4-Cl -	3.188	0.86	172.6	114
			3.166	0.85	174.9
			3.220	0.87	179.2
			3.473	0.94	167.7
	SIZSIG	µ4-Br -	3.343	0.87	176.5	114
			3.186	0.82	175.4
			3.346	0.87	171.9
			3.459	0.93	172.6
	SIZREB	µ4-Br -	3.363	0.87	177.5	114
			3.225	0.83	174.9
			3.358	0.87	173.6
			3.552	0.92	172.9
	SIZSOM	µ4-Cl -	3.176	0.86	173.9	114
			3.162	0.85	171.2
			3.220	0.87	174.7
			3.202	0.86	(a)
	SIZSUS	µ4-Cl -	3.154	0.85	169.9	114
			3.140	0.85	(a)
			3.092	0.83	173.0
			3.244	0.87	169.7
	GIHCUY	µ2-I -	3.451	0.89	171.9


Thouraya Benmoussa
email: benmoussa_thouraya@yahoo.fr

Oula Amrouni
email: oulabz@yahoo.fr

Abderraouf Hzami
email: abderraoufhzami@gmail.com

Laurent Dezileau
email: laurent.dezileau@gm.univ-montp2.fr

Gil Mahe
email: gilmahe@hotmail.com

Saadi

Saâdi Abdeljaouad
email: saadi_abdeljaouad@yahoo.fr

Á A Hzami

Á S Abdeljaouad

Human Impact on the Morpho-Sedimentary Evolution on the Coastal Deltaic Zones (Case of Application: Artificial Canal of Medjerda River, Tunisa)

whether they are published or not. The documents may come

Introduction

Shorelines are defined as an interface where natural, anthropogenic, socio-economic constraints are exacerbated and constantly changing. The study of coastal environments linked to different global rivers is all the more important as they can be considered as markers of the evolution of sedimentary contributions in marine environments in relation to climatic as well as human variations [START_REF] Milliman | World-wide delivery of river sediment to the oceans, John D[END_REF][START_REF] Syvitski | Global sediment fluxes to the Earth's coastal ocean[END_REF]. The evolution of the nearshore sediment distribution is related to the variability of hydrodynamic forcing and sediment availability in coastal areas [START_REF] Amrouni | Contribution of Grain-size Trend to Sediment of a Microtidal Beach. Case of the Gulf of Tunis Bay (Cape Ferina-Cape Gammarth, Tunisia)[END_REF]). The study area constitutes the coastal alluvial plain of the Medjerda River (Antiquités africaines 1995), the western bay of the Gulf of Tunis. It receives the majority of the terrigenous inputs feeding its coast [START_REF] Ouesalti | Presentation of the Tunisian site: la basse vallée de Oued Medjerda et la lagune de Ghar El Melh. Water Demand Integration[END_REF]). The mainly anthropogenic activities influencing the evolution of the northern coast sediment distribution of the Gulf of Tunis is the construction of several dams on the Medjerda-River [START_REF] Louati | Shoreline change assessment using remote sensing and GIS techniques: a case study of the Medjerda delta coast, Tunisia[END_REF].

Materials and Methods

The methodology was based on sedimentological investigation completed by spatial monitoring carried out on the mouth and the nearshore seafloor of the new Medjerda River (Since 1939). A surface sediment sampling campaign was conducted in June 2014. A total of 70 samples were taken respectively northern and southern to the new mouth of the Medjerda-River. Four short sediment cores (CEM-1: 168 cm), (CEM-2: 80 cm), (CEM-3: 42 cm) and (CEM-4: 50 cm) were collected in August and October 2016, respectively from the central front of delta, on the levee deposit, on the alluvial plain deposit and on the beach of Medjerda-Raouad (Antiquités africaines 1995). All of the submarine samples were subjected to the grain size analysis at INSTM institute. The grain size parameters (Mz, Ski,standard deviation, Ku) were calculated according to the method of [START_REF] Folk | Brazos River bar, a study in the significance of grain size parameters[END_REF]. The determination of transport types and sedimentary facies was carried out using the CM diagram method of [START_REF] Passega | Grain-size representation by CM patterns as a geological tool[END_REF]; [START_REF] Bravard | The CM pattern as a tool for the classification of alluvial suites and floodplains along the river continuum[END_REF]. A high resolution multi-proxy study was undertaken on the cores in the UM, HDR-laboratory. The grain-size analysis was carried out using a Beckman Coulter © LS 13 320. The geochemical analysis was carried out on the sedimentary material using the X-ray Fluorescence, based on 210P b and 137 Cs by Gamma spectrometry in order to establish a chronology of the geomorphological evolution of the new delta of Medjerda during the last century. The Principal Component Analysis (PCA) was carried out through the XLSAT-2016 software. The monitoring of the morphological change was established by the spatial analysis of digital data (aerial photographs, topographic maps and satellite imageries) changes between 1936-2016 with the ArcGIS 10.2 software.

Results and Discussion

Longshore Evolution of Grain Size of Submarine Samples

The summer longitudinal grain size evolution of marine sediments shows a decreasing trend from south to north. Indeed, the mean grain size (Me) from south to north of the new mouth varies respectively from 450 to 250 µm, and Mz is from the range of 1.18-1.98 U respectively. The finest tail toward the northern edge of the Medjerda nearshore is related to the wave dominated action, obviously the south-east summer direction. However, The coastal drift dominant and responsible for sediment transport on the northern coast of the Gulf of Tunis is NW-SE direction (El [START_REF] Arrim | Étude d'impact de la dynamique sédimentaire sur la stabilité du littoral du Golfe de Tunis[END_REF]. Although recent studies [START_REF] Amrouni | Contribution of Grain-size Trend to Sediment of a Microtidal Beach. Case of the Gulf of Tunis Bay (Cape Ferina-Cape Gammarth, Tunisia)[END_REF], showed an antagonistic seasonal action of the South-eastern.

To the north. As well, Gulf of Tunis bay shows a seasonal variation of 18% of the summer South-East waves (in 2016).

Grain Size and Geochemical Evolution of Sediment Cores

The high-resolution (1 cm) grain size analysis of the cores shows a spatial variability. The CEM1 core shows two distinctive sedimentary units. The layer of fine sand (D50 = 98 lm), is surmounted by clay layer which are intercalated by silty laminas. The CEM2 core reveals the same sedimentary units but is marked by wider transition layer from which the sediment became a fine-silty distribution. The core CEM3 shows that its basal part is formed of coarser sand (D50 = 228 lm). The CEM4 core shows two sedimentary units. A basal part formed of clay surmounted by a layer of medium to coarse sand (D50 = 315 lm). The mean grain size evolution on the historical beach profile (before clay deposition) shows a decreasing trend from the historical beackshore (CEM-3) to nearshore (CEM-1).

The geochemical results show varying concentrations of chemical elements such as Fe, K, Al, Rb, Nb, Cr, Ti, Ba, Ca, Sr, Zr, V, and potentially toxic metal trace elements such as Pb, Zn and As in the sedimentary cores. The Principal Component Analysis (PCA) of the chemical elements shows the presence of 3 poles: a pole of terrigenous elements (Fe, K, Al, Rb, Cr, Ti), a pole of marine elements (Ca, Zr, Sr) and a pole of the pollutant minerals (Zn, Pb and As). The evolution of the contents of chemical elements in the sedimentary column reveals a good correlation with the granulometric analysis. The marine tracers (Ca, Sr) show a significant decreasing concentration in the clay layers compared to their rate in the sandy one. The rate in terrigenous elements is higher in the fine sediments. On the other side, the chemical pollutants (Zn, Pb and As) show significant peaks especially in the clay deposits. The granulometric and geochemical analysis of the sediment cores shows that the progradation of a new delta at the new mouth of the artificial Medjerda-River was manifested by the fine detrital deposits (Silt and clay). The grain size correlation established from the backshore to the nearshore shows that the historical sandy beach (CEM3 core base) was behind the current shoreline (in the historical backshore area). The past nearshore was illustrated by the fine sand in the bottom layer of the CEM1 core. The temporal grain size distribution reveals the marine and the fluvial ones processes governing the evolution of coastal seafloor closer to the deltaic system. In fact, the transition layer is due to active seasonal East-Southeast wave current. The deltaic deposit erosion and the shoreline retreat at the Medjerda delta was manifested by the top layer of medium to coarse biogenic sand presented in the CEM-4 core which surmounted the fluvial clay deposits. The retained fluvial discharge by the dam construction decreases the coarser fraction toward silt to clay deposit.

Transport Pattern and Deposit Mechanism

The sediment samples presented on the RS segment were focused on the CM-image for the lower clay facies of CEM1, CEM2, and CEM3, which implies that a uniform suspension during the deposition of the unit was controlled by fluvial traction currents. The QR segment determined the CM patterns for the lower sandy units of CEM2 and upper unit of the CEM4 core shows the relatively larger Q99 values of sediment, which implies that the sediments are coarser. These deposits moved by saltation represent the reworking of the sand by wave action in the swash and surf zone. Finally the transitional lithologic facies is related to the interaction of fluvial deposit and the marine action closer the deltaic mouth.

Historical Evolution of the New Delta of the Medjerda

The 210 Pb/ 137 Cs-method dating associated with the spatio-temporal monitoring of the diachronic satellite imagery shows that a new delta has been developed at the new mouth of the Medjerda since 1950. The sedimentation speed was estimated at 3.32 cm an -1 between the years 1950 and 1988. The severe erosion of the river mouth ranged to 5 m/year has been affected between 1988 and 2016.

Conclusion

The result shows that the coast of new mouth of Medjerda River passed through two morpho-sedimentary states during the last century.

1. A relatively rapid progradation with a fluvial dominance marked by silt and clay deposits rich in terrigenous chemical elements from the year 1950. This sedimentary evolution of the new delta is manifested by the filling of the old mouth since 1973 flood. The winnowing of finest fraction (clay and silt) provided during the flood event on the delta front, by the active wave current lead to the preferential spatial grain size distribution toward the northern behavior coast. 2. A retrogradation statement since 1988. Indeed, the dominance of clay deposits more than coarser fraction result to the impact of the dam construction of Sidi Salem dam in 1982. Only the finer fractions can feed the coast.