Maxime Puys

Marie-Laure Potet

Pascal Lafourcade
email: pascal.lafourcade@udamail.fr

Formal Analysis of Security Properties on the OPC-UA SCADA Protocol

. Nowadays they are increasingly communicating over insecure media such as Internet. Due to their interaction with the real world, it is crucial to prove the security of their protocols. In this paper, we formally study the security of one of the most used industrial protocols: OPC-UA . Using ProVerif, a well known cryptographic protocol verification tool, we are able to check secrecy and authentication properties. We find several attacks on the protocols and provide countermeasures.

Introduction

Industrial systems also called SCADA (Supervisory Control And Data Acquisition) have been known to be targeted by cyberattacks since the famous Stuxnet case [START_REF] Langner | Stuxnet: Dissecting a cyberwarfare weapon[END_REF] in 2010. Due to the criticality of their interaction with the real world, these systems can potentially be really harmful for humans and environment. The frequency of such attacks is increasing to become one of the priorities for governmental agencies, e.g. [START_REF] Stouffer | Guide to industrial control systems (ICS) security[END_REF] from the US National Institute of Standards and Technology (NIST) or [START_REF] Anssi | Managing cybersecurity for ICS[END_REF] from the French Agence Nationale de la Sécurité des Systèmes d'Information (ANSSI).

Industrial systems differ from other systems because of the long lifetime of the devices and their difficulty to be patched in case of vulnerabilities. Such specificities encourage to carefully check standards and applications before deploying them. As it already appeared for business IT's protocols for twenty years, automated verification is crucial in order to discover flaws in the specifications of protocols before assessing implementations. However, the lack of formal verification of industrial protocols has been emphasized in 2006 by Igure et al. [START_REF] Vinay | Security issues in SCADA networks[END_REF] and in 2009 by Patel et al. [START_REF] Sandip | Improving the cyber security of SCADA communication networks[END_REF]. They particularly argued that automated protocol verification help to understand most of the vulnerabilities of a protocol before changing its standards in order to minimize the number of revisions which costs time and money.

State-of-the-art. Most of the works on the security of industrial protocols only rely on specifications written in human language rather than using formal methods. In 2004, Clarke et al. [START_REF] Gordon R Clarke | Practical modern SCADA protocols: DNP3, 60870.5 and related systems[END_REF] discussed the security of DNP3 (Distributed Network Protocol) and ICCP (Inter-Control Center Communications Protocol). In 2005, Dzung et al. [START_REF] Dzung | Security for industrial communication systems[END_REF] proposed a detailed survey on the security in SCADA systems including informal analysis on the security properties offered by various industrial protocols: OPC (Open Platform Communications), MMS (Manufacturing Message Specification), IEC 61850 , ICCP and EtherNet/IP . In 2006, in the technical documentation of OPC-UA (OPC Unified Architecture) the authors detailed the security measures of the protocol (specially in part 2, 4 and 6). In 2015, Wanying et al. [START_REF] Wanying | The study of security issues for the industrial control systems communication protocols[END_REF] summarized the security offered by MODBUS , DNP3 and OPC-UA .

On the other hand, some works propose new versions of existing protocols to make them secure against malicious adversaries. In 2007, Patel et al. [START_REF] Sandip | Analysis of SCADA security models[END_REF] studied the security of DNP3 and proposed two ways of enhancing it through digital signatures and challenge-response models. In 2009, Fovino et al. [START_REF] Fovino | Design and implementation of a secure MODBUS protocol[END_REF] proposed a secure version of MODBUS relying on well-known cryptographic primitives such as RSA and SHA2. In 2013, Hayes et al. [START_REF] Hayes | Securing MODBUS transactions using hash-based message authentication codes and stream transmission control protocol[END_REF] designed another secure MODBUS protocol using hashbased message authentication codes and built on STCP (Stream Transmission Control Protocol). To the best of our knowledge, Graham et al. [START_REF] Graham | Correctness proofs for SCADA communication protocols[END_REF] is the only work directly using formal methods to prove the security of industrial protocols or find attack against them. They proposed a formal verification of DNP3 using OFMC [START_REF] Basin | An on-the-fly model-checker for security protocol analysis[END_REF] (Open-Source Fixed-Point Model-Checker) and SPEAR II [START_REF] Saul | SPEAR II -the security protocol engineering and analysis resource[END_REF] (Security Protocol Engineering and Analysis Resource).

Contributions. We propose a formal analysis of the security of the sub-protocols involved in the OPC-UA handshake, namely OPC-UA OpenSecureChannel and OPC-UA CreateSession . These sub-protocols are crucial for the security since the first aims at authenticating a client and a server and deriving secret keys while the second allows the client to send his credentials to the server. To perform our security analysis, we use one of the most efficient tools in the domain of cryptographic protocol verification according to [START_REF] Lafourcade | Performance evaluations of cryptographic protocols. verification tools dealing with algebraic properties[END_REF], namely ProVerif developed by Blanchet et al. [START_REF] Blanchet | An efficient cryptographic protocol verifier based on Prolog rules[END_REF]. It considers the classical Dolev-Yao intruder model [START_REF] Dolev | On the security of public key protocols[END_REF] who controls the network, listens, stops, forges, replays or modifies some messages according to its knowledge. The perfect encryption hypothesis is assumed, meaning that it is not possible to decrypt a ciphertext without its encryption key or to forge a signature without knowing the secret key. ProVerif can verify security properties of a protocol such as secrecy and authentication. The first property ensures that a secret message cannot be discovered by an unauthorized agent (including the intruder). The authentication property means that one participant of the protocol is guaranteed to communicate with another one. Modeling credential in ProVerif is not common and requires to understand the assumptions made in the protocol in order to model it correctly. We follow the official OPC-UA standards in our models and checked it against a free implementation called FreeOpcUa1 . Finally, using ProVerif , we automatically find attacks against both sub-protocols and provide simple realistic countermeasures. All sources we developed are available2 .

Outline. In Section 2, we analyze the security of OPC-UA OpenSecureChannel and OPC-UA CreateSession in Section 3. Finally, we conclude in Section 4.

OPC-UA OpenSecureChannel

The OpenSecureChannel sub-protocol aims to authenticate a client and a server and allows them to exchange two secret nonces (random numbers) that will be used to derive shared keys for the later communications. Moreover, OPC-UA can be used with three security modes, namely None, Sign and SignAndEncrypt.

-SignAndEncrypt: messages are signed {h(m)} sk(X) and encrypted {m} pk(X) , where h is an hash function, sk(X) the secret key associated to X and pk(X) the public key of X. This mode claims to provide secrecy of communication using symmetric and asymmetric encryption, but also both authentication and integrity through digital signatures.

-Sign: it is the same as SignAndEncrypt but messages are only signed {h(m)} sk(x) , and not encrypted. -None: using this mode, the OpenSecureChannel sub-protocol does not serve much purpose as it does not provide any security but is used for compatibility. This protocol is described in Figure 1. In message 1, C requests information on S with GEReq meaning GetEndpointRequest. In message 2, DiscoveryEndpoint answers with the following information where GERes stands for GetEndpointResponse, SP for Security Policy and UP for UserPolicy. Both SP and UP are used for cryptographic primitive negotiations. In message 3, C sends a nonce N C to S with OSReq standing for OpenSecureChannelRequest. Finally in message 4, S answers a nonce N S to C with OSCRes for OpenSecureChannelResponse, ST for SecurityToken (a unique identifier for the channel) and TTL for TimeToLive (its life-time). The four terms GEReq, GERes, OSCReq and OSCRes indicate the purpose of each message of the protocol. At the end of this protocol, both C and S derive four keys (K CS , KSig CS , K SC and KSig SC ) by hashing the nonces with a function named P _hash, similar as in TLS [START_REF] Dierks | The transport layer security (TLS) protocol, version 1.2[END_REF]: (K CS , KSig CS ) = P _hash(N C , N S ) and (K SC , KSig SC ) = P _hash(N S , N C ).

Modeling

Normally, a GetEnpointRequest would be answered by a list of session endpoints with possibly different security modes. We suppose that the client always accepts the security mode proposed. Client's and server's certificates are modeled by their public keys. Moreover, thanks to the perfect encryption hypothesis, we can abstract the cryptographic primitives used. We consider an intruder whose public key would be accepted by a legitimate client or server. Such an intruder could for instance represent a legitimate device that has been corrupted through a virus or that is controlled by a malicious operator. We consider the following security objectives: (i) the secrecy of the keys obtained by C (denominated by K CS and KSig CS ), (ii) the secrecy of the keys obtained by S (denominated by K SC and KSig SC ), (iii) the authentication of C on N C and (iv) the authentication of S on N S .

Results

We model in ProVerif this protocol for the three security modes of OPC-UA for each objective proposed. Results provided by ProVerif are shown in Table Obviously, as the security mode None does not provide any security, all objectives can be attacked. Moreover, as nonces are exchanged in plaintext in security mode Sign, the keys are leaked. Finally, in the case of Sign and SignAndEncrypt, the intruder reroutes messages to mount attacks on authentication in order to bypass replay protections such as timestamps as the packet's destination is changed rather than being replayed later. Figure 2 shows an attack on the authentication of C using N C . This attack is possible because the standard OPC-UA protocol does not require explicitly to give the identity of the receiver of a message. Thus it allows the intruder to send to S the signed message C sent to him similarly as the man-in-the-middle attack on the Needham-Schroeder protocol [START_REF] Lowe | Breaking and fixing the Needham-Schroeder public-key protocol using FDR[END_REF].

Fixed version

We propose a fixed version of the OpenSecureChannel sub-protocol using one of the classical counter-measures for communication protocols proposed in [START_REF] Abadi | Prudent engineering practice for cryptographic protocols[END_REF]. It consists in explicitly adding the public key of the receiver to the messages and thus avoiding an intruder to reroute signed messages to usurp hosts, as presented in Section 2.2. This resolves the authentication problem but, as ProVerif confirms, attacks on secrecy are still present. In order to solve the remaining secrecy attacks, we use the key wrapping [START_REF] Focardi | An introduction to security API analysis[END_REF] mechanism present in the OPC-UA standards [START_REF] Mahnke | OPC unified architecture[END_REF][START_REF]OPC Unified Architecture. Part 2: Security model[END_REF][START_REF]OPC Unified Architecture. Part 4: Services[END_REF][START_REF]OPC Unified Architecture. Part 6: Mappings[END_REF]. All occurrences of We also use ProVerif to confirm the security of the protocol with all our countermeasures. The results are presented in Table 2

OPC-UA CreateSession

The OPC-UA CreateSession sub-protocol allows a client to send credentials (e.g. a login and a password) over an already created Secure Channel. This sub-protocol is presented in Figure 3. This protocol follows the security mode that was chosen during the OpenSecureChannel sub-protocol and uses the symmetric keys derived, thus encryption becomes symmetric and signature relies on a Message Authentication Code (MAC). Then messages sent by C are encrypted using K CS (resp. signed with KSig CS ) and messages sent by S are encrypted with K SC (resp. signed with KSig SC ). More formally, in message 1, C sends a nonce as a challenge to S with CSReq meaning Create-SessionRequest. In message 2, S answers with Sig N C = {pk(C), N C } sk(S) and CSRes for CreateSessionResponse. The message Sig N C is the response of C's challenge and requires S to sign with its private (asymmetric) key to prove that he is the same as in the OpenSecureChannel sub-protocol. For this particular use, the OPC-UA standard explicitly asks to add C's public key to the signature (which confirms the counter-measure given in Section 2.3). In message 3, C answers S's challenge with Sig N S and sends his credentials to S with ASReq for ActivateSessionRequest. Finally, in message 4, S confirms to C that the session is created with ASRes for ActivateSessionResponse and N S2 a fresh nonce as a challenge that C should use to refresh the session when it is timedout. Again, CSReq, CSRes, ASReq and ASRes indicate the purpose of each message of the protocol.

Modeling

As this protocol involves logins and passwords, we assume that C uses a different password for each server he speaks with. On the contrary, as mentioned in Section 2.1, we consider an intruder that can play a legitimate device that has been corrupted and would obtain the credentials of the client just by playing the protocol with him. Modeling of credentials is still not common in ProVerif . We use two functions: Login and Passwd. The first one takes as parameter the public key of a host in order to associate his login with him. This function is public for everybody. The function Passwd takes as parameter the private key of its owner to make it secret, but also the public key of the server to model a different password for each server. Then we provide the following equation: verifyCreds(pk(S),Login(pk(C)),Passwd(sk(C),pk(S))) = true. It allows the server to verify if a password and a login are matching and if the password is the one he knows (using his public key). According to our results for the OpenSecureChannel sub-protocol, the secrecy of the symmetric keys in security mode Sign depends on if the protocol uses key wrapping. Again, as the OPC-UA standard is not clear on how to use the mechanism in this mode, we check with and without this security. This means that if keys are compromised, then the intruder has access to it. We consider four security objectives: (i) the secrecy of the password, (ii) the authentication of C on his password, (iii) the authentication of C on Sig N S and (iv) the authentication of S on Sig N C .

Results

Results without key wrapping (thus with keys leaked in security mode Sign, cf. Table 1) are presented in Table 3. Again, all objectives are attacked in security mode None. Also the secrecy of the password cannot hold even in security mode Sign since it will be sent by the client in plaintext during a legitimate exchange. However, both challengeresponse nonces ensure authentication since the private keys are used instead of the symmetric keys. An attack on the authentication on P asswd in security mode Sign is found by the tool. In this attacks the intruder replaces the credentials of C by other valid credentials and recalculates the MAC of the message using the leaked keys. If we consider that key wrapping is used in the OpenSecureChannel sub-protocol (thus without keys leaked in security mode Sign) then according to ProVerif results the authentication on C's password becomes secure. This analysis shows that the use of key wrapping is crucial in security mode Sign. Thus it should be clearly said in the OPC-UA standard since missing this feature completely breaks the security of Sign mode. Moreover, C's credential should also be encrypted when exchanged in Sign mode to ensure their confidentiality. Finally, we check the source code of the free implementation of OPC-UA (FreeOpcUa). This implementation is secure since it forces encryption of secrets even in security mode Sign.

Conclusion

We provided a formal verification of the industry standard communication protocol OPC-UA , relying its official specifications [START_REF] Mahnke | OPC unified architecture[END_REF][START_REF]OPC Unified Architecture. Part 2: Security model[END_REF][START_REF]OPC Unified Architecture. Part 4: Services[END_REF][START_REF]OPC Unified Architecture. Part 6: Mappings[END_REF]. We used ProVerif a tool for automatic cryptographic protocol verification. Protocol modelings were tedious tasks since specifications are often elusive to allow interoperability. Particularly due to unclear statements on the use of cryptography with security mode Sign, we studied the protocol with and without counter-measures and proved the need of encryption for secrets to ensure messages security properties. We also found attacks on authentication and provided realistic counter-measures. We chose to focus on the two sub-protocols involved in the security handshake as they represent the core of the protocol's security. In the future, we aim at testing the attacks we found on official implementations which are proprietary in order to check if they filled the gap as did FreeOpcUa.

Fig. 1 .

 1 Fig. 1. OPC-UA OpenSecureChannel sub-protocol in mode SignAndEncrypt.

Fig. 2 .

 2 Fig. 2. Attack on NC : I usurps C when speaking to S.

Fig. 3 .

 3 Fig. 3. OPC-UA CreateSession sub-protocol

Table 1 .

 1 1. Results for OpenSecureChannel sub-protocol

	OPC-UA Security mode	Objectives Sec KCS Sec KSC Auth NS Auth NC
	None	UNSAFE UNSAFE UNSAFE UNSAFE
	Sign	UNSAFE UNSAFE UNSAFE UNSAFE
	SignEnc	SAFE	SAFE UNSAFE UNSAFE

Table 2 .

 2 and show that both authentication and secrecy are now secure for security modes Sign and SignAndEncrypt. As nonces are encrypted in security mode Sign, keys remain secret. Results for fixed OpenSecureChannel sub-protocol

	OPC-UA Security mode	Objectives Sec KCS Sec KSC Auth NS Auth NC
	None	UNSAFE UNSAFE UNSAFE UNSAFE
	Sign	SAFE	SAFE	SAFE	SAFE
	SignEnc	SAFE	SAFE	SAFE	SAFE

Table 3 .

 3 Results for OPC-UA CreateSession sub-protocol

	OPC-UA Security mode	Objectives Sec P asswd Auth P asswd Auth SigN S Auth SigN C
	None	UNSAFE	UNSAFE	UNSAFE	UNSAFE
	Sign	UNSAFE	UNSAFE	SAFE	SAFE
	SignEnc	SAFE	SAFE	SAFE	SAFE

https://freeopcua.github.io/

http://indusprotoverif.forge.imag.fr/PPL16.tar.gz

Acknowledgements. This work has been partially funded by the CNRS PEPS SISC ASSI 2016, the LabEx PERSYVAL-Lab (ANR-11-LABX-0025), the ARAMIS project (PIA P3342-146798) and "Digital trust" Chair from the University of Auvergne Foundation.


Jean-Guillaume Dumas
email: jean-guillaume.dumas@imag.fr

Pascal Lafourcade
email: pascal.lafourcade@udamail.fr

Jean-Baptiste Orfila
email: jean-baptiste.orfila@imag.fr

Maxime Puys
email: maxime.puys@imag.fr

Private Multi-party Matrix Multiplication and Trust Computations *

Keywords: Secure Multiparty Computation (MPC), Distributed Matrix Multiplication, Trust evaluation, Proverif

This paper deals with distributed matrix multiplication. Each player owns only one row of both matrices and wishes to learn about one distinct row of the product matrix, without revealing its input to the other players. We first improve on a weighted average protocol, in order to securely compute a dot-product with a quadratic volume of communications and linear number of rounds. We also propose a protocol with five communication rounds, using a Paillier-like underlying homomorphic public key cryptosystem, which is secure in the semi-honest model or secure with high probability in the malicious adversary model. Using ProVerif, a cryptographic protocol verification tool, we are able to check the security of the protocol and provide a countermeasure for each attack found by the tool. We also give a randomization method to avoid collusion attacks. As an application, we show that this protocol enables a distributed and secure evaluation of trust relationships in a network, for a large class of trust evaluation schemes.

Introduction

Secure multiparty computations (MPC), introduced by Yao [START_REF] Yao | Protocols for secure computations[END_REF] with the millionaires' problem, has been intensively studied during the past thirty years. The idea of MPC is to allow n players to jointly compute a function f using their private inputs without revealing them. In the end, they only know the result of the computation and no more information. Depending on possible corruptions of players, one may prove that a protocol may resist against a collusion of many players, or that it is secure even if attackers try to maliciously modify their inputs. Mostly any function can be securely computed [START_REF] Ben-Or | Completeness theorems for non-cryptographic faulttolerant distributed computation[END_REF] and many tools exist to realize MPC protocols. They comprise for instance the use of a Trusted Third Party [START_REF] Du | A practical approach to solve secure multi-party computation problems[END_REF], the use of Shamir's secret sharing scheme [START_REF] Shamir | How to share a secret[END_REF], or more recently the use of homomorphic encryption [START_REF] Goethals | On private scalar product computation for privacy-preserving data mining[END_REF]. It is also possible to mix these techniques [START_REF] Damgård | Multiparty computation from somewhat homomorphic encryption[END_REF].

Our goal is to apply MPC to the a distributed eval-uation of trust, as defined in [START_REF] Jøsang | Probabilistic logic under uncertainty[END_REF][START_REF] Dumas | Matrix powers algorithm for trust evaluation in PKI architectures[END_REF]. There, confidence is a combination of degrees of trust, distrust and uncertainty between players. Aggregation of trusts between players on a network is done by a matrix product defined on two monoids (one for the addition of trust, the other one for multiplication, or transitivity): each player knows one row of the matrix, its partial trust on its neighbors, and the network as a whole has to compute a distributed matrix squaring. Considering that the trust of each player for his colleagues is private, at the end of the computation, nothing but one row of the global trust has to be learned by each player (i.e., nothing about private inputs should be revealed to others). Thus, an MPC protocol to resolve this problem should combine privacy (nothing is learned but the output), safety (computation of the function does not reveal anything about inputs) and efficiency [START_REF] Lindell | Secure computation for privacy preserving data mining[END_REF]. First, we need to define a MPC protocol which allows us to efficiently compute a distributed matrix product with this division of data between players.

The problem is reduced to the computation of a dot product between vectors U and V such that one player knows U and V is divided between all players. Related Work. Dot product in the MPC model has been widely studied [START_REF] Du | Privacy-preserving cooperative statistical analysis[END_REF][START_REF] Amirbekyan | A new efficient privacy-preserving scalar product protocol[END_REF][START_REF] Wang | Towards empirical aspects of secure scalar product[END_REF].

However, in these papers, assumptions made on data partitions are different: there, each player owns a complete vector, and the dot product is computed between two players where; in our setting, trust evaluation should be done among peers, like certification authorities. For instance, using a trusted third party or permuting the coefficients is unrealistic. Now, computing a dot product with n players is actually close to the MPWP protocol of [START_REF] Dolev | Computing multi-party trust privately: in O(n) time units sending one (possibly large) message at a time[END_REF], computing a mean in a distributed manner: computing dot products is actually similar to computing a weighted average where the weights are in the known row, and the values to be averaged are privately distributed. In MPWP the total volume of communication for a dot product is O n 3 with O (n) communication rounds. Other generic MPC protocols exist, also evaluating circuits, they however also require

O n 3 computations and/or communications per dotproduct [START_REF] Bendlin | Semi-homomorphic encryption and multiparty computation[END_REF][START_REF] Damgård | Multiparty computation from somewhat homomorphic encryption[END_REF].

Contributions. We provide the following results:

• A protocol P-MPWP, improving on MPWP, which reduces both the computational cost, by allowing the use of Paillier's cryptosystem, and the communication cost, from O n 3 to O n 2 . • An O (n) time and communications protocol Distributed and Secure Dot-Product (DSDP i ) (for i participants) which allows us to securely compute a dot product UV , against a semi-honest adversary, where one player owns a vector U and where each player knows one coefficient of V .

• A parallel variant that performs the dot-product computation in parallel among the players, limits the total number of rounds. This is extended to a Parallel Distributed and Secure Matrix-Multiplication (PDSMM i ) family of protocols. • A security analysis of the DSDP protocol using a cryptographic protocol verification tool, here ProVerif [START_REF] Blanchet | An efficient cryptographic protocol verifier based on prolog rules[END_REF][START_REF] Blanchet | Cryptographic Protocol Verifier User Manual[END_REF]. This tool allows us to define countermeasures for each found attack: adapted proofs of knowledge in order to preserve privacy and a random ring order, where private inputs are protected as in a wiretap code [START_REF] Ozarow | Wire-tap channel II[END_REF] and where the players take random order in the protocol to preserve privacy with high probability, even against a coalition of malicious insiders. • Finally, we show how to use these protocols for the computation of trust aggregation, where classic addition and multiplication are replaced by more generic operations, defined on monoids.

In Section 2, we thus first recall some multi-party computation notions. We then introduce in Section 3 the trust model based on monoids. In Section 4, we present our quadratic variant of MPWP and a linear-time protocol in Section 5. We then give the associated security proofs and countermeasures in Section 6 and present parallelized version in Section 7. Finally, in Section 8, we show how our protocols can be adapted to perform a private multi-party trust computation in a network.

Background and Definitions

We use a public-key homomorphic encryption scheme where both addition and multiplication are considered. There exist many homomorphic cryptosystems, see for instance (Mohassel, 2011, § 3) and references therein. We need the following properties on the encryption function E (according to the context, we use E PubB , or E 1 or just E to denote the encryption function, similarly for the signature function, D 1 or D privB ): computing several modular additions, denoted by Add(c 1 ; c 2 ), on ciphered messages and one modular multiplication, denoted by Mul(c; m), between a ciphered message and a cleartext.

That is,

∀m 1 , m 2 ∈ Z/mZ: Add(E(m 1 ); E(m 2 )) = E(m 1 + m 2 mod m) and Mul(E(m 1 ); m 2 ) = E(m 1 m 2 mod m).
For instance, Paillier's or Benaloh's cryptosystems (Paillier, 1999;[START_REF] Benaloh | Dense probabilistic encryption[END_REF][START_REF] Fousse | Benaloh's dense probabilistic encryption revisited[END_REF] can satisfy these requirements, via multiplication in the ground ring for addition of enciphered messages (Add(E(m 1 ); E(m 2 )) = E(m 1 )E(m 2 ) mod m), and via exponentiation for ciphered multiplication (Mul(E(m 1 ); m 2 ) = E(m 1 ) m 2 mod m), we obtain the following homomorphic properties:

E(m 1 )E(m 2 ) = E(m 1 + m 2 mod m) (1) E(m 1 ) m 2 = E(m 1 m 2 mod m) (2)
Since we consider the semantic security of the cryptosystem, we assume that adversaries are probabilistic polynomial time machines. In MPC, most represented intruders are the following ones:

• Semi-honest (honest-but-curious) adversaries: a corrupted player follows the protocol specifications, but also tries to gather as many information as possible in order to deduce some private inputs. • Malicious adversaries: a corrupted player that controls the network and stops, forges or listens to messages in order to gain information.

Monoids of Trust

There are several schemes for evaluating the transitive trust in a network. Some use a single value representing the probability that the expected action will happen; the complementary probability being an uncertainty on the trust. Others include the distrust degree indicating the probability that the opposite of the expected action will happen [START_REF] Guha | Propagation of trust and distrust[END_REF]). More complete schemes can be introduced to evaluate trust: Jøsang introduces the Subjective Logic notion which expresses beliefs about the truth of propositions with degrees of "uncertainty" in [START_REF] Jøsang | Probabilistic logic under uncertainty[END_REF]. Then the authors of [START_REF] Huang | A formal-semanticsbased calculus of trust[END_REF] applied the associated calculus of trust to public key infrastructures. There, trust is represented by a triplet, (trust, distrust, uncertainty) for the proportion of experiences proved, or believed, positive; the proportion of experiences proved negative; and the proportion of experiences with unknown character. As uncertainty = 1-trust -distrust, it is sufficient to express trust with two values as trust, distrust . In e.g. [START_REF] Foley | Aggregating trust using triangular norms in the keynote trust management system[END_REF] algorithms are proposed to quantify the trust relationship between two entities in a network, using transitivity and reachability. For instance, in [START_REF] Dumas | Matrix powers algorithm for trust evaluation in PKI architectures[END_REF] the authors use an adapted power of the adjacency matrix to evaluate the trust using all existing (finite) trust paths between entities. We show in the following of this section, that powers of this adjacency matrix can be evaluated privately in a distributed manner, provided than one disposes of an homomorphic cryptosystem satisfying the homomorphic Properties (1) and (2).

Aggregation of Trust

Consider Alice trusting Bob with a certain trust degree, and Bob trusting Charlie with a certain trust degree. The sequential aggregation of trust formalizes a kind of transitivity to help Alice to make a decision about Charlie, that is based on Bob's opinion. In the following, we first consider that the trust values are given as a pair a, b ∈ D 2 , for D a principal ideal ring: for three players P 1 , P 2 and P 3 , where P 1 trusts P 2 with trust value a, b ∈ D 2 and P 2 trusts P 3 with trust value c, d ∈ D 2 the associated sequential aggregation of trust is a function : c, d = ac + bd, ad + bc . Similarly, from Alice to Charlie, there might be several ways to perform a sequential aggregation (several paths with existing trust values). Therefore it is also possible to aggregate these parallel paths with the same measure, in the following way: for two disjoint paths Proof. As a + 0a.0, b.1 = a, b , 0, 1 is neutral for . Then, for b invertible, if a = 0, then 0, b -1 is an inverse for 0, b . Otherwise, for a -1 invertible,

D 2 × D 2 → D 2 ,
a(a -1) -1 , b -1 a, b = a, b a(a -1) -1 , b -1 = a + a(a -1) -1 -a 2 (a -1) -1 , bb -1 = 0, 1 . Similarly, if a, b
c, d = 0, 1 , then bd = 1 and b is invertible. Then also (a -1)c = a. Finally if a = 0 and a -1 is a zero divisor, there exists λ = 0 such that λ(a -1) = 0, thus λ(a -1)c = 0 = λa, but then λ(a -1)λa = -λ = 0. As this is contradictory, the only possibilities are a = 0 or a -1 invertible.

Multi-party Private Aggregation

For E an encryption function, we define the natural morphism on pairs, so that it can be applied to trust values: E( a, b ) = E(a), E(b) .We can thus extend homomorphic properties to pairs so that the parallel and sequential aggregation can then be computed homomorphically, provided that one entry is in clear.

Lemma 2. With an encryption function E, satisfying the homomorphic Properties (1) and (2), we have:

Mul(E ( a, b ) ; c, d ) = E ( a, b c, d ) = E(a) c E(b) d , E(a) d E(b) c Add(E ( a, b ) ; c, d ) = E ( a, b c, d ) = E(a)E(c)E(a) -c , E(b) d
Moreover, those two functions can be computed on an enciphered a, b , provided that c, d is in clear.

Proof. From the homomorphic properties of the encryption functions, we have: This shows, that in order to compute the aggregation of trust privately, the first step is to be able to compute dot-products privately.

E(a) c E(b) d = E(ac + bd), E (
4 From MPWP to P-MPWP

MPWP description

The MPWP protocol [START_REF] Dolev | Computing multi-party trust privately: in O(n) time units sending one (possibly large) message at a time[END_REF] is used to securely compute private trust values in an additive reputation system between n players. Each player P i (excepted P 1 , assumed to be the master player) has a private entry v i , and P 1 private entries are weights u i associated to others players. The goal is to compute a weighted average trust, i.e., ∑ n i=2 u i * v i . The idea of MPWP is the following: the first player creates a vector TV containing her private entries ciphered with her own public key using Benaloh's cryptosystem, i.e., TV = [E 1 (w 2 ), . . . , E 1 (w n )]. Then, P 1 also sends a (n -1) × (n -1) matrix M, with all coefficients initialized to 1 and a variable A = 1. Once (M, TV, A) received, each player computes:

A = A * E 1 (u i ) v i * E 1 (z i )
, where z i is a random value generated by P i . At the end, the first player gets

D 1 (A) = ∑ n i=2 u i v i + z i .
Then, the idea is to cut the z i values in n -1 positive shares such that z i = ∑ n j=2 z i, j . Next, each z i, j is ciphered with the public key of P j , the result is stored into the i th column of M, and M is forwarded to the next player. In a second phase, players securely remove the added random values to A, from M = (m i, j ) = (E j (z i, j )): each player P j , except P 1 , computes her PSS j = ∑ n i=2 D j (m i, j ) = ∑ n i=2 z i, j by deciphering all values contained in the j th row of M; then they send γ j = E 1 (PSS j ) to P 1 , their PSS i ciphered with the public key of P 1 . At the end, P 1 retrieves the result by computing

Trust = D 1 (A) -∑ n j=2 D 1 (γ j ) = D 1 (A) -∑ n j=2 PSS j = D 1 (A) -∑ n j=2 ∑ n i=2 z i, j = D 1 (A) -∑ n i=2 z i = ∑ n i=2 u i v i .

P-MPWP: A lighter MPWP

P-MPWP is a variant of MPWP with two main differences: first Paillier's cryptosystem is used instead of Benaloh's, and, second, the overall communications cost is reduced from O n 3 to O n 2 by sending parts of the matrix only. All steps of P-MPWP but those clearly identified in the following are common with MPWP, including the players' global settings. Since P-MPWP is using a cryptosystem where players can have different modulus, some requirements must be verified in the players' settings. First of all, a bound B needs to be fixed for the vectors' private coefficients:

∀i, 0 ≤ u i ≤ B, 0 ≤ v i ≤ B (3)
With Benaloh, the common modulus M must be greater than the dot product, thus at most:

(n -1)B 2 < M. (4)
Differently, with Paillier, each player P i has a different modulus N i . Then, by following the MPW P protocol steps, at the end of the first round, P 1 obtains

A = ∏ n i=2 E 1 (u i ) v i * E 1 (z i ).
In order to correctly decipher this coefficient, if the players' values, as well as their random values z i , satisfy the bound (3), her modulo N 1 must be greater than (n -1)(B 2 + B). For others players, there is only one deciphering step, at the secound round. They received (n -1) shares all bounded by B. Hence, their modulus N i need only be greater than (n -1)B. These modulus requirements are summarized in the following lemma: Lemma 3. Let n > 3 be the number of players. Under the bound (3), if ∀i, 0 ≤ z i ≤ B and if also the modulus satisfy (n -1)(B 2 + B) < N 1 and (n -1)B < N i , ∀i = 2, . . . , n, then at the end of P-MPWP, P 1 obtains S n = ∑ n i=2 u i * v i . Now, the reduction of the communications cost in P-MPWP, is made by removing the exchange of the full M matrix between players. At the z i, j shares computation, each P i directly sends the j th coefficient to the j th player instead of storing results in T . In the end, each player P i receives (n -1) values ciphered with his public key, and he can compute the PSS i by deciphering and adding each received values, exactly as in MPW P. Thus, each player sends only O (n) values, instead of O n 2 . All remaining steps can be executed as in MPWP.

Both Paillier's and Benaloh's cryptosystems provides semantic security, thus the security of P-MPWP is not altered. Moreover, since a common bound is fixed a priori on private inputs, P-MPWP security can be reduced to the one in MPWP with the common modulo M between all players [START_REF] Michalas | Vulnerabilities of decentralized additive reputation systems regarding the privacy of individual votes[END_REF]. Finally, since all exploitable (i.e., clear or ciphered with the dedicated key) information exchanged represents a subset of the MPWP players' knowledge, if one is able to break P-MPWP privacy, then one is also able to break it in MPWP.

A Linear Dot Product Protocol

Overview with Three Players

We first present in Figure 1 our DSDP 3 protocol (Distributed and Secure Dot-Product), for 3 players. The idea is that Alice is interested in computing a dimension 3 dot-product S = u T • v, between her vector u and a vector v whose coefficients are owned by different players. The other players send their coefficients, encrypted, to Alice. Then she homomorphically multiplies each one of these by her u i coefficients and masks the obtained u i v i by a random value r i . Then the other players can decrypt the resulting u i v i + r i : with two unknowns u i and r i they are not able to recover v i . Finally the players enter a ring computation of the overall sum before sending it to Alice. Then only, Alice removes her random masks to recover the final dot-product. Since at least two players have added u 2 v 2 + u 3 v 3 , there is at least two unknowns for Alice, but a single equation.

We need that after several decryptions and re-encryptions, and removal of the random values r i , S is exactly ∑ u i v i .

The homomorphic Properties (1) and ( 2) only guaranty that D(Add(Mul(E(v i ); u i ); r i )) = v i u i + r i mod N i , for the modulo N i of the cryptosystem used by player P i . But then these values must be re-encrypted with another player's cryptosystem, potentially with another modulo. Finally Alice also must be able to remove the random values and recover S over Z. On the one hand, if players can share the same modulo M = N i for the homomorphic properties then decryptions and re-encryptions are naturally compatible. This is possible for instance in Benaloh's cipher. On the other hand, in a Paillier-like cipher, at the end of the protocol, Alice will actually recover

S 4 = ((u 2 v 2 + r 2 ) mod N 2 + u 3 v 3 + r 3 ) mod N 3 . He can remove r 3 , via S 3 = S 4 -r 3 mod N 3 , but then S 3 = ((u 2 v 2 + r 2 ) mod N 2 + u 3 v 3 ) mod N 3 . Now, if
vectors coefficients are bounded by say B, and if the third modulo is larger than the second, N 3 > N 2 + B 2 , the obtained value is actually the exact value over the naturals:

S 3 = (u 2 v 2 + r 2 ) mod N 2 + u 3 v 3 . Then Alice can re- move the second random value, this time modulo N 2 : S 2 = (u 2 v 2 + u 3 v 3 ) mod N 2 , where now N 2 > 2B 2
suffices to recover S = S 2 ∈ N. We generalize this in the following section.

General Protocol with n Players

We give the generalization DSDP n , of the protocol of Figure 1 for n players in Algorithm 4 hereafter. For this protocol to be correct, we use the previously defined bound (3) on the players' private inputs. Then, for n players, there are two general cases: Fisrt, if all the players share the same modulo M = N i for all i for the homomorphic properties, then Alice can also use M to remove the r i . Then, to compute the correct value S, it is sufficient to satisfy the bound (4). Second, for a Paillier-like cipher, differently, the modulo of the homomorphic properties are distinct. We thus prove the following Lemma 5. Lemma 5. Under the bound (3), and for any r i , let

M 2 = (u 2 v 2 +r 2 ) mod N 2 and M i = (M i-1 +u i v i +r i ) mod N i , for i = 2 . . . n -1. Let also S n+1 = M n and S i = (S i+1 -r i ) mod N i for i = n . . . 2. If we have: N i-1 + (n -i + 1)B 2 < N i , for all i = 3..n (n -1)B 2 < N 2 (5) then S 2 = ∑ n i=2 u i v i ∈ N. Proof. By induction, we first show that S i = M i-1 + ∑ n j=i u j v j , for i = n..3: indeed S n = (M n -r n )
Algorithm 4 DSDP n Protocol: Distributed and Secure Dot-Product of size n Require: n ≥ 3 players, two vectors U and V such that P 1 knows complete vector U, and each players P i knows component v i of V , for i = 1 . . . n; Require: E i (resp. D i ), encryption (resp. decryption) function of P i , for i = 2 . . . n. Ensure: P 1 knows the dot-product S = U T V .

1: for i = 2 . . . n do {P i :

c i = E i (v i ); P i c i → P 1 } 2: for i = 2 . . . n do 3: P 1 : r i $ ← Z/N i Z 4: P 1 : α i = c u i i * E i (r i ) so that α i = E i (u i v i + r i ) 5: P 1 α 2 → P 2 6: for i = 2 . . . n -1 do P 1 : α i+1 → P i 7: P 2 : ∆ 2 = D 2 (α 2 ) so that ∆ 2 = u 2 v 2 + r 2 8: P 2 : β 3 = α 3 * E 3 (∆ 2 ) so that β 3 = E 3 (u 3 v 3 + r 3 + ∆ 2 ); P 2 β 3 → P 3 9: for i = 3 . . . n -1 do 10: P i : ∆ i = D i (β i ) so that ∆ i = ∑ i k=2 u k v k + r k
11:

P i : β i+1 = α i+1 * E i+1 (∆ i ) so that β i+1 = E i+1 (u i+1 v i+1 + r i+1 + ∆ i ); P i β i+1 → P i+1 12: P n : ∆ n = D n (β n ); P n : γ = E 1 (∆ n ); P n γ → P 1 13: return P 1 : S = D 1 (γ) -∑ n-1 i=1 r i + u 1 v 1 . mod N n = (M n-1 + u n v n ) mod N n . But M n-1 is modulo N n-1 , so (M n-1 + u n v n ) < N n-1 + B 2
, and then (5

) for i = n, ensures that N n-1 + B 2 < N n and S n = M n-1 + u n v n ∈ N. Then, for 3 ≤ i < n, S i = (S i+1 -r i ) mod N i = (M i + ∑ n j=i+1 u j v j - r i ) mod N i = (M i-1 + u i v i + r i + ∑ n j=i+1 u j v j -r i ) mod N i = (M i-1 + ∑ n j=i u j v j ) mod N i , by induction. But (3) enforces that M i-1 + ∑ n j=i u j v j < N i-1 + (n - i + 1)B 2 and
(5) also ensures the latter is lower than N i . Therefore S i = M i-1 + ∑ n j=i u j v j and the induction is proven. Finally,

S 2 = (S 3 -r 2 ) mod N 2 = (M 2 + ∑ n j=3 u j v j -r 2 ) mod N 2 = (∑ n j=2 u j v j ) mod N 2 . As ∑ n j=2 u j v j < (n -1)B 2
, by (5) for i = 2, we have S 2 = ∑ n j=2 u j v j ∈ N. This shows that the DSDP n protocol of Algorithm 4 can be implemented with a Paillier-like underlying cryptosystem, provided that the successive players have increasing modulo for their public keys. to P 1 , then homomorphically added to random values, r i . Then, P i (i ≥ 2) deciphers the message received by P i-1 into ∆ i . By induction, we obtain

c 2 = E pubB (v 2 ) c 3 = E pubC (v 3 ) c 2 o o c 3 o o α 2 = c u 2 2 * E pubB (r 2 ) α 3 = c u 3 3 * E pubC (r 3 ) α 2 , α 3 / / ∆ 2 = D privB (α 2 ) {now ∆ 2 is (v 2 u 2 + r 2 )} β 3 = α 3 * E pubC (∆ 2 ) β 3 / / ∆ 3 = D privC (β 3 ) {now ∆ 3 is (v 3 u 3 + r 3 ) + (v 2 u 2 + r 2 )} γ = E pubA (∆ 3 ) γ o o S = D privA (γ) -r 2 -r 3 + u 1 v 1 {now S is u 1 v 1 + u 2 v 2 + u 3 v 3 }
∆ i = ∑ i k=2 u k v k + r k .
This value is then re-enciphered with next player's key and the next player share is homomorphically added. Finally, P 1 just has to remove all the added randomness to obtain

S = ∆ n -∑ n i=2 r i + u 1 v 1 = ∑ n i=1 u i v i .
For the complexity, the protocol needs n -1 encryptions and communications for the c i ; 2(n -1) homomorphic operations on ciphers and n -1 communications for the α i ; n -1 decryptions for the ∆ i ; n -1 encryptions, homomorphic operations and communications for the β i ; and finally one encryption and one communication for γ. Then P 1 needs O (n) operations to recover S.

Security of the DSDP protocol

We study the security of DSDP n using both mathematical proofs and automated verifications. We first demonstrate the security of the protocol for semihonest adversaries. Then we incrementally build its security helped by attacks found by ProVerif, an automatic verification tool for cryptographic protocols.

Security Proofs

The standard security definition in MPC models (Lindell, 2009) covers actually many security issues, such as correctness, inputs independence, privacy, etc. We first prove that under this settings, computation of the dot product is safe.

Lemma 7. For n ≥ 3, the output obtained after computing a dot product where one player owns complete vector U, and where each coefficient v i of the second vector V is owned by the player P i , is safe.

Proof. After executing DSDP n with n ≥ 3, P 1 received the dot product of U and V . Therefore, it owns only one equation containing (n -1) unknown values (coefficients from v 2 to v n ). Then, he cannot deduce other players' private inputs.

Then, proving the security relies on a comparison between a real-world protocol execution and an ideal one. The latter involves an hypothetical trusted third party (T T P) which, knowing only the players' private inputs, returns the correct result to the correct players. The protocol is considered secure if the players' views in the ideal case cannot be distinguished from the real ones. Views of a player P i (denoted View P i ) are defined as distributions containing: the players' inputs (including random values), the messages received during a protocol execution and the outputs. The construction of the corrupted players' view in the ideal world is made by an algorithm called Simulator. Definition 8. In the presence of a set C of semi-honest adversaries with inputs set X C , a protocol Π securely computes f : ([0, 1] * ) m → ([0, 1] * ) m (and f C denotes the outputs of f for each adversaries in C) if there exists a probabilistic polynomial-time algorithm Sim, such that:

{Sim(C, {X C }, f C (X))} X∈([0,1] * ) m is compu- tationally indistinguishable from {C, {View Π P i } P i ∈C }.
For DSDP n , it is secure only if C is reduced to a singleton, i.e. if only one player is corrupted.

Lemma 9. By assuming the semantic security of the cryptosystem E, for n ≥ 3, DSPD n is secure against one semi-honest adversary.

Proof. We assume that the underlying cryptosystem E is semantically secure (IND-CPA secure). First, we suppose that only P 1 is corrupted. His view, in a real execution of the protocol, is View P 1 = {U, R, γ, S, A, B,C}, where U = {u i } 1≤i≤n , R = {r i } 1≤i≤n , A = {α i } 2≤i≤n , B = {β i } 3≤i≤n-1 and C = {c i } 2≤i≤n . Now, Sim 1 is the simulator for P 1 in the ideal case, where a simulated value x is denoted x : by definition, P 1 's private entries (vectors U and R) are directly accessible to Sim 1 , along with the output S, sent by the T T P. Sim 1 starts by generating n -2 random values, and then ciphers them using the corresponding public keys: this simulates the c i values. Then, using the provided r i and u i with the associated c i and P i 's public key, Sim 1 computes:

α i = c u i i * E i (r i ), 2 ≤ i ≤ n.
Next, the simulation of B is done by ciphering random values with the appropriate public key. The γ value is computed using R along with the protocol output S: γ = E 1 (S + ∑ n-2 i r i + u 1 v 1 ). In the end, the simulator view is View Sim 1 = {U, R, γ , S, A , B ,C }. If an adversary is able to distinguish any ciphered values (e.g. C from C and thus A from A), hence he is able to break the semantic security of the underlying cryptographic protocol. This is assumed impossible. Moreover, since the remaining values are computed as in a real execution, P 1 is not able to distinguish View P 1 from View Sim 1 . Second, we suppose that a player P i , i ≥ 2 is corrupted and denote by Sim i the simulator in this case. Since the role played by each participant is generic, (except for P n , which only differs by his computation of γ instead of β n+1 ), the simulators are easily adaptable. During a real protocol execution, the view of P i is View P i = {v i , A, B,C, γ, ∆ i }. Simulating the values also known to P 1 is similar, up to the used keys. Hence, the simulation of A , B , γ , C (except c i ) is made by ciphering random values using the adequate public key. c i is ciphered using v i and the public key of P i . For ∆ i , the simulator Sim i has to forward the random value previously chosen to be ciphered as α i . Indistinguishability is based on the semantic security of E (for A, B, C and γ) and on the randomness added by P 1 (and thus unknown by P i ). Then, ∆ i is computationally indistinguishable from the real ∆ i . Hence, View P i and View S i are indistinguishable and DSDP n is secure against one semi-honest adversary.

Automated Verification

Alongside mathematical proofs, we use an automatic protocol verification tool to analyze the security of the protocol. Among existing tools, we use ProVerif [START_REF] Blanchet | An efficient cryptographic protocol verifier based on prolog rules[END_REF][START_REF] Blanchet | Cryptographic Protocol Verifier User Manual[END_REF]. It allows users to add their own equational theories to model a large class of protocols. In our case, we model properties of the underlying cryptosystem including addition and multiplication. Sadly, verification of protocol in presence of homomorphic function over abelian groups theory has been proven undecidable [START_REF] Delaune | An undecidability result for agh[END_REF]. Moreover, as showed in [START_REF] Lafourcade | Performance evaluations of cryptographic protocols verification tools dealing with algebraic properties[END_REF], some equational theories such as Exclusive-Or can already outspace the tool's capacities. Thus we have to provide adapted equational theories to be able to obtain results with the tool. We modeled the application of Pailler's or shared modulus encryption properties on α i messages that Bob receives as follows:

(i). ∀u, v, r, k, bob(E k (r), u, E k (v)) = E k (uv + r)
This property allows Bob to obtain u 2 v 2 + r 2 from α 2 . This also allows an intruder to simulate such calculus and impersonate Bob. We also model: r,x,y,z,a,b,c,k,dave(E k

(ii). β 3 by ∀u, v, r, x, y, z, k, charlie(E k (uv + r), E k (xy + z)) = E k (uv + xy + r + z) (iii). β 4 by ∀u, v,
(uv + xy + r + z), E k (ab + c)) = E k (uv + xy + ab + r + z + c)
In the following, we use ProVerif to prove the security of our protocols under the abstraction of the functionalities given in our equational theory. ProVerif discovers some attacks in presence of active intruder. We then propose some countermeasures. The limits of ProVerif are reached and it does not terminate. The associated source files are available in a web-site: matmuldistrib.forge.imag.fr.

Analysis in case of a passive adversary. Using these equational theories on the protocol described in Figure 1, we verify it in presence of a passive intruder. Such adversary is able to observe all the traffic of the protocol and tries to deduce secret information of the messages. This corresponds to a ProVerif intruder that only listens to the network and does not send any message. By default, this intruder does not possess the private key of any agent and thus does not belong to the protocol. To model a semi-honest adversary as defined in Section 2, we just give secret keys of honest participants to the passive intruder knowledge in ProVerif. Then the tool proves that all secret terms cannot be learn by the intruder for any combinations of leaked key. This confirms the proofs given in Section 6.1 against the semi-honest adversaries.

Analysis in case of malicious adversary. The malicious adversary described in Section 2 is an active intruder that controls the network and knows a private key of a compromised honest participant. Modeling this adversary in ProVerif, we are able to spot the two following attacks and give some countermeasures: (i) Only the key of Alice is compromised and the countermeasure uses proofs of knowledge.

Intruder(Alice)

Bob Charlie

c 2 =E pubB (v 2 ) o o α 2 = c uI 2 * E pubB (r I ) x 3 = E pubC (v I ) α 3 = x u I 3 * E pubC (r I ) α 2 ,α 3 / / ∆ 2 = D privB (α 2 ) {now ∆ 2 is (v 2 u I + r I )} β 3 =α 3 * E pubC (∆ 2 ) / / ∆ 3 = D privC (β 3 ) {now ∆ 3 is (v I u I + r I ) + (v 2 u I + r I )} γ=E pubA (∆ 3 ) o o v 2 = (D privA (γ) -v I u I -r I -r I )u -1 I Figure 2: Attack on the secrecy of v 2
(ii) Only the key of Charlie is compromised and the countermeasure uses signatures. In the rest of the section, we present these two points. In the Section 7.2, we also give a solution called random ring for the case where both keys of Alice and Charlie are compromised.

(i) The key of Alice is compromised. An attack on the secrecy of v 2 , the secret generated by Bob, is then presented in Figure 2.

The malicious adversary usurps Alice and replaces all the α i messages, arriving from the other agents, with one message she generated, except one message, denoted c 2 in Figure 2. He lets the protocol end normally and obtains a term where only v 2 is unknown. He learns v 2 . If the key of Alice (P 1 ) is compromised, ProVerif also finds an attack on any of the other players secrecy. Suppose, w.l.o.g, that P 2 is the target, P 1 replaces each α i except α 2 by ciphers E i (x i ) where x i are known to him. x i = 0 could do for instance (x i = 0v i + r i also), since after completion of the protocol, P 1 learns u 2 v 2 + r 2 + ∑ n i=3 x i , where the u i and r i are known to him. Therefore, P 1 learns v 2 . Note also that similarly, for instance, α 2 = 1v 2 +0 and x 3 = v 3 could also reveal v 2 to P 3 . Counter measure: this attack, and more generally attacks on the form of the α i can be counteracted by zero-knowledge proofs of knowledge. P 1 has to prove to the other players that α i is a non trivial affine transform of their secret v i . For this we use a variant of a proof of knowledge of a discrete logarithm [START_REF] Chaum | Demonstrating possession of a discrete logarithm without revealing it[END_REF] given in Figure 3.

In the Protocol 4, this proof of a non trivial affine transform applies as is to α 2 with µ 2 = g u 2 , ρ 2 = g r 2 so that the check of P 2 is δ 2 = g ∆ 2 ?

== µ v 2 2 ρ 2 . Differently, for the subsequent players, the δ i-1 = g ∆ i-1 used to test must be forwarded: indeed the subsequent players have to check in line 10 that ∆ i = u i v i + r i + ∆ i-1 . Thus with P 1 providing µ i = g u i , ρ i = g r i and P i-1 providing δ i-1 , the check of player P i ends with

δ i = Alice Public: g Bob c = E pubB (v) c o o α = E pubB (uv + r) µ = g u and ρ = g r α, µ, ρ / / Check µ = 1, µ = g so that u = 0, u = 1 Check ρ = 1, ρ = g so that r = 0, r = 1 ∆ = D privB (α) if ∆ = uv + r Check g ∆ ? == µ v ρ then g uv+r = (g u ) v g r
g ∆ i ? == µ v i i ρ i δ i-1 .
As for proofs of knowledge of discrete logarithm, secrecy of our proof of non trivial affine transform is guaranteed as long as the discrete logarithm is difficult. The overhead in the protocol, in terms of communications, is to triple the size of the messages from P 1 to P i , with α i growing to (α i , µ i , ρ i ), and to double the size of the messages from P i to P i+1 , with β i growing to (β i , δ i ). In terms of computations, it is also a neglectible linear global overhead.

(ii) The key of Charlie is compromised. There ProVerif finds another attack on the secrecy of v 2 . This time the key of Charlie is compromised and the malicious adversary blocks all communications to and from Alice who is honest. The adversary performs the same manipulation on the α i terms which are directly sent to Bob. Thus, this attack becomes feasible since the adversary knows the terms u 2 , u 3 , r 2 , r 3 and v 3 that he generated and ∆ 3 = (v 2 u 2 + r 2 ) + (v 3 u 3 + r 3 ) using the private key of Charlie. Such an attack relies on the fact that Bob has no way to verify if the message he receives from Alice has really been sent by Alice. This can be avoided using cryptographic signatures.

This attack can be generalized to any number of participants. The attack needs the adversary to know the key of Alice (since she is the only one to know the u i and r i values thanks to the signatures). Then, to obtain the secret value of a participant P i , the key of participants P i-1 and P i+1 are also needed:

(i). P i-1 knows ∆ i-1 = (u 2 v 2 + ... + u i-1 v i-1 + r 2 + ... + r i-1 ). (ii). P i+1 knows ∆ i+1 = (u 2 v 2 + ... + u i-1 v i-1 + u i v i + u i+1 v i+1 + r 2 + ... + r i-1 + r i + r i+1 ).
Thus, by simplifying ∆ i-1 and ∆ i+1 , the malicious adversary obtains u i v i + u i+1 v i+1 + r i + r i+1 where he can remove u i+1 , v i+1 , r i , r i+1 and u i to obtain v i . For more than three participants, we see in Section 7.2 that these kinds of threats can be diminished if the protocol is replayed several times in random orders.

In order to speed up the overall process, we show that we can cut each dot-product into blocks of 2 or 3 coefficients. On the one hand, the overall volume of communications is unchanged, while the number of rounds is reduced from n to a maximum of 5. On the other hand, semantic security is dropped, but we will see at the end of this section that by simply repeating the protocol with a wiretap mask it is possible to make the probability of breaking the protocol negligible.

An application of the DSDP n protocol is the computation of matrix multiplication. In this case, instead of knowing one vector, each player P i owns two rows, A i and B i , one of each n × n matrices A and B. At the end, each P i learns a row C i of the matrix C = AB. In order to compute the matrix product, it is therefore natural to parallelize DSDP n : each dot-product is cut into blocks of 2 or 3 coefficients. Indeed, scalar product between three players (resp. four) involves two (resp. three) new coefficients in addition to the ones already known by P i . For P 1 , the idea is to call DSDP 3 on the coefficients u 1 , v 1 and u 2 , u 3 of P 1 , and v 2 , v 3 of P 2 and P 3 . Then P 1 knows s = u 1 v 1 + u 2 v 2 + u 3 v 3 . P 1 can then continue the protocol with P 4 and P 5 , using (s, 1) as his first coefficient and u 4 , u 5 to be combined with v 4 , v 5 , etc. P 1 can also launch the computations in parallel. Then P 1 adds his share u 1 v 1 only after all the computations. For this it is sufficient to modify line 13 of DSDP n as: P 1 : S = D 1 (γ) -∑ n-1 i=1 r i . This is given as the ESDP n protocol variant in Algorithm 10.

Algorithm 10 ESDP n Protocol: External Secure Dot-Product of size n Require: n + 1 players, P 1 knows a coefficient vector U ∈ F n , each P i knows components v i-1 of V ∈ F n , for i = 2 . . . n + 1. Ensure: P 1 knows S = U T V .

return DSDP n+1 (P 1 . . . P n+1 , [0,U], [0,V ]).

Partition in Pairs or Triples

Depending on the parity of n, and since gcd(2, 3) = 1, calls to ESDP 2 and ESDP 3 are sufficient to cover all possible dot-product cases, as shown in protocol PDSMM n of Algorithm 11. The protocol is cut in two parts. The loop allows us to go all over coefficients by block of size 2. In the case where n is even, a block of 3 coefficients is treated with an instance of ESDP 3 .

In terms of efficiency and depending on the parity of n, ESDP 2 is called n-1 2 or n 2 -2 times, and ESDP 3 is called 0 or 1 times. for Each column: j=1 . . . n do 3:

s ← a i,i b i, j 4:
if n is even then 5: Proof. Correctness means that at the end, each P i has learnt row C i of C = AB. Since the protocol is applied on each rows and columns, let us show that for a row i and a column j, Algorithm 11 gives the coefficient c i j such that c i j = ∑ n k=1 a ik * b k j . First, the k i coefficients are just the values 1 . . . (i -1) and (i + 1) . . . n in order. Then, the result of any ESDP 2 step is a i,k 1 b k 1 , j + a i,k 2 b k 2 , j and the result of the potential

k 1 ← (i -1) mod n + 1; k 2 ← (i -2) mod n + 1; k 3 ← (i -3) mod n + 1; 6: s ← s + ESDP 3 (P i , [P k 3 , P k 2 , P k 1 ], [a i,k 3 , a i,k 2 , a i,k 1 ], [b k 3 , j , b k 2 , j , b k 1 , j ]) 7: t ← n-4
k 1 ← (i + 2h -1) mod n + 1; k 2 ← (i + 2h) mod n + 1; 12: s ← s + ESDP 2 (P i , [P k 1 , P k 2 ], [a i,k 1 , a i,k 2 ], [b k 1 , j , b k 2 , j ])
ESDP 3 step is a i,k 3 b k 3 , j + a i,k 2 b k 2 , j + a i,k 1 b k 1 , j .
Therefore accumulating them in addition of a i,i * b i, j produces as expected c i j = ∑ n k=1 a ik * b k j . Now for the number of rounds, for all i and j, all the ESDP calls are independent. Therefore, if each player can simultaneously send and receive multiple data we have that: in parallel, ESDP 2 , like DSDP 3 in Figure 1, requires 4 rounds with a constant number of operations: one round for the c i , one round for the α i , one round for β 3 and one round for γ. As shown in Algorithm 4, ESDP 3 , like DSDP 4 , requires only a single additional round for β 4 .

Random Ring Order Mitigation

We have previously seen that if the first player of a dot-product cooperates with the third one she can always recover the second player private value. If the first player cooperates with two well placed players she can recover the private value of a player in between. In the trust evaluation setting every malicious player plays the role of the first player in its row and therefore as soon as there is a collaboration, there is a risk of leakage. To mitigate this cooperation risk, our idea is to repeat the dot product protocol in random orders, except for the first player. To access a given private value, the malicious adversaries have to be well placed in every occurrence of the protocol. Therefore if their placement is chosen uniformly at random the probability that they recover some private value diminishes with the number of occurrences. In practice, they use a pseudo, but unpredictable, random generator to decide their placement: as each of them has to know their placement, they can for instance use a cryptographic hash function seeded with the alphabetical list of the players distinguished names, with the date of the day and with random values published by each of the players. We detail the overall procedure only for one dot-product, within the PDSMM n protocol. Each player except the first one masks his coefficient v as in a simple wiretap channel [START_REF] Ozarow | Wire-tap channel II[END_REF], as sketched in Algorithm 13.

Algorithm 13 Wiretap repetition of the dot-product 1: The players agree on d occurrences. 2: Each player computes his placement order in each occurrence of the protocol from the cryptographic hash function. 3a: With a shared modulus cryptosystem, the players should share a common modulo M satisfying Hypothesis (4). In the first occurrence, each player P j then masks his private input coefficient v j with d -1 random values λ j,i ∈ Z/MZ: v j -∑ d i=2 λ j,i . 3b: With a Paillier-like cryptosystem, the players choose their moduli according to Hypothesis (5), where B 2 is replaced by dB 2 , in groups of size n = 4 (the requirements of (5) on the moduli are somewhat sequential, but can be satisfied independently if each modulo is chosen in a distinct interval larger than 3dB 2 ). Then, in the first occurrence, each player P j masks his private input coefficient v j with d -1 random values 0 ≤ λ j,i < B: v j + ∑ d i=2 (Bλ j,i ) < dB. 4: Then for each subsequent occurrence, each player replaces its coefficient by one of the λ j,i . 5: In the end, the first player has gathered d dotproducts and just needs to sum them in order to recover the correct one.

Theorem 14. Algorithm 13 correctly allows the first player to compute the dot-product.

Proof. First, in a shared modulus setting, after the first occurrence, Alice (P 1 ) gets S 1 = ∑ n j=2 u j v j -∑ d i=2 λ j,i . Then in the following occurrences, Alice gets S i = ∑ n j=2 u j λ j,i . Finally she computes ∑ d i=1 S i = ∑ n j=2 u j v j . Second, similarly, in a Paillier-like setting, after the first occurrence, Alice recovers S 1 = ∑ n j=2 u j v j + ∑ d i=2 (Bλ j,i ) . Then in the following occurrences, Alice gets

S i = ∑ n j=2 u j λ j,i . Finally she computes ∑ d i=1 S i - (d -1)B(∑ n j=2 u j ) = ∑ n j=2 u j (v j + (d -1)B) -(d - 1)Bu j = ∑ n j=2 u j v j .
We give now the probability of avoiding attacks in the case when n = 2t + 1, but the probability in the even case should be close.

Theorem 15. Consider n = 2t + 1 players, grouped by 3, of which k ≤ n -2 are malicious and cooperating, including the first one Alice. Then, it is on average sufficient to run Algorithm 13 with d ≤ 2 ln min{k -1, nk, n-1 2 } 1 + k-1 n-k-1 occurrences, to prevent the malicious players from recovering any private input of the non malicious ones.

Proof. The idea is that for a given private input of a non malicious player Bob, to be revealed to Alice, Bob needs to be placed between cooperating malicious adversaries at each occurrence of the protocol. If there is only one non malicious player, then nothing can be done to protect him. If there is 2 non malicious, they are safe if they are together one time, this happens with probability 1 n-2 , and thus on average after n -2 occurrences. Otherwise, PDSMM n uses t = n-1 2 groups of 3, including Alice. Thus, each time a group is formed with one malicious and one non malicious other players, Alice can learn the private value of the non malicious player. Now, after any occurrence, the number a of attacked players is less than the number of malicious players minus 1 (for Alice) and obviously less than the number of non malicious players: 0 ≤ a < min{k -1, n -k}. Thus let b = k -1a and c = nka. In the next occurrence, the probability of saving at least one more non malicious is a(a-1+c)(n-3)! (n-1)! n-1 2 = a(a-1+c) 2(n-2) = a(n-k-1) 2(n-2) , so that the average number of occurrences to realize this is E n,k (a) = 2(n-2) a(n-k-1) . Thus, T n,k (a), the average number of occurrences to save all the non malicious players, satisfies T n,k (a) ≤ E n,k (a) + T n,k (a -1) ≤ ∑ 3 i=a E n,k (i) + T n,k (2) = (∑ 3 i=a 1 i ) 2(n-2) n-k-1 + T n,k (2). With 2 attacked and c saved, T n,k=n-c-2 (2) = n-2 c+1 so that T n,k (a) ≤ (H a -3 2 ) 2(n-2) n-k-1 + n-2 n-k-1 , where bounds on the Harmonic numbers give H a ≤ ln a (see, e.g., [START_REF] Batir | Sharp bounds for the psi function and harmonic numbers[END_REF]) and since a ≤ k -1 and a ≤ nk, this shows also that 2a ≤ n -1. Therefore, T n,k (a) ≤ 2 ln min{k -1, nk, n-1 2 } n-2 n-k-1 . For instance, if k, the number of malicious insiders, is less than the number of non malicious ones, the number of repetitions sufficient to prevent any attack is on average bounded by O (log k). To guaranty a probability of failure less than ε, one needs to consider also the worst case. There, we can have k = n-2 malicious adversaries and the number of repetitions can grow to n ln(1/ε):

Proposition 16. With n = 2t + 1, the number d of random ring repetitions of Algorithm 13 to make the probability of breaking the protocol lower than ε satisfies d < n ln(1/ε) in the worst case.

Proof. There are at least 2 non-malicious players, otherwise the dot-product reveals the secrets in any case. Any given non-malicious player is safe from any attacks if in at least one repetition he was paired with another non-malicious player. In the worst case, k = n -2 players are malicious and the latter event arises with probability (1

-1 n-1 ) d for d repeti- tions. If d ≥ n ln ε -1 , then d > (n -1)(-ln ε) > ln ε ln(1-1 n-1 )
, which shows that (1 -1 n-1 ) d < ε.

Overall, the wiretap variant of Algorithm 13 can guaranty any security, at the cost of repeating the protocol. As the number of repetitions is fixed at the beginning by all the players, all these repetitions can occur in parallel. Therefore, the overall volume of communication is multiplied by the number of repetitions, while the number of rounds remains constant. This is summarized in Table 1 and Figure 4, for the average (Theorem 15) and worst (Proposition 16) cases of Algorithm 13, and where the protocols of the previous sections are also compared. On the one hand, we see in Figure 4 that quadratic protocols, with homomorphic encryption, are not usable for a realistic large group of players (trust aggregation could be used for instance by certificate authorities, and there are several hundreds of those in current operating systems or web browsers). On the other hand, quasi linear time protocols present good performance, while preserving some reasonable security properties: the average wiretap curve is on average sufficient to prevent any attack and still has a quasi linear asymptotic behavior. The steps in this curve are the rounding of log(n) to the next integer and correspond to one more random ring wiretap round.

→

  P 3 , the associated parallel aggregation of trust is a function : D 2 ×D 2 → D 2 , that computes the resulting trust value as: a, b c, d = a + cac, bd . We prove the following Lemma.

  Lemma 1. a, b is invertible for if and only if (b is invertible in D) and (a = 0 or a -1 is invertible).

  a) d E(b) c = E(ad + bc), E(a)E(c)E(a) -c = E(a+c+a(-c)) and E(b) d = E(bd). For the computation, both right hand sides depend only on ciphered values E(a), E(b), and on clear values c and d (E(c) can be computed with the public key, from c).

Theorem 6 .

 6 Under the bounds (3), and under Hypothesis (4) with a shared modulus underlying cipher, or under Hypothesis (5) with a Paillier-like underlying cipher, the DSDP n protocol of Algorithm 4 is correct. It requires O (n) communications and O (n) encryption and decryption operations. Proof. First, each player sends his ciphered entry Alice

Figure 1 :

 1 Figure 1: DSDP 3 : Secure dot product of vectors of size 3 with a Paillier-like asymetric cipher.

Figure 3 :

 3 Figure 3: Proof of a non trivial affine transform

  h = 1 . . .t do 11:

  Theorem 12. The PDSMM n Protocol in Algorithm 11 is correct. It runs in less than 5 parallel communication rounds.

Figure 4 :

 4 Figure 4: Quadratic and linear protocols timings

  Algorithm 11 PDSMM n Protocol: Parallel Distributed and Secure Matrix Multiplication Require: n players, each player P i knows rows A i and B i of two n × n matrices A, B. Ensure: Each player P i knows row i of C = AB.1: for Each row: i=1 . . . n do

	2:

Table 1 :

 1 Communication complexities

	Protocol	Volume	Rounds Paillier
	MPWP	O n 3	O (n)
	P-MPWP ( § 4)	n 2+o(1)	O (n)
	Alg. 13 (Wiretap) Alg. 4 (DSDP n )	n 2+o(1) ln 1 ε n 1+o(1)	5 O (n)
	Alg. 11 (PDSMM n )	n 1+o(1)	5
	Alg. 13 (Average)	n 1+o(1)	5

* This work was partially supported by "Digital trust" Chair from the University of Auvergne Foundation, by the HPAC project (ANR 11 BS02 013), the ARAMIS project (PIA P3342-146798) and the LabEx PERSYVAL-Lab (ANR-11-LABX-0025).

Conclusion: MPC of Trust

We now come back to the aggregation of trust. As shown in Section 3, the first step is to reduce the computation to that of dot-products. We show how to fully adapt the protocol of Section 5 to the evaluation of trust values with parallel and sequential aggregations:

Corollary 17. The protocol DSDP of Algorithm 4 can be applied on trust values, provided that the random values r i are invertible for .

Proof. • u i , v i , r i , c i , α i , β i , ∆ i , γ are now couples;

• Encryption and decryption (E(v i ), D(β i ), E(∆ i ), E(γ), etc.) now apply on couples, using the morphism

and can still be computed by P 1 , since c i = E(v i ) and u i and r i are known to him; • Similarly,

• Finally, as is commutative, S is recovered by adding the inverses for of the r i .

From (Dumas and Hossayni, 2012, Definition 11), the d-aggregation of trust is a dot-product but slightly modified to not include the value u 1 v 1 . Therefore at line 3, in the protocol of Algorithm 11, it suffices to set s to the neutral element of (that is s ← 0, 1 , instead of s ← a i, j b i, j ).

There remains to encode trust values that are proportions, in [0, 1], into D = Z/NZ. With n participants, we use a fixed precision 2 -p such that 2 n(2p+1) < N ≤ 2 n(2(p+1)+1) and round the trust coefficients to x2 p mod N from [0, 1] → D. Then the dot-product can be bounded as follows:

Lemma 18. If each coefficient of the u i and v i are between 0 and 2 p -1, then the coefficients of S = n i=1 (u i v i ) are bounded by 2 n(2p+1) in absolute value.

Proof. For all u, v, the coefficients of (u v) are between 0 and

Then, by induction, when aggregating k of those with , the absolute values of the coefficients remain less than 2 k(2p+1) -1.

Therefore, with N an 2048 bits modulus and n ≤ 4 in the ESDP protocols of Algorithm 11, Lemma 18 allows a precision close to 2 -255 ≈ 10 -77 .

In conclusion, we provide an efficient and secure protocol DSDP n to securely compute dot products (against semi-honest adversary) in the MPC model, with unsual data division between n players. It can be used to perform a private matrix multiplication and also be adapted to securely compute trust aggregation between players.


STUDY OF SURFICIAL WEATHERING PROFILES USING HELICOPTER BORNE TRANSIENT ELECTROMAGNETIC SURVEYS:

A

Mots clés : Cartographie géologique, régolithe, TDEM, profils d'altération

ABSTRACT

In weathered volcanic tropical islands, geological studies are often limited due to the generally poorly outcropping conditions. Ground geophysical campaigns are also hard to perform due to difficult access in densely populated and forested areas. Recognition of geometric and petrographic characteristics of weathering mantles is a prerequisite to provide sustainable solutions to the management of natural hazards. In this particular context, airborne TDEM appears as a promising method to provide precise information about the Regolith. In 2010, the BRGM (the French geological survey) and the Prefecture of Mayotte decided to fund a geological mapping project including a heliborne TDEM resistivity survey of Mayotte. The SkyTEM helicopter borne transient electromagnetic method has been chosen in order to obtain a quasi-3D resistivity map of the island. Good conductivity contrasts (from 1 to 600 ohm.m) between the different rock types allow defining the geometry of the principal geological units, up to a depth of 200 m. Preliminary results are very promising and have shown that TDEM is a powerful tool for regolith mapping and surficial weathering profile characterization.

Key words: Geological mapping,regolith,TDEM, weathering profiles .1 INTRODUCTION

In volcanic weathered tropical islands, geological studies are often limited due to the generally poorly outcropping conditions. Ground geophysical campaigns are also hard to perform due to the difficult access in densely populated and densely forested areas. Recognition of geometric and petrographic characteristics of weathering mantles is a prerequisite to provide sustainable solutions to the management of natural hazards. In this particular context, Airborne Time Domain Electromagnetic Method (TDEM) appears as the most suitable method to provide precise information about the regolith. In Mayotte (French volcanic island located in the northern Mozambique Channel in the Indian Ocean) much of the regolith formations are residual and consist of intensely weathered basalts and phonolites. Weathering profiles are generally thick (greater than 10 meters). Saprolites in place can have a strong cohesion but torrential rainfall can brutally decrease the resistance and producte large landslides at the limit between alloterites and saprolites.

.2 MATERIALS AND METHODS

In 2010, BRGM (the French geological survey) and the Prefecture of Mayotte decided to fund a geological mapping project including heliborne TDEM resistivity survey of the island. The SkyTEM helicopter borne transient electromagnetic method has been performed in October 2010 in order to obtain a quasi-3D resistivity map of the island. Average helicopter flying speed was 65 km/h and the flight altitude of the transmitter frame and receiver coil was 40 m. Flight lines were oriented North-South with an average spacing of 200 m and 3000 km have been covered. Good conductivity contrasts (from 1 to 600 ohm.m) between the different rocks types allow to define the geometry of the principal geological units, up to 200 m depth. This work is focused on the correlation between weathering profile and resistivity.

.3 RESULTS

Figure 1 focuses this analysis on the weathering profile. Fresh lavas have a resistivity generally lower than 250 .m. The saprolite shows a resistivity between 10 and 90 .m with a maximal frequency at 40 .m. The alloterite, shows higher resistivity (50 to 250 .m) with a maximal frequency at 100 .m. -Alloterite between 0 to 5 meters; -Laminated with preserved features saprolite between 5 to 60 meters; -Fissured lavas between 60 to 85 meters; -Fresh lavas between 85 to 120 meters of depth Preliminary results are very promising and TDEM seems to be a useful tool to provide informations which can assist in regolith mapping and characterisation of surficial weathering profiles. Correlation between TDEM resistivity and regolith horizons are often good. Alloterites have higher resistivity values than the saprolites. On the contrary, we observe a decrease of resistivity of fresh primary rocks with weathering (i.e. fissured lavas).

Fig. 1 -

 1 Fig. 1-Resistivity histogram for each geological formation Figure 2 shows the evolution of resistivity versus depth where alloterite has been mapped in the subsurface. The resistivity of the first five meters is high (~ 110 .m) and decreases quickly between 5 et 20 m to reach a value of 20 .m. Between 20 to 60 meters, the resistivity value decreases slowly to 15 .m. Between 60 and 85 m, the resistivity increases and a constant value of 25 .m is encountered at a depth of 120 m..

Fig. 2 -

 2 Fig.2-Toward a 2D resistivity characterization of the weathering profile

CASE STUDY IN MAYOTTE VOLCANIC ISLAND.

  Dans les îles tropicales volcaniques, des études géologiques sont souvent limitées en raison des mauvaises conditions d'affleurement. Les campagnes de géophysique au sol sont difficiles à mettre en oeuvre compte tenu des difficultés d'accès dans des zones densément peuplées et boisées. La reconnaissance et la caractérisation géométriques et pétrographiques des manteaux d'altérites est un prérequis pour répondre aux demandes concernant, par exemple, la gestion des risques naturels. Dans ce contexte particulier, acquérir des données TDEM aéroportées apparaît comme la méthode la plus appropriée pour fournir des informations précises sur le régolithe. En 2010, le BRGM et la préfecture de Mayotte ont décidé de financer un projet de cartographie géologique, incluant un levé de résistivité TDEM héliporté sur l'ensemble de Mayotte.

	CAROLINE	RICORDEL-PROGNON 1 .,	JACQUES	DEPARIS 1 .,
	FREDERIC LACQUEMENT 1 ., NEHLIG PIERRE 1 ., BERNARD JULIEN 1
	BRGM -3, avenue Claude-Guillemin, BP 36009 -45060 Orléans cedex 2 -
	France
	RÉSUMÉ
				La méthode
	électromagnétique a été choisie afin d'obtenir une image de la résistivité quasi-
	3D de l'île. De bons contrastes de conductivité (de 1 à 600 ohm.m) entre les
	différents types de roches ont permis de définir la géométrie des principales
	unités géologiques, jusqu'à une profondeur de 200 m. Les premiers résultats sont
	très prometteurs et ont montré qu'il s'agit d'un outil puissant pour la
	cartographie de régolithe et en particulier la cartographie des profils
	d'altération.