Sanitizable signatures authorize semi-trusted sanitizers to modify admissible blocks of a signed message. Most works consider only one sanitizer while those considering multiple sanitizers are limited by their capacity to manage admissible blocks which must be the same for all of them. We study the case where different sanitizers with different roles can be trusted to modify different blocks of the message. We define a model for multi-sanitizer sanitizable signatures which allow managing authorization for each sanitizer independently. We also provide formal definitions of its security properties. We propose two secure generic constructions FSV-k-SAN and IUT-k-SAN with different security properties. We implement both constructions and evaluate their performance on a server and a smartphone.

EDHOC is a lightweight authenticated key exchange protocol designed for constrained IoT devices. It currently supports asymmetric authentication, either using digital signatures or static Diffie-Hellman (DH) keys. Since many IoT deployments rely on Pre-Shared Keys (PSK) for authentication, a new PSK-based authentication method (EDHOC-PSK) is currently under standardization. This paper presents a symbolic analysis EDHOC-PSK (draft version 06) using SAPIC+, which compiles a single formal specification into multiple state-of-the-art verification tools, including Tamarin and ProVerif. Our model extends the typical Dolev-Yao (DY) adversary with additional capabilities, including leakage of ephemeral secrets, leakage of the long-term Pre-Shared Key leakage of the session key and a discrete-logarithm oracle. We verify the confidentiality, authentication, and key-agreement properties stated in the draft, and we refine the specification of identity protection by distinguishing anonymity and unlinkability. We show that EDHOC-PSK achieves anonymity for both parties against active attackers, while unlinkability holds only for the Initiator under passive attackers. Finally, we analyze a post-quantum Store-Now-Decrypt-Later (SNDL) adversary and find that all proven properties remain intact except Perfect Forward Secrecy (PFS), which cannot be preserved once DH secrets are recoverable.

We address the perpetual grid exploration (PGE) by a swarm of autonomous, asynchronous, myopic, and luminous robots. We first show that it is impossible for the robots to explore the grid regardless of their number and the number of colors they can take if their visibility range is one. We also show that PGE is impossible with three oblivious robots that have a visibility range of two hops. We then present three optimal algorithms solving the problem. The first algorithm uses four oblivious robots with a visibility range of two, but assumes they agree on a common chirality. For the two other algorithms, no common chirality is assumed. The former uses three robots that have a visibility range of two and a two-color light. The latter uses three oblivious robots under visibility range three.

International audience

Biometric systems are widely used for authentication and identification. The False Match Rate (FMR) quantifies the probability of matching a biometric template to a non-corresponding template and serves as an indicator of the system robustness against security threats. We analyze biometric systems through two main contributions. First, we study untargeted attacks, where an adversary aims to impersonate any user in the database. We compute the number of trials needed for a successful impersonation and derive the critical population size ( i.e., the maximum database size) and critical (FMR) required to maintain security against untargeted attacks as the database grows. Second, we address the biometric birthday problem, which quantifies the probability that there exists two distinct users that collide ( i.e., can impersonate each other). We compute approximate and exact probabilities of collision and derive the associated critical population size and critical (FMR) to bound the risk of biometric collisions, particularly in large-scale databases. These thresholds provide actionable insights for designing biometric systems that mitigate the risks of impersonation and biometric collisions, particularly in large-scale databases. Nevertheless, our findings show that current systems fail to meet the required security level against untargeted attacks, even in small databases, and face significant challenges with the biometric birthday problem as databases grow.

In this paper, we consider the exploration of an infinite grid by a swarm of fully-synchronous robots with weak capabilities: they are disoriented, opaque, do not communicate explicitely, have limited visibility, and cannot occupy the same position at the same time. Our first result shows that, in this context, minimizing the visibility range and the number of used colors are two orthogonal issues: it is impossible to design a solution to our exploration problem that is optimal w.r.t. both parameters simultaneously. Consequently, we address optimality of these two criteria separately by proposing two algorithms; the former being optimal in terms of visibility range, the latter being optimal in terms of number of used colors. More precisely, the first algorithm solves the problem using eight oblivious robots under visibility range two (this visibility being optimal when considering oblivious robots), and the second algorithm solves the problem under visibility range one using six robots and two colors (which is optimal under this visibility range). Finally, we also tackle the optimality in terms of number of robots. According to the lower bound given in Bramas et al. (2020), we propose an algorithm working with a minimum number of robots (five) under visibility range one. This latter uses twelve colors and also guarantees that nodes are visited infinitely often. • The infinite grid exclusive exploration by synchronous oblivious robots is impossible under visibility range one whatever by their number. • The infinite grid exclusive exploration can be achieved by eight synchronous oblivious robots under the optimal visibility range two. • The infinite grid exclusive exploration can be achieved by six synchronous robots under visibility range one using only two colors. • The infinite grid exclusive exploration can be achieved by only five synchronous robots under visibility range one, yet using twelve colors.

Digital ticketing systems typically offer ticket purchase, refund, validation, and, optionally, anonymity of users. However, it would be interesting for users to transfer their tickets, as is currently done with physical tickets. We propose Applause, a ticketing system allowing the purchase, refund, validation, and transfer of tickets based on trusted authority, while guaranteeing the anonymity of users, as long as the used payment method provides anonymity. To study its security, we formalise the security of the transferable E-Ticket scheme in the game-based paradigm. We prove the security of Applause computationally in the standard model and symbolically using the protocol verifier ProVerif. Applause relies on standard cryptographic primitives, rendering our construction efficient and scalable, as shown by a proof-of-concept. In order to obtain Spotlight, an auditable version, proved to be secure, users will remain anonymous except for a trusted third party, which will be able to disclose their identity in the event of a disaster.

International audience

We tackle the problem of secure cumulative reward maximization in multi-armed bandits in a cross-silo federated learning setting. Under the orchestration of a central server, each data owner participating at the cumulative reward computation has the guarantee that its raw data is not seen by some other participant. We rely on cryptographic schemes and propose SAMBA, a generic framework for Secure federAted Multi-armed BAndits. We show that SAMBA returns the same cumulative reward as the non-secure versions of bandit algorithms, while satisfying formally proven security properties. We also show that the overhead due to cryptographic primitives is linear in the size of the input, which is confirmed by our implementation.

Blockchain is a type of distributed ledger.A wide range of consensus algorithms exists to reach consensus in a decentralized manner.However, most of them trade energy consumption for a degree of openness.Blockchains are primarily used for tokens and cryptocurrencies.Often the process of minting new tokens depends on actionable real world behaviors.A difficulty persists in securely translating said behavior into a decentralized blockchain.We formalize the generic concept of Proof of Behavior (PoB), and use it to create a consensus mechanism for generic permissionless blockchains.

We consider the problem of cumulative reward maximization in multi-armed bandits. We address the security concerns that occur when data and computations are outsourced to an honest-but-curious cloud i.e., that executes tasks dutifully, but tries to gain as much information as possible. We consider situations where data used in bandit algorithms is sensitive and has to be protected e.g., commercial or personal data. We rely on cryptographic schemes and propose [Formula: see text], a secure multi-party protocol based on the UCB algorithm. We prove that [Formula: see text] computes the same cumulative reward as UCB while satisfying desirable security properties. In particular, cloud nodes cannot learn the cumulative reward or the sum of rewards for more than one arm. Moreover, by analyzing messages exchanged among cloud nodes, an external observer cannot learn the cumulative reward or the sum of rewards produced by some arm. We show that the overhead due to cryptographic primitives is linear in the size of the input. Our implementation confirms the linear-time behavior and the practical feasibility of our protocol, on both synthetic and real-world data.

A Proof-of-Location (POL) system is used to issue a proof-of-location token ($pol$) to a user who has been present at a location$\ell oc$, such that it can be later presented to a verifier to assure the presence of the user at$\ell oc$. Basic POL security requirements areunforgeabilityof$pol$, and itsnon-transferability(a$pol$issued to user$u_1$cannot be used by$u_2$). An additional important property of POL systems isuser privacyagainst the issuers and verifiers. We make two contributions. First, we formalize the POL security and privacy properties, and construct the first system providing provable security and privacy against the issuer and the verifier, both. Second, we introduce ageo-tampering attackthat completely breaks POL system security, by simply changing the location of a$pol$issuing node. The attack applies to portable infrastructure nodes that are not continually monitored. We propose an algorithm that is used by a$pol$issuer to provide a location integrity “proof”, that will be embedded in a$pol$to protect against this attack. The proof relies on a novel application of euclidean Distance Matrices. We implemented our POL on an off-the-shelf Android smartphone to show the practicality of the proposed algorithms.

The stochastic multi-armed bandit is a classical reinforcement learning model, where a learning agent sequentially chooses an action (pull a bandit arm) and the environment responds with a stochastic reward drawn from an unknown distribution associated with the chosen action. A popular objective for the agent is to identify the arm having the maximum expected reward, also known as the best arm identification problem. We address the security concerns that occur in a cross-silo federated learning setting, where multiple data owners collaborate under the orchestration of a server to execute a best arm identification algorithm. We propose three secure protocols, which guarantee desirable security properties for the: input data (i.e., reward values), intermediate data (i.e., sums of rewards), and output data (i.e., ranking of arms and in particular the identified best arm). More precisely: (1) no data owner can learn the identified best arm; moreover, no data owner can learn local data pertaining to another data owner; (2) the orchestration participants cannot learn the identified best arm, any reward value, or any sum of rewards; (3) by analyzing the messages exchanged over the network, an external observer cannot learn the identified best arm, or any reward value, or any sum of rewards. Each protocol has a different architecture, uses different techniques, and proposes a different trade-off with respect to several criteria that we thoroughly analyze: number of participants, generality of the supported reward functions, cryptographic overhead, and communication cost. To build our protocols, we rely on secure multi-party computation, AES-CBC, and the additive homomorphic property of Paillier.

International audience

The federated learning paradigm allows several data owners to contribute to a machine learning task without exposing their potentially sensitive data. We focus on cumulative reward maximization in Multi-Armed Bandits (MAB), a classical reinforcement learning model for decision making under uncertainty. We demonstrate Samba, a generic framework for Secure federAted Multi-armed BAndits. The demonstration platform is a Web interface that simulates the distributed components of Samba, and which helps the data scientist to configure the end-to-end workflow of deploying a federated MAB algorithm. The user-friendly interface of Samba, allows the users to examine the interaction between three key dimensions of federated MAB: cumulative reward, computation time, and security guarantees. We demonstrate Samba with two real-world datasets: Google Local Reviews and Steam Video Game.

Cancelable biometric schemes aim at generating secure biometric templates by combining user specific tokens, such as password, stored secret or salt, along with biometric data. This type of transformation is constructed as a composition of a biometric transformation with a feature extraction algorithm. The security requirements of cancelable biometric schemes concern the irreversibility, unlinkability and revocability of templates, without losing in accuracy of comparison. While several schemes were recently attacked regarding these requirements, full reversibility of such a composition in order to produce colliding biometric characteristics, and specifically presentation attacks, were never demonstrated to the best of our knowledge. In this paper, we formalize these attacks for a traditional cancelable scheme with the help of integer linear programming (ILP) and quadratically constrained quadratic programming (QCQP). Solving these optimization problems allows an adversary to slightly alter its fingerprint image in order to impersonate any individual. Moreover, in an even more severe scenario, it is possible to simultaneously impersonate several individuals.

Biometric recognition encompasses two operating modes. The first one is biometric identification which consists in determining the identity of an individual based on her biometrics and requires browsing the entire database (i.e., a 1:N search). The other one is biometric authentication which corresponds to verifying claimed biometrics of an individual (i.e., a 1:1 search) to authenticate her, or grant her access to some services. The matching process is based on the similarities between a fresh and an enrolled biometric template. Considering the case of binary templates, we investigate how a highly populated database yields near-collisions, impacting the security of both the operating modes. Insight into the security of binary templates is given by establishing a lower bound on the size of templates and an upper bound on the size of a template database depending on security parameters. We provide efficient algorithms for partitioning a leaked template database in order to improve the generation of a master-template-set that can impersonates any enrolled user and possibly some future users. Practical impacts of proposed algorithms are finally emphasized with experimental studies.

Suguru is a paper and pencil puzzle invented by Naoki Inaba. The goal of the game is to fill a grid with numbers between 1 and 5 while respecting three simple constraints. We first prove the NP-completeness of Suguru puzzle. For this we design gadgets to encode the PLANAR-CIRCUIT-SAT in a Suguru grid. We then design a physical Zero-Knowledge Proof (ZKP) protocol for Suguru. This ZKP protocol allows a prover to prove that he knows a solution of a Suguru grid to a verifier without leaking any information on the solution. To construct such a physical ZKP protocol, we only rely on a few physical cards and adapted encoding. For a Suguru grid with n cells, we only use 5n+5 cards. Moreover, we prove the three classical security properties of a ZKP: completeness, extractability, and zero-knowledge.

The multi-armed bandit is a reinforcement learning model where a learning agent repeatedly chooses an action (pull a bandit arm) and the environment responds with a stochastic outcome (reward) coming from an unknown distribution associated with the chosen arm. Bandits have a wide-range of application such as Web recommendation systems. We address the cumulative reward maximization problem in a secure federated learning setting, where multiple data owners keep their data stored locally and collaborate under the coordination of a central orchestration server. We rely on cryptographic schemes and propose Samba, a generic framework for Secure federAted Multi-armed BAndits. Each data owner has data associated to a bandit arm and the bandit algorithm has to sequentially select which data owner is solicited at each time step. We instantiate Samba for five bandit algorithms. We show that Samba returns the same cumulative reward as the nonsecure versions of bandit algorithms, while satisfying formally proven security properties. We also show that the overhead due to cryptographic primitives is linear in the size of the input, which is confirmed by our proof-of-concept implementation.

In 1968, Liu described the problem of securing documents in a shared secret project. In an example, at least six out of eleven participating scientists need to be present to open the lock securing the secret documents. Shamir proposed a mathematical solution to this physical problem in 1979, by designing an efficient k-out-of- n secret sharing scheme based on Lagrange’s interpolation. Liu and Shamir also claimed that the minimal solution using physical locks is clearly impractical and exponential in the number of participants. In this paper we relax some implicit assumptions in their claim and propose an optimal physical solution to the problem of Liu that uses physical padlocks, but the number of padlocks is not greater than the number of participants. Then, we show that no device can do better for k-out-of- n threshold padlock systems as soon as [Formula: see text], which holds true in particular for Liu’s example. More generally, we derive bounds required to implement any threshold system and prove a lower bound of [Formula: see text] padlocks for any threshold larger than 2. For instance we propose an optimal scheme reaching that bound for 2-out-of- n threshold systems and requiring less than [Formula: see text] padlocks. We also discuss more complex access structures, a wrapping technique, and other sublinear realizations like an algorithm to generate 3-out-of- n systems with [Formula: see text] padlocks. Finally we give an algorithm building k-out-of- n threshold padlock systems with only [Formula: see text] padlocks. Apart from the physical world, our results also show that it is possible to implement secret sharing over small fields.

This paper describes the heuristics used by the Shadoks team for the CG:SHOP 2021 challenge on motion planning. Using the heuristics outlined in this paper, our team won first place with the best solution to 202 out of 203 instances and optimal solutions to at least 105 of them.

In relay attacks, a man-in-the-middle adversary impersonates a legitimate party and makes it this party appear to be of an authenticator, when in fact they are not. In order to counteract relay attacks, distance-bounding protocols provide a means for a verifier (e.g., an payment terminal) to estimate his relative distance to a prover (e.g., a bankcard). We propose FlexiDB, a new cryptographic model for distance bounding, parameterised by different types of fine-grained corruptions. FlexiDB allows to consider classical cases but also new, generalised corruption settings. In these settings, we exhibit new attack strategies on existing protocols. Finally, we propose a proof-of-concept mechanisation of FlexiDB in the interactive cryptographic prover EasyCrypt. We use this to exhibit a flavour of man-in-the-middle security on a variant of MasterCard's contactless-payment protocol.

International audience

Summary One of the most critical properties that must be ensured to have a secure electronic voting is verifiability. Political parties, observers, and especially voters want to be able to verify that all eligible votes are cast as intended and counted as cast without compromising votes secrecy or voters privacy. Over the past few decades, an important number of e‐voting protocols attempt to deal with this issue by using cryptographic techniques and/or a public bulletin board. Recently, some blockchain‐based e‐voting systems have been proposed, but were not found practical in the real world, because they do not support situations with large numbers of candidates and voters. In this article, we design and implement a verifiable blockchain‐based online voting protocol, called verify‐your‐vote . Our protocol ensures several security properties thanks to some cryptographic primitives and blockchain technology. We also evaluate its performance in terms of time, cost, and the number of voters and candidates that can be supported.

We propose a technique to construct physical Zero-Knowledge Proof (ZKP) protocols for puzzles that require a single loop draw feature. Our approach is based on the observation that a loop has only one hole and this property remains stable by some simple transformations. Using this trick, we can transform a simple big loop, which is visible to anyone, into the solution loop by using transformations that do not disclose any information about the solution. We illustrate our technique by applying it to construct physical ZKP protocols for two Nikoli puzzles: Slitherlink and Masyu.

This exploratory paper intends to drive preliminary insights on the different mental models accountants and blockchain developers have on the implementation of blockchain for accounting. Based on the question of whether blockchain applications for accounting could be revolutionary, this paper employs a ground theory methodology based on semi-structured interviews and concept analysis to highlight the different approaches to transparency and trust between the selected groups, the challenges of blockchain and the potential effects of this technology in accounting. Although deeper studies are needed, the conclusions highlight the socio-technical nature of accounting; the relevance and changes of the concepts of trust and transparency when marrying both disciplines; and the real relevance of this technology for the processes of auditing and accounting.

We consider the problem of cumulative reward maximization in multi-armed bandits. We address the security concerns that occur when data and computations are outsourced to an honest-but-curious cloud i.e., that executes tasks dutifully, but tries to gain as much information as possible. We consider situations where data used in bandit algorithms is sensitive and has to be protected e.g., commercial or personal data. We rely on cryptographic schemes and propose UCB-DS, a distributed and secure protocol based on the UCB algorithm. We prove that UCB-DS computes the same cumulative reward as UCB while satisfying desirable security properties. In particular, cloud nodes cannot learn the cumulative reward or the sum of rewards for more than one arm. Moreover, by analyzing messages exchanged among cloud nodes, an external observer cannot learn the cumulative reward or the sum of rewards produced by some arm. We show that the overhead due to cryptographic primitives is linear in the size of the input. Our implementation confirms the linear-time behavior and the practical feasibility of our protocol, on both synthetic and real-world data.

Touch screens have become ubiquitous in the past few years, like for instance in smartphones and tablets. These devices are often the entry door to numerous information systems, hence having a secure and practical authentication mechanism is crucial. In this paper, we examine the complexity of different authentication methods specifically designed for such devices. We study the widely spread technology to authenticate a user using a Personal Identifier Number code (PIN code). Entering the code is a critical moment where there are several possibilities for an attacker to discover the secret. We consider the three attack models: a Bruteforce Attack (BA) model, a Smudge Attack (SA) model, and an Observation Attack (OA) model where the attacker sees the user logging in on his device. The aim of the intruder is to learn the secret code. Our goal is to propose alternative methods to enter a PIN code. We compare such different methods in terms of security. Some methods require more intentional resources than other, this is why we performed a psychological study on the different methods to evaluate the users' perception of the different methods and their usage.

The MapReduce programming paradigm allows to process big data sets in parallel on a large cluster of commodity machines. The MapReduce users often outsource their data and computations to a public cloud provider. We focus on the fundamental problem of matrix multiplication, and address the inherent security and privacy concerns that occur when outsourcing to a public cloud. Our goal is to enhance the two state-of-the-art algorithms for MapReduce matrix multiplication with privacy guarantees such as: none of the nodes storing an input matrix can learn the other input matrix or the output matrix, and moreover, none of the nodes computing an intermediate result can learn the input or the output matrices. To achieve our goal, we rely on the well-known Paillier's cryptosystem and we use its partially homomorphic property to develop efficient algorithms that satisfy our problem statement. We develop two different approaches called Secure-Private (SP) and Collision-Resistant-Secure-Private (CRSP), and compare their trade-offs with respect to three fundamental criteria: computation cost, communication cost, and privacy guarantees. Finally, we give security proofs of our protocols.

Distance-bounding protocols have been introduced to thwart relay attacks against contactless authentication protocols. In this context, verifiers have to authenticate the credentials of untrusted provers. Unfortunately, these protocols are themselves subject to complex threats such as terrorist-fraud attacks, in which a malicious prover helps an accomplice to authenticate. Provably guaranteeing the resistance of distance-bounding protocols to these attacks is complex. The classical solutions assume that rational provers want to protect their long-term authentication credentials, even with respect to their accomplices. Thus, terrorist-fraud resistant protocols generally rely on artificial extraction mechanisms, ensuring that an accomplice can retrieve the credential of his partnering prover, if he is able to authenticate. We propose a novel approach to obtain provable terrorist-fraud resistant protocols that does not rely on an accomplice being able to extract any long-term key. Instead, we simply assume that he can replay the information received from the prover. Thus, rational provers should refuse to cooperate with third parties if they can impersonate them freely afterwards. We introduce a generic construction for provably secure distance-bounding protocols, and give three instances of this construction: (1) an efficient symmetric-key protocol, (2) a public-key protocol protecting the identities of provers against external eavesdroppers, and finally (3) a fully anonymous protocol protecting the identities of provers even against malicious verifiers that try to profile them.

Accountability plays a key role in dependable distributed systems. It allows to detect, isolate and churn malicious/selfish nodes that deviate from a prescribed protocol. To achieve these properties, several accountable systems use at their core cryptographic primitives that produce non-repudiable evidence of inconsistent or incorrect behavior.

International audience

International audience

International audience

International audience

HB+ is a lightweight authentication scheme, which is secure against passive attacks if the Learning Parity with Noise Problem (LPN) is hard. However, HB+ is vulnerable to a key-recovery, man-in-the-middle (MiM) attack dubbed GRS. The HB+DB protocol added a distance-bounding dimension to HB+, and was experimentally proven to resist the GRS attack.

Ring and group signatures allow their members to anonymously sign documents in the name of the group. In ring signatures, members manage the group themselves in an ad-hoc manner while in group signatures, a manager is required. Moreover, k-times traceable group and ring signatures [1] allow anyone to publicly trace two signatures from a same user if he exceeds the a priori authorized number of signatures. In [2], Canard et al. give a 1-time traceable ring signature where each member can only generate one anonymous signature. Hence, it is possible to trace any two signatures from the same user. Some other works generalize it to the k-times case, but the traceability only concerns two signatures. In this paper, we define the notion of k-times full traceable ring signature (k-FTRS) such that all signatures produced by the same user are traceable if and only if he produces more than k signatures. We construct a k-FTRS called Ktrace. We extend existing formal security models of k-times linkable signatures to prove the security of Ktrace in the random oracle model. Our primitive k-FTRS can be used to construct a k-times veto scheme or a proxy e-voting scheme that prevents denial-of-service caused by cheating users.

International audience

International audience

Contactless communications have become omnipresent in our daily lives, from simple access cards to electronic passports. Such systems are particularly vulnerable to relay attacks, in which an adversary relays the messages from a prover to a verifier. Distance-bounding protocols were introduced to counter such attacks. Lately, there has been a very active research trend on improving the security of these protocols, but also on ensuring strong privacy properties with respect to active adversaries and malicious verifiers.

International audience

Auctions have a long history, having been recorded as early as 500 B.C. [Auction Theory, Academic Press, San Diego, USA, 2002]. Nowadays, electronic auctions have been a great success and are increasingly used in various applications, including high performance computing [Concurrency and Computatio n: Practice and Experience 14(13–15) (2002), 1507–1542]. Many cryptographic protocols have been proposed to address the various security requirements of these electronic transactions, in particular to ensure privacy. Brandt [International Journal of Information Security 5 (2006), 201–216] developed a protocol that computes the winner using homomorphic operations on a distributed ElGamal encryption of the bids. He claimed that it ensures full privacy of the bidders, i.e. no information apart from the winner and the winning price is leaked. We first show that this protocol – when using malleable interactive zero-knowledge proofs – is vulnerable to attacks by dishonest bidders. Such bidders can manipulate the publicly available data in a way that allows the seller to deduce all participants’ bids. We provide an efficient parallelized implementation of the protocol and the attack to show its practicality. Additionally we discuss some issues with verifiability as well as attacks on non-repudiation, fairness and the privacy of individual bidders exploiting authentication problems.

Cryptographic accumulators are space/time efficient data structures used to verify if a value belongs to a set. They have found many applications in networking and distributed systems since their introduction by Benaloh and de Mare in 1993. Despite this popularity, there is currently no thorough performance evaluation of the different existing designs. Symmetric and asymmetric accumulators are used likewise without any particular argument to support either of the design. We aim to establish the speed of each design and their application's domains in terms of their size and the size of the values.

Once a secure mechanism for authenticated communication is deployed in a Wireless Sensor Network (WSN), several situations may arise: a node can leave the network, a new node can join the network, an intruder could try to join the network or capture a node. Therefore it is important to revoke and renew certain keys that are learned by a malicious node. We propose several secure WSN protocols for revocations and renewal of cryptographic keys in the network based on symmetric encryption and elliptic curve cryptography (ECC). For all our solutions, we provide a formal analysis of the security of our protocols using Scyther, an automatic verification tool for cryptographic protocols. All the proposed protocols are proven secure but have different security levels by using different types of keys. Finally we implemented all our protocols on real testbeds using TelosB motes and compared their efficiency.

International audience

An electronic auction protocol will only be used by those who trust that it operates correctly. Therefore, e-auction protocols must be verifiable: seller, buyer and losing bidders must all be able to determine that the result was correct. We pose that the importance of verifiability for e-auctions necessitates a formal analysis. Consequently, we identify notions of verifiability for each stakeholder. We formalize these and then use the developed framework to study the verifiability of two examples, the protocols due to Curtis et al. and Brandt, identifying several issues.

We propose SR3, a secure and resilient algorithm for convergecast routing in WSNs. SR3 uses lightweight cryptographic primitives to achieve data confidentiality and data packet unforgeability. SR3 has a security proven by formal tool. We made simulations to show the resiliency of SR3 against various scenarios, where we mixed selective forwarding, blackhole, wormhole, and Sybil attacks. We compared our solution to several routing algorithms of the literature. Our results show that the resiliency accomplished by SR3 is drastically better than the one achieved by those protocols, especially when the network is sparse. Moreover, unlike previous solutions, SR3 self-adapts after compromised nodes suddenly change their behavior.

Privacy is one of the main issues in electronic voting. We propose a family of symbolic privacy notions that allows to assess the level of privacy ensured by a voting protocol. Our definitions are applicable to protocols featuring multiple votes per voter and special attack scenarios such as vote-copying or forced abstention. Finally we employ our definitions on several existing voting protocols to show that our model allows to compare different types of protocols based on different techniques, and is suitable for automated verification using existing tools.

Chosen-ciphertext security is by now a standard security property for asymmetric encryption. Many generic constructions for building secure cryptosystems from primitives with lower level of security have been proposed. Providing security proofs has also become standard practice. There is, however, a lack of automated verification procedures that analyze such cryptosystems and provide security proofs. This paper presents an automated procedure for analyzing generic asymmetric encryption schemes in the random oracle model. It has been applied to several examples of encryption schemes among which the construction of Bellare-Rogaway 1993, of Pointcheval at PKC'2000 and REACT.

Cryptographic protocols are successfully analyzed using formal methods. However, formal approaches usually consider the encryption schemes as black boxes and assume that an adversary cannot learn anything from an encrypted message except if he has the key. Such an assumption is too strong in general since some attacks exploit in a clever way the interaction between protocol rules and properties of cryptographic operators. Moreover, the executability of some protocols relies explicitly on some algebraic properties of cryptographic primitives such as commutative encryption. We give a list of some relevant algebraic properties of cryptographic operators, and for each of them, we provide examples of protocols or attacks using these properties. We also give an overview of the existing methods in formal approaches for analyzing cryptographic protocols.