Author: "Pascal Lafourcade" - Searchworks@Jio Institute Digital Library Search Results

Your search keyword '"Pascal Lafourcade"' showing total 422 results

Start Over Author "Pascal Lafourcade"

422 results on '"Pascal Lafourcade"'

251. Formal analysis of a private access control protocol to a cloud storage

Author: Mouhebeddine Berrima, Matthieu Giraud, Pascal Lafourcade, Narjes Ben Rajeb, Université de Monastir - University of Monastir (UM), Laboratoire d'Informatique, de Modélisation et d'Optimisation des Systèmes (LIMOS), Ecole Nationale Supérieure des Mines de St Etienne-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])-Centre National de la Recherche Scientifique (CNRS), Laboratoire d'Informatique, de Parallélisme et de Productique (LIP2), Faculté des Sciences Mathématiques, Physiques et Naturelles de Tunis (FST), Université de Tunis El Manar (UTM)-Université de Tunis El Manar (UTM), ANR-16-IDEX-0001,CAP 20-25,CAP 20-25 (I-Site)(2016), Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])-Centre National de la Recherche Scientifique (CNRS), ANR-16-IDEX-0001,CAP 20-25,CAP 20-25(2016), and Ecole Nationale Supérieure des Mines de St Etienne-Centre National de la Recherche Scientifique (CNRS)-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])
Subjects: Authentication, Cloud storage, Cryptographic primitive, formal methods, Computer science, business.industry, Data security, Cloud computing, Cryptographic protocol, Computer security, computer.software_genre, Encryption, data and user privacy, attribute based signature, Theoretical Computer Science, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Hardware and Architecture, attribute based encryption, Attribute-based encryption, business, computer, Software
Abstract: International audience; Cloud storage provides an attractive solution for many organizations and enterprises due to its features such as scalability, availability and reduced costs. However, storing data in the cloud is challenging if we want to ensure data security and user privacy. To address these security issues cryptographic protocols are usually used. Such protocols rely on cryptographic primitives which have to guarantee some security properties such that data and user privacy or authentication. Attribute-Based Signature (ABS) and Attribute-Based Encryption (ABE) are very adapted for storing data on an untrusted remote entity. In this work, we enhance the security of cloud storage systems through a formal analysis of a cloud storage protocol based on ABS and ABE schemes. We clarify several ambiguities in the design of this protocol and model the protocol and its security properties with ProVerif an automatic tool for the verification of cryptographic protocols. We discover an unknown attack against user privacy in the Ruj et al. protocol. We propose a correction, and automatically prove the security of the corrected protocol with ProVerif.
Published: 2018
Full Text: View/download PDF

252. Verify-Your-Vote: A Verifiable Blockchain-based Online Voting Protocol

Author: Souheib Yousfi, Marwa Chaieb, Riadh Robbana, Pascal Lafourcade, Lafourcade, Pascal, Laboratoire d'Informatique, de Modélisation et d'Optimisation des Systèmes (LIMOS), Ecole Nationale Supérieure des Mines de St Etienne-Centre National de la Recherche Scientifique (CNRS)-Université Clermont Auvergne [2017-2020] (UCA [2017-2020]), Institut National des Sciences Appliquées et de Technologie - Carthage (INSAT Carthage), and Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])-Centre National de la Recherche Scientifique (CNRS)
Subjects: Electronic voting, Computer science, Cryptography, 0102 computer and information sciences, 02 engineering and technology, Computer security, computer.software_genre, Encryption, 01 natural sciences, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Blockchain, 020204 information systems, 0202 electrical engineering, electronic engineering, information engineering, ProVerif, Elliptic curve cryptography, Protocol (object-oriented programming), [INFO.INFO-CR] Computer Science [cs]/Cryptography and Security [cs.CR], Authentication, Cryptographic primitive, Elliptic Curve Cryptography, business.industry, Online e-voting, 010201 computation theory & mathematics, Verifiable secret sharing, Verifiability, business, computer
Abstract: International audience; Blockchain provides the possibility to design new types of applications and systems that allow their users to store data in a secure and transparent way. In this paper, we design a fully verifiable online electronic voting protocol using a blockchain. Our e-voting protocol, called VYV for Verify-Your-Vote, involves cryptographic primitives based on Elliptic-Curve Cryptography (ECC), pairings and Identity Based Encryption (IBE). It ensures the following privacy and security properties: only eligible voter can vote, authentication of the voter, vote privacy, receipt-freeness, fairness, individual and universal verifiability. Furthermore , we formally prove the security of our protocol, using ProVerif tool.
Published: 2018

253. Revisiting AES Related-Key Differential Attacks with Constraint Programming

Author: Pascal Lafourcade, David Gerault, Christine Solnon, Marine Minier, Laboratoire d'Informatique, de Modélisation et d'Optimisation des Systèmes (LIMOS), Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])-Centre National de la Recherche Scientifique (CNRS), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Cryptology, arithmetic : algebraic methods for better algorithms (CARAMBA), Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Algorithms, Computation, Image and Geometry (LORIA - ALGO), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Geometry Processing and Constrained Optimization (M2DisCo), Laboratoire d'InfoRmatique en Image et Systèmes d'information (LIRIS), Université Lumière - Lyon 2 (UL2)-École Centrale de Lyon (ECL), Université de Lyon-Université de Lyon-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Institut National des Sciences Appliquées de Lyon (INSA Lyon), Université de Lyon-Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Centre National de la Recherche Scientifique (CNRS)-Université Lumière - Lyon 2 (UL2)-École Centrale de Lyon (ECL), Université de Lyon-Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Centre National de la Recherche Scientifique (CNRS), IMPACT-DIGITRUST, Ecole Nationale Supérieure des Mines de St Etienne-Centre National de la Recherche Scientifique (CNRS)-Université Clermont Auvergne [2017-2020] (UCA [2017-2020]), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL), Institut National des Sciences Appliquées de Lyon (INSA Lyon), Université de Lyon-Institut National des Sciences Appliquées (INSA)-Université de Lyon-Institut National des Sciences Appliquées (INSA)-Centre National de la Recherche Scientifique (CNRS)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-École Centrale de Lyon (ECL), Université de Lyon-Université Lumière - Lyon 2 (UL2)-Institut National des Sciences Appliquées de Lyon (INSA Lyon), Université de Lyon-Université Lumière - Lyon 2 (UL2), Department of Algorithms, Computation, Image and Geometry (LORIA - ALGO), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, and Institut National de Recherche en Informatique et en Automatique (Inria)
Subjects: Theoretical computer science, Computer science, 02 engineering and technology, Theoretical Computer Science, Constraint Programming, [INFO.INFO-AI]Computer Science [cs]/Artificial Intelligence [cs.AI], [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], 0202 electrical engineering, electronic engineering, information engineering, Constraint programming, Differential (infinitesimal), Focus (computing), AES, business.industry, Advanced Encryption Standard, 020206 networking & telecommunications, Plaintext, Adversary, Related-key attacks, Longest path problem, Computer Science Applications, ACM: I.: Computing Methodologies/I.2: ARTIFICIAL INTELLIGENCE, Symmetric-key algorithm, Signal Processing, 020201 artificial intelligence & image processing, business, Information Systems
Abstract: International audience; The Advanced Encryption Standard (AES) is one of the most studied symmetric encryption schemes. During the last years, several attacks have been discovered in different adversarial models. In this paper, we focus on related-key differential attacks, where the adversary may introduce differences in plaintext pairs and also in keys. We show that Constraint Programming (CP) can be used to model these attacks, and that it allows us to efficiently find all optimal related-key differential characteristics for AES-128, AES-192 and AES-256. In particular, we improve the best related-key differential for the whole AES-256 and give the best related-key differential on 10 rounds of AES-192, which is the differential trail with the longest path. Those results allow us to improve existing related-key distinguishers, basic related-key attacks and q-multicollisions on AES-256.
Published: 2018
Full Text: View/download PDF

254. A Cryptographer's Conspiracy Santa

Author: Xavier Bultel and Jannik Dreier and Jean-Guillaume Dumas and Pascal Lafourcade, Bultel, Xavier, Dreier, Jannik, Dumas, Jean-Guillaume, Lafourcade, Pascal, Xavier Bultel and Jannik Dreier and Jean-Guillaume Dumas and Pascal Lafourcade, Bultel, Xavier, Dreier, Jannik, Dumas, Jean-Guillaume, and Lafourcade, Pascal
Abstract: In Conspiracy Santa, a variant of Secret Santa, a group of people offer each other Christmas gifts, where each member of the group receives a gift from the other members of the group. To that end, the members of the group form conspiracies, to decide on appropriate gifts, and usually divide the cost of each gift among all participants of that conspiracy. This requires to settle the shared expenses per conspiracy, so Conspiracy Santa can actually be seen as an aggregation of several shared expenses problems. First, we show that the problem of finding a minimal number of transaction when settling shared expenses is NP-complete. Still, there exists good greedy approximations. Second, we present a greedy distributed secure solution to Conspiracy Santa. This solution allows a group of people to share the expenses for the gifts in such a way that no participant learns the price of his gift, but at the same time notably reduces the number of transactions with respect to a naive aggregation. Furthermore, our solution does not require a trusted third party, and can either be implemented physically (the participants are in the same room and exchange money using envelopes) or, virtually, using a cryptocurrency.
Published: 2018
Full Text: View/download PDF

255. Les monnaies virtuelles décentralisées sont-elles des dispositifs d’avenir ?

Author: Ariane Tichit, Pascal Lafourcade, and Vincent Mazenod
Subjects: crypto-monnaies, lcsh:HB71-74, lcsh:Economics as a science, monnaies locales, crypto-currencies, monetary, lcsh:Economic history and conditions, innovations, LETs, social currencies, lcsh:HC10-1085, monnaies virtuelles décentralisées, SELs, decentralized virtual currencies
Abstract: Dans cet article nous défendons l’idée que les monnaies virtuelles décentralisées peuvent contribuer au changement systémique impulsé par l’ESS. Nous montrons tout d’abord qu’elles cumulent en effet des points forts des monnaies locales et des SELs dans leur pouvoir transformateur et apportent des solutions à certaines de leurs faiblesses, tout en ayant évidemment leurs propres limites. Ensuite, nous soulignons qu’une grande diversification est en cours au sein des crypto-monnaies et que certaines d’entre elles développent désormais des protocoles économes en énergie plus utiles à la collectivité ou basés sur la coopération, alors que d’autres se mettent au service de projets à valeurs proches de l’ESS. Ceci pourrait fédérer deux courants qui pour le moment s’opposent sur les valeurs et ainsi créer un mouvement d’une ampleur suffisante pour représenter un véritable contre-pouvoir face aux structures dominantes. Nous émettons toutefois des critiques sur ces dispositifs et proposons, en dernier lieu, une idée de crypto-monnaie géolocalisée avec fonte qui pourrait répondre à certaines limites rencontrées notamment par les monnaies locales dans leur définition de la proximité. In this paper we argue that decentralized virtual currencies can contribute to systemic change driven by SSE. We first show that they cumulate a number of the strengths of local currencies and SELs in their transformative power and provide solutions to some of their weaknesses, while obviously having their own limitations. Secondly, we emphasize that there is a great diversification within crypto-currencies and that some of them are now developing energy-saving protocols that are more useful to the community or based on cooperation, while others serve projects close to SSE. The fusion of these projects, that have a priori opposed values, could therefore create a movement of sufficient magnitude to begin to represent a true counter-power. However, we have some criticisms of these devices and finally propose an idea of crypto-coin with geolocalized demurrage that could meet certain limits encountered especially by local currencies in their definition of proximity.
Published: 2017

256. Les monnaies virtuelles décentralisées sont-elles des dispositifs d’avenir ?

Author: Pascal Lafourcade, Vincent Mazenod, and Ariane Tichit
Subjects: Marketing, Pharmacology, Organizational Behavior and Human Resource Management, Cryptocurrency, Solidarity economy, Strategy and Management, New energy, Pharmaceutical Science, ComputingMilieux_LEGALASPECTSOFCOMPUTING, Virtual currency, Microeconomics, Economy, Social transformation, Digital currency, Drug Discovery, Economics, ComputingMilieux_COMPUTERSANDSOCIETY, Theoretical psychology
Abstract: In this article, we show that decentralized virtual currencies can be powerful tools for societal transformation. Indeed, the study of the joint and disjoint elements between the first Bitcoin currencies, SELs and local currencies, reveals that these projects are not so far. Then, we present the current evolution of crypto-currencies towards new energy aware, community-based, useful and fundamentally innovative protocols, emphazing their strong potential. Finally, some recent crypto-currencies are close to the values of the Social and Solidarity Economy, and even though they have some technical and theoretical problems, they have the merit of offering new perspectives. Finally, we propose an idea of decentralized money geolocalized melty, which would allow us to meet a certain number of limits that are experienced by traditional local currencies.
Published: 2017
Full Text: View/download PDF

257. Formal Analysis of Combinations of Secure Protocols

Author: Jannik Dreier, Pascal Lafourcade, Elliott Blot, Université Clermont Auvergne [2017-2020] (UCA [2017-2020]), Proof techniques for security protocols (PESTO), Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL), This work was supported in part by the project C-ROADS, by the Indo-French Centre for the Promotion of Advanced Research (IFCPAR) and Center Franco-Indien Pour LA Promotion DE LA Recherche Avancee (CEFIPRA) through the project DST/CNRS 2015-03 under DST-INRIA-CNRS TargetedProgramme., Laboratoire d'Informatique, de Modélisation et d'Optimisation des Systèmes (LIMOS), Ecole Nationale Supérieure des Mines de St Etienne-Centre National de la Recherche Scientifique (CNRS)-Université Clermont Auvergne [2017-2020] (UCA [2017-2020]), This research was conducted with the support of the Indo-French Centre for the Promotion of Advanced Research (IFCPAR) and the Center Franco-Indien Pour La Promotion De La Recherche Avanc ́ee (CEFIPRA) through the project DST/CNRS 2015-03 under DST-INRIA-CNRS Targeted Programme, and by the CNRS PEPS SISC ASSI 2016/2017., ANR-16-IDEX-0001,CAP 20-25,CAP 20-25(2016), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Ecole Nationale Supérieure des Mines de St Etienne-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])-Centre National de la Recherche Scientifique (CNRS), Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])-Centre National de la Recherche Scientifique (CNRS), and Dreier, Jannik
Subjects: Protocol (science), Otway–Rees protocol, Computer science, Formal methods, ComputerSystemsOrganization_COMPUTER-COMMUNICATIONNETWORKS, Symbolic model, 0102 computer and information sciences, 02 engineering and technology, Gas meter prover, Computer security, computer.software_genre, 01 natural sciences, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], 010201 computation theory & mathematics, Universal composability, ACM: D.: Software/D.4: OPERATING SYSTEMS/D.4.6: Security and Protection/D.4.6.6: Verification, 0202 electrical engineering, electronic engineering, information engineering, Security, 020201 artificial intelligence & image processing, Isolation (database systems), Tamarin, computer, [INFO.INFO-CR] Computer Science [cs]/Cryptography and Security [cs.CR]
Abstract: International audience; When trying to prove the security of a protocol, one usually analyzes the protocol in isolation, i.e., in a network with no other protocols. But in reality, there will be many protocols operating on the same network, maybe even sharing data including keys, and an intruder may use messages of one protocol to break another. We call that a multi-protocol attack. In this paper, we try to find such attacks using the Tamarin prover. We analyze both examples that were previously analyzed by hand or using other tools, and find novel attacks.
Published: 2017
Full Text: View/download PDF

258. Duck Attack on Accountable Distributed Systems

Author: Pascal Lafourcade, Cédric Lauradoux, Amrit Kumar, National University of Singapore (NUS), Privacy Models, Architectures and Tools for the Information Society (PRIVATICS), Inria Grenoble - Rhône-Alpes, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-CITI Centre of Innovation in Telecommunications and Integration of services (CITI), Institut National des Sciences Appliquées de Lyon (INSA Lyon), Institut National des Sciences Appliquées (INSA)-Université de Lyon-Institut National des Sciences Appliquées (INSA)-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National des Sciences Appliquées de Lyon (INSA Lyon), Institut National des Sciences Appliquées (INSA)-Université de Lyon-Institut National des Sciences Appliquées (INSA)-Université de Lyon, Laboratoire d'Informatique, de Modélisation et d'Optimisation des Systèmes (LIMOS), Ecole Nationale Supérieure des Mines de St Etienne-Centre National de la Recherche Scientifique (CNRS)-Université Clermont Auvergne [2017-2020] (UCA [2017-2020]), Université de Lyon-Institut National des Sciences Appliquées (INSA)-Université de Lyon-Institut National des Sciences Appliquées (INSA)-Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National des Sciences Appliquées de Lyon (INSA Lyon), Université de Lyon-Institut National des Sciences Appliquées (INSA)-Université de Lyon-Institut National des Sciences Appliquées (INSA)-Inria Lyon, Institut National de Recherche en Informatique et en Automatique (Inria), Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])-Centre National de la Recherche Scientifique (CNRS), and Lauradoux, Cédric
Subjects: Cryptographic primitive, Exploit, Computer science, business.industry, Secure log, Distributed computing, Hash function, Duck attack, 020206 networking & telecommunications, Cryptography, Public verifiability, 02 engineering and technology, Cryptographic protocol, Data structure, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], 020204 information systems, 0202 electrical engineering, electronic engineering, information engineering, Key (cryptography), 020201 artificial intelligence & image processing, Accountability, business, Protocol (object-oriented programming), [INFO.INFO-CR] Computer Science [cs]/Cryptography and Security [cs.CR]
Abstract: International audience; Accountability plays a key role in dependable distributed systems.It allows to detect, isolate and churn malicious/selfish nodes thatdeviate from a prescribed protocol. To achieve these properties, sev-eral accountable systems use at their core cryptographic primitivesthat produce non-repudiable evidence of inconsistent or incorrectbehavior.In this paper, we show how selfish and colluding nodes canexploit the use of cryptographic digests in accountability protocolsto mount what we call a duck attack. In a duck attack, selfish andcolluding nodes exploit the use of cryptographic digests to alter thetransmission of messages while masquerading as honest entities.The end result is that their selfish behavior remains undetected. Thisundermines the security guarantees of the accountability protocols.We first discover the duck attack while analyzing PAG — a cus-tom cryptographic protocol to build accountable systems presentedat ICDCS 2016. We later discover that accountable distributed sys-tems based on a secure log (essentially a hash-based data structure)are also vulnerable to the duck attack and apply it on AcTinG — aprotocol presented at SRDS 2014. To defeat our attack, we modifythe underlying secure log to have high-order dependency on themessages stored in it.
Published: 2017

259. Dual Protocols for Private Multi-party Matrix Multiplication and Trust Computations

Author: Maxime Puys, Pascal Lafourcade, Jean-Baptiste Orfila, Jean-Guillaume Dumas, Calculs Algébriques et Systèmes Dynamiques (CASYS), Laboratoire Jean Kuntzmann (LJK ), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019])-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019]), Laboratoire d'Informatique, de Modélisation et d'optimisation des Systèmes (LIMOS), Université Blaise Pascal - Clermont-Ferrand 2 (UBP)-Université d'Auvergne - Clermont-Ferrand I (UdA)-SIGMA Clermont (SIGMA Clermont)-Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Centre National de la Recherche Scientifique (CNRS), Université Clermont Auvergne [2017-2020] (UCA [2017-2020]), VERIMAG (VERIMAG - IMAG), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019]), ANR-11-LABX-0025,PERSYVAL-lab,Systemes et Algorithmes Pervasifs au confluent des mondes physique et numérique(2011), European Project: 676541,H2020,H2020-EINFRA-2015-1,OpenDreamKit(2015), and SIGMA Clermont (SIGMA Clermont)-Université d'Auvergne - Clermont-Ferrand I (UdA)-Ecole Nationale Supérieure des Mines de St Etienne-Centre National de la Recherche Scientifique (CNRS)-Université Blaise Pascal - Clermont-Ferrand 2 (UBP)
Subjects: Theoretical computer science, General Computer Science, Computer science, Volume (computing), Homomorphic encryption, 020206 networking & telecommunications, 02 engineering and technology, Cryptographic protocol, Matrix multiplication, Dual (category theory), [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Privacy, Secure Multiparty Computation MPC, 0202 electrical engineering, electronic engineering, information engineering, 020201 artificial intelligence & image processing, Law, Protocol (object-oriented programming), Countermeasure (computer), Adversary model, Matrix Multiplication
Abstract: International audience; 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 two dual protocols 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 cryptographic protocol verification tools, we are able to check the security of both protocols and provide a countermeasure for each attack found by the tools. We also give a generic 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.
Published: 2017
Full Text: View/download PDF

260. Verifiable Private Polynomial Evaluation

Author: David Gerault, Manik Lal Das, Pascal Lafourcade, Xavier Bultel, Hardik Gajera, Matthieu Giraud, Université Clermont Auvergne [2017-2020] (UCA [2017-2020]), Laboratoire d'Informatique, de Modélisation et d'Optimisation des Systèmes (LIMOS), Ecole Nationale Supérieure des Mines de St Etienne-Centre National de la Recherche Scientifique (CNRS)-Université Clermont Auvergne [2017-2020] (UCA [2017-2020]), Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])-Centre National de la Recherche Scientifique (CNRS), Lafourcade, Pascal, and Ecole Nationale Supérieure des Mines de St Etienne-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])-Centre National de la Recherche Scientifique (CNRS)
Subjects: Security properties, Discrete mathematics, Polynomial, 0102 computer and information sciences, 02 engineering and technology, Function (mathematics), 01 natural sciences, law.invention, Random oracle, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], 010201 computation theory & mathematics, law, 020204 information systems, Scheme (mathematics), 0202 electrical engineering, electronic engineering, information engineering, Verifiable secret sharing, ACM: K.: Computing Milieux/K.4: COMPUTERS AND SOCIETY/K.4.4: Electronic Commerce/K.4.4.5: Security, Cryptanalysis, Mathematics, [INFO.INFO-CR] Computer Science [cs]/Cryptography and Security [cs.CR]
Abstract: Delegating the computation of a polynomial to a server in a verifiable way is challenging. An even more challenging problem is ensuring that this polynomial remains hidden to clients who are able to query such a server. In this paper, we formally define the notion of Private Polynomial Evaluation (PPE). Our main contribution is to design a rigorous security model along with relations between the different security properties. We define polynomial protection (\(\textsf {PP}\)), proof unforgeability (\(\textsf {UNF}\)), and indistinguishability against chosen function attack (\(\textsf {IND}\text {-}\textsf {CFA}\)), which formalizes the resistance of a PPE against attackers trying to guess which polynomial is used among two polynomials of their choice. As a second contribution, we give a cryptanalysis of two PPE schemes of the literature. Finally, we design a PPE scheme called \(\mathsf {PIPE}\) and we prove that it is \(\textsf {PP}\)-, \(\textsf {UNF}\)- and \(\textsf {IND}\text {-}\textsf {CFA}\)-secure under the decisional Diffie-Hellman assumption in the random oracle model.
Published: 2017

261. Vérifier la sécurité de nos communications

Author: pascal lafourcade, Université Clermont Auvergne [2017-2020] (UCA [2017-2020]), Laboratoire d'Informatique, de Modélisation et d'Optimisation des Systèmes (LIMOS), Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])-Centre National de la Recherche Scientifique (CNRS), ANR-16-IDEX-0001,CAP 20-25,CAP 20-25(2016), Ecole Nationale Supérieure des Mines de St Etienne-Centre National de la Recherche Scientifique (CNRS)-Université Clermont Auvergne [2017-2020] (UCA [2017-2020]), ANR-16-IDEX-0001,CAP 20-25,CAP 20-25 (I-Site)(2016), Ecole Nationale Supérieure des Mines de St Etienne-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])-Centre National de la Recherche Scientifique (CNRS), Interstices, inria, and CAP 20-25 - - CAP 20-252016 - ANR-16-IDEX-0001 - IDEX - VALID
Subjects: vérification automatique, algorithmes symétriques, algorithmes asymétriques, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], algorithmes de chiffrement, algorithmes à clé publique, protocole de communication, sécurité réseau, [INFO.INFO-CR] Computer Science [cs]/Cryptography and Security [cs.CR], protocole cryptographique
Abstract: National audience; Quand nous échangeons des messages numériques, nous sommes persuadés de communiquer avec l'interlocuteur que nous avons choisi. Pour s'en assurer réellement, il faut mettre en place des protocoles de communication sécurisés. Mais même en utilisant des canaux sûrs, cela peut ne pas suffire comme l'illustre l'attaque de G. Lowe dite « de l'homme du milieu ».
Published: 2017

262. SR3: secure resilient reputation-based routing

Author: Pascal Lafourcade, Stéphane Devismes, Karine Altisen, Raphaël Jamet, VERIMAG (VERIMAG - IMAG), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019]), Université Grenoble Alpes [2016-2019] (UGA [2016-2019]), Laboratoire d'Informatique, de Modélisation et d'Optimisation des Systèmes (LIMOS), Ecole Nationale Supérieure des Mines de St Etienne-Centre National de la Recherche Scientifique (CNRS)-Université Clermont Auvergne [2017-2020] (UCA [2017-2020]), Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])-Centre National de la Recherche Scientifique (CNRS), SYNCHRONE, Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Grenoble (INPG)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Université Joseph Fourier - Grenoble 1 (UJF)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Grenoble (INPG)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Université Joseph Fourier - Grenoble 1 (UJF), Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Grenoble (INPG)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Université Joseph Fourier - Grenoble 1 (UJF), Ecole Nationale Supérieure des Mines de St Etienne-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])-Centre National de la Recherche Scientifique (CNRS), Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS), and Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)
Subjects: Routing protocol, Dynamic Source Routing, Equal-cost multi-path routing, Computer Networks and Communications, Computer science, Routing table, media_common.quotation_subject, 02 engineering and technology, security, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], 0202 electrical engineering, electronic engineering, information engineering, Electrical and Electronic Engineering, media_common, Static routing, Cryptographic primitive, business.industry, Policy-based routing, ComputerSystemsOrganization_COMPUTER-COMMUNICATIONNETWORKS, 020206 networking & telecommunications, resiliency, 020202 computer hardware & architecture, Link-state routing protocol, routing, Multipath routing, 020201 artificial intelligence & image processing, Routing (electronic design automation), Index Terms—Wireless sensor networks, business, Wireless sensor network, Information Systems, Computer network, Reputation
Abstract: International audience; In this paper, we propose SR3 (which means Secure Resilient Reputation-based Routing), a secure and resilient algorithm for convergecast routing in WSNs (Wireless Sensor Networks). SR3 uses lightweight cryptographic primitives to achieve data confidentiality and unforgeability. Security of SR3 has been proven formally using two verification tools: CryptoVerif and Scyther. 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.
Published: 2017
Full Text: View/download PDF

263. Formal analysis and offline monitoring of electronic exams

Author: Yliès Falcone, Ali Kassem, Pascal Lafourcade, VERIMAG (VERIMAG - IMAG), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019]), Concurrency, Mobility and Transactions (COMETE), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X), Compiler Optimization and Run-time Systems (CORSE), Inria Grenoble - Rhône-Alpes, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire d'Informatique de Grenoble (LIG ), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019])-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019]), Laboratoire d'Informatique, de Modélisation et d'Optimisation des Systèmes (LIMOS), Ecole Nationale Supérieure des Mines de St Etienne-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])-Centre National de la Recherche Scientifique (CNRS), Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), and Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])-Centre National de la Recherche Scientifique (CNRS)
Subjects: Java, ComputingMilieux_THECOMPUTINGPROFESSION, Event (computing), Computer science, Programming language, 020207 software engineering, 02 engineering and technology, [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE], Cryptographic protocol, computer.software_genre, Theoretical Computer Science, Automaton, Hardware and Architecture, Information and Communications Technology, 0202 electrical engineering, electronic engineering, information engineering, ComputingMilieux_COMPUTERSANDEDUCATION, 020201 artificial intelligence & image processing, [INFO.INFO-ES]Computer Science [cs]/Embedded Systems, computer, Software, computer.programming_language
Abstract: International audience; More and more universities are moving toward electronic exams (in short e-exams). This migration exposes exams to additional threats, which may come from the use of the information and communication technology. In this paper, we identify and define several security properties for e-exam systems. Then, we show how to use these properties in two complementary approaches: model-checking and monitoring. We illustrate the validity of our definitions by analyzing a real e-exam used at the pharmacy faculty of University Grenoble Alpes (UGA) to assess students. On the one hand, we instantiate our properties as queries for ProVerif, an automatic verifier of cryptographic protocols, and we use it to check our modeling of UGA exam specifications. ProVerif found some attacks. On the other hand, we express our properties as Quantified Event Automata (QEAs), and we synthesize them into monitors using MarQ, a Java tool designed to implement QEAs. Then, we use these monitors to verify real exam executions conducted by UGA. Our monitors found fraudulent students and discrepancies between the specifications of UGA exam and its implementation.
Published: 2017
Full Text: View/download PDF

264. LOCALPKI: A User-Centric Formally Proven Alternative to PKIX

Author: Pascal Lafourcade, Jean-Baptiste Orfila, Pascal Thoniel, Jean-Guillaume Dumas, Francis Melemedjian, Calculs Algébriques et Systèmes Dynamiques (CASYS), Laboratoire Jean Kuntzmann (LJK ), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019])-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019]), Laboratoire d'Informatique, de Modélisation et d'Optimisation des Systèmes (LIMOS), Ecole Nationale Supérieure des Mines de St Etienne-Centre National de la Recherche Scientifique (CNRS)-Université Clermont Auvergne [2017-2020] (UCA [2017-2020]), NTX Research SA (NTX Research SA), ANR-11-LABX-0025,PERSYVAL-lab,Systemes et Algorithmes Pervasifs au confluent des mondes physique et numérique(2011), European Project: 676541,H2020,H2020-EINFRA-2015-1,OpenDreamKit(2015), and Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])-Centre National de la Recherche Scientifique (CNRS)
Subjects: 060201 languages & linguistics, education.field_of_study, Computer science, business.industry, End user, Population, Public key infrastructure, 06 humanities and the arts, 02 engineering and technology, Cryptographic protocol, Computer security, computer.software_genre, Registration authority, Public-key cryptography, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], 0602 languages and literature, Certificate authority, 0202 electrical engineering, electronic engineering, information engineering, ACM: K.: Computing Milieux/K.6: MANAGEMENT OF COMPUTING AND INFORMATION SYSTEMS/K.6.5: Security and Protection, 020201 artificial intelligence & image processing, ACM: K.: Computing Milieux/K.4: COMPUTERS AND SOCIETY/K.4.4: Electronic Commerce/K.4.4.5: Security, education, business, computer, User-centered design
Abstract: International audience; A public-key infrastructure (PKI) binds public keys to identities of entities. Usually, this binding is established through a process of registration and issuance of certificates by a certificate authority (CA) where the validation of the registration is performed by a local registration authority. In this paper, we propose an alternative scheme, called LOCALPKI, where the binding is performed by the local authority and the issuance is left to the end user or to the local authority. The role of our third entity is then to register this binding and to provide up-to-date status information on this registration. The idea is that many more local actors could then take the role of a local authority, thus allowing for an easier spread of public-key certificates in the population. We also prove our scheme's security with Tamarin an automatic verification tool of cryptographic protocols.
Published: 2017
Full Text: View/download PDF

265. Formally Verifying Flow Properties in Industrial Systems

Author: Maxime Puys, Jannik Dreier, Jean-Louis Roch, Pascal Lafourcade, Marie-Laure Potet, Proof techniques for security protocols (PESTO), Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL), VERIMAG (VERIMAG - IMAG), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019]), Université Clermont Auvergne [2017-2020] (UCA [2017-2020]), Laboratoire d'Informatique, de Modélisation et d'Optimisation des Systèmes (LIMOS), Ecole Nationale Supérieure des Mines de St Etienne-Centre National de la Recherche Scientifique (CNRS)-Université Clermont Auvergne [2017-2020] (UCA [2017-2020]), This work has been partially funded by the CNRS PEPS SISC ASSI 2016., ANR-11-LABX-0025,PERSYVAL-lab,Systemes et Algorithmes Pervasifs au confluent des mondes physique et numérique(2011), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])-Centre National de la Recherche Scientifique (CNRS), and Ecole Nationale Supérieure des Mines de St Etienne-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])-Centre National de la Recherche Scientifique (CNRS)
Subjects: [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Computer science, industrial systems, Systems engineering, Industrial systems, automated verification, [INFO.INFO-ES]Computer Science [cs]/Embedded Systems, SCADA, Flow properties, Security protocols, [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL], symbolic model, flow integrity
Abstract: International audience; In contrast to other IT systems, industrial systems often do not only require classical properties like data confidentiality or authentication of the communication, but have special needs due to their interaction with physical world. For example, the reordering or deletion of some commands sent to a machine can cause the system to enter an unsafe state with potentially catastrophic effects. To prevent such attacks, the integrity of the message flow is necessary. We provide a formal definition of Flow Integrity. We apply our framework to two well-known industrial protocols: OPC-UA and MODBUS. Using TAMARIN, a cryptographic protocol verification tool, we confirm that most of the secure modes of these protocols ensure Flow Integrity given a resilient network. However, we also identify a weakness in a supposedly secure version of MODBUS.
Published: 2017
Full Text: View/download PDF

266. Breaking and fixing the HB+DB protocol

Author: David Gerault, Cristina Onete, Pascal Lafourcade, Ioana Boureanu, University of Surrey (UNIS), Université Clermont Auvergne [2017-2020] (UCA [2017-2020]), Laboratoire d'Informatique, de Modélisation et d'Optimisation des Systèmes (LIMOS), Ecole Nationale Supérieure des Mines de St Etienne-Centre National de la Recherche Scientifique (CNRS)-Université Clermont Auvergne [2017-2020] (UCA [2017-2020]), EMbedded SEcurity and Cryptography (EMSEC), SYSTÈMES LARGE ÉCHELLE (IRISA-D1), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), CentraleSupélec-Télécom Bretagne-Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Rennes (ENS Rennes)-Université de Bretagne Sud (UBS)-Centre National de la Recherche Scientifique (CNRS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-CentraleSupélec-Télécom Bretagne-Université de Rennes 1 (UR1), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA), ANR-05-GANI-0001,GenOvul,Exploitation de la variabilité génétique intra et inter-espèces pour l'étude du déterminisme génétique du taux d'ovulation(2005), Université Clermont Auvergne (UCA), Ecole Nationale Supérieure des Mines de St Etienne-Université Clermont Auvergne (UCA)-Centre National de la Recherche Scientifique (CNRS), Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Université de Bretagne Sud (UBS)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-CentraleSupélec-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Université de Rennes (UNIV-RENNES)-CentraleSupélec-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Université de Rennes (UNIV-RENNES)-CentraleSupélec, Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])-Centre National de la Recherche Scientifique (CNRS), Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), and Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)
Subjects: [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Computer science, 0202 electrical engineering, electronic engineering, information engineering, 020206 networking & telecommunications, 020201 artificial intelligence & image processing, 02 engineering and technology, Computer security, computer.software_genre, Topology, computer, Protocol (object-oriented programming)
Abstract: International audience; The HB protocol and its HB + successor are lightweight authentication schemes based on the Learning Parity with Noise (LPN) problem. They both suffer from the so-called GRS-attack whereby a man-in-the-middle (MiM) adversary can recover the secret key. At WiSec 2015, Pagnin et al. proposed the HB+DB protocol: HB + with an additional distance-bounding dimension added to detect and counteract such MiM attacks. They showed experimentally that HB+DB was resistant to GRS adversaries, and also advanced HB+DB as a distance-bounding protocol, discussing its resistance to worst-case distance-bounding attackers. In this paper, we exhibit flaws both in the authentication and distance-bounding layers of HB+DB; these vulnerabilities encompass practical attacks as well as provable security shortcomings. First, we show that HB+DB may be impractical as a secure distance-bounding protocol, as its distance-fraud and mafia-fraud security-levels scale poorly compared to other distance-bounding protocols. Secondly, we describe an effective MiM attack against HB+DB: our attack refines the GRS-strategy and still leads to key-recovery by the attacker, yet this is not deterred by HB+DB's distance-bounding. Thirdly, we refute the claim that HB+DB's security against passive attackers relies on the hardness of the LPN problem. We also discuss how (erroneously) requiring such hardness, in fact, lowers HB+DB's efficiency and its resistance to authentication and distance-bounding attacks. Drawing on HB+DB's design flaws, we also propose a new distance-bounding protocol – BLOG. It retains parts of HB+DB, yet BLOG is provably secure, even – in particular – against MiM attacks. Moreover, BLOG enjoys better practical security (asymptotical in the security parameter).
Published: 2017
Full Text: View/download PDF

267. SPADE : un protocole délimiteur de distance anonyme et résistant à la fraude terroriste

Author: Xavier Bultel, Sébastien Gambs, David Gérault, pascal lafourcade, Cristina Onete, Jean-Marc Robert, Université Clermont Auvergne [2017-2020] (UCA [2017-2020]), Université du Québec à Montréal = University of Québec in Montréal (UQAM), Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES), Ecole de Technologie Supérieure [Montréal] (ETS), and Lafourcade, Pascal
Subjects: [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], [INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI], [INFO.INFO-NI] Computer Science [cs]/Networking and Internet Architecture [cs.NI], Distance bounding, Sécurité, [INFO.INFO-CR] Computer Science [cs]/Cryptography and Security [cs.CR]
Abstract: International audience; Les communications sans contact sont omniprésentes dans notre quotidien, allant des badges de contrôle d'accès au passeport électronique. Ces systèmes sont sensibles aux attaques par relais, dans lesquelles un adversaire transfère simplement les messages entre le prouveur et le vérifieur pour usurper l'identité du prouveur. Les protocoles délimiteurs de distance (distance-bounding) ont été ont ntroduits pour contrer ces attaques en assurant une borne sur la distance entre le prouveur et le vérifieur grâcè a la mesure du temps des communications. Par la suite de nombreux travaux ont amélioré la sécurité de ces protocoles, mais ont aussi cherché à assurer le respect de la vie privée face à des adversaires actifs et également face à des vérifieurs malicieux. En particulier, une menace difficile à prévenir est la fraude terroriste, où un prouveur lointain coopère avec un complice proche pour tromper le vérifieur. La contre-mesure usuelle pour cette menace est de rendre impossible l'action du complice sans l'aide du prouveur lointain, à moins que le prouveur ne lui donne suffisamment d'information pour qu'il retrouve sa clef privée et puisse ainsi toujours se faire passer pour le prouveur. Dans cet article, nous proposons une nouvelle approche où le prouveur ne révèle pas sa clef privée mais utilise une clef de session avec une signature de groupe, la rendant ainsi utilisable plusieurs fois. Ceci permet à un adversaire d'usurper l'identité du prouveur sans même connaître sa clef de signature. Grâce à cette approche nous proposons SPADE le premier protocole de délimiteur de distance qui est anonyme, révocable et formellement prouvé sûr. Mots-clefs : Protocole délimiteur de distance (Distance Bounding), Sécurité, résitance à la fraude terroriste.
Published: 2017

268. A Terrorist-fraud Resistant and Extractor-free Anonymous Distance-bounding Protocol

Author: Jean-Marc Robert, Gildas Avoine, Cristina Onete, Xavier Bultel, Pascal Lafourcade, David Gerault, Sébastien Gambs, EMbedded SEcurity and Cryptography (EMSEC), SYSTÈMES LARGE ÉCHELLE (IRISA-D1), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Université de Bretagne Sud (UBS)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-CentraleSupélec-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Université de Rennes (UNIV-RENNES)-CentraleSupélec-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Université de Rennes (UNIV-RENNES)-CentraleSupélec, Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES), Institut Universitaire de France (IUF), Ministère de l'Education nationale, de l’Enseignement supérieur et de la Recherche (M.E.N.E.S.R.), Laboratoire d'Informatique, de Modélisation et d'Optimisation des Systèmes (LIMOS), Ecole Nationale Supérieure des Mines de St Etienne-Université Clermont Auvergne (UCA)-Centre National de la Recherche Scientifique (CNRS), Université Clermont Auvergne (UCA), Université du Québec à Montréal (UQAM), Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT), Ecole de Technologie Supérieure [Montréal] (ETS), CentraleSupélec-Télécom Bretagne-Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Rennes (ENS Rennes)-Université de Bretagne Sud (UBS)-Centre National de la Recherche Scientifique (CNRS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-CentraleSupélec-Télécom Bretagne-Université de Rennes 1 (UR1), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA), Ecole Nationale Supérieure des Mines de St Etienne-Centre National de la Recherche Scientifique (CNRS)-Université Clermont Auvergne [2017-2020] (UCA [2017-2020]), Université Clermont Auvergne [2017-2020] (UCA [2017-2020]), Université du Québec à Montréal = University of Québec in Montréal (UQAM), Université de Bretagne Sud (UBS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Rennes (ENS Rennes)-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-CentraleSupélec-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS), Institut National des Sciences Appliquées (INSA), Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])-Centre National de la Recherche Scientifique (CNRS), Université de Rennes (UR), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes 1 (UR1), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), and Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)
Subjects: Protocol (science), Authentication, Computer science, 020206 networking & telecommunications, Context (language use), 02 engineering and technology, 16. Peace & justice, Computer security, computer.software_genre, ComputingMilieux_MANAGEMENTOFCOMPUTINGANDINFORMATIONSYSTEMS, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Authentication protocol, Universal composability, 0202 electrical engineering, electronic engineering, information engineering, Key (cryptography), 020201 artificial intelligence & image processing, Distance-bounding protocol, computer
Abstract: 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.
Published: 2017
Full Text: View/download PDF

269. Bitcoin : une monnaie dématérialisée

Author: pascal lafourcade, Jean-Guillaume Dumas, Laboratoire d'Informatique, de Modélisation et d'Optimisation des Systèmes (LIMOS), Ecole Nationale Supérieure des Mines de St Etienne-Centre National de la Recherche Scientifique (CNRS)-Université Clermont Auvergne [2017-2020] (UCA [2017-2020]), Calculs Algébriques et Systèmes Dynamiques (CASYS), Laboratoire Jean Kuntzmann (LJK ), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019])-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019]), ANR-16-IDEX-0001,CAP 20-25,CAP 20-25(2016), and Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])-Centre National de la Recherche Scientifique (CNRS)
Subjects: [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], ComputingMilieux_MISCELLANEOUS
Abstract: International audience
Published: 2017

270. Les monnaies virtuelles décentralisées sont-elles des outils d’avenir ?

Author: Ariane Tichit, pascal lafourcade, Vincent Mazenod, Etudes & Documents - Publications, CERDI, CAP 20-25 - - CAP 20-252016 - ANR-16-IDEX-0001 - IDEX - VALID, Centre d'Études et de Recherches sur le Développement International (CERDI), Université d'Auvergne - Clermont-Ferrand I (UdA)-Centre National de la Recherche Scientifique (CNRS), Laboratoire d'Informatique, de Modélisation et d'Optimisation des Systèmes (LIMOS), Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])-Centre National de la Recherche Scientifique (CNRS), ANR-16-IDEX-0001,CAP 20-25,CAP 20-25(2016), Ecole Nationale Supérieure des Mines de St Etienne-Centre National de la Recherche Scientifique (CNRS)-Université Clermont Auvergne [2017-2020] (UCA [2017-2020]), and Ecole Nationale Supérieure des Mines de St Etienne-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])-Centre National de la Recherche Scientifique (CNRS)
Subjects: Decentralized virtual currencies, LETs, ComputingMilieux_COMPUTERSANDSOCIETY, ComputingMilieux_LEGALASPECTSOFCOMPUTING, Social currencies, Monetary innovations, [SHS.ECO]Humanities and Social Sciences/Economics and Finance, [SHS.ECO] Humanities and Social Sciences/Economics and Finance, Crypto-currencies
Abstract: In this article, we show that decentralized virtual currencies can be powerful tools for societal transformation. Indeed, the study of the joint and disjoint elements between the first Bitcoin currencies, SELs and local currencies, reveals that these projects are not so far. Then, we present the current evolution of crypto-currencies towards new energy aware, community-based, useful and fundamentally innovative protocols, emphazing their strong potential. Finally, some recent crypto-currencies are close to the values of the Social and Solidarity Economy, and even though they have some technical and theoretical problems, they have the merit of offering new perspectives. Finally, we propose an idea of decentralized money geolocalized melty, which would allow us to meet a certain number of limits that are experienced by traditional local currencies.
Published: 2017

271. Evaluation of Secure Multi-Hop Node Authentication and Key Establishment Mechanisms for Wireless Sensor Networks

Author: Gerard Chalhoub, Pascal Lafourcade, Ismail Mansour, Laboratoire d'Informatique, de Modélisation et d'optimisation des Systèmes (LIMOS), SIGMA Clermont (SIGMA Clermont)-Université d'Auvergne - Clermont-Ferrand I (UdA)-Ecole Nationale Supérieure des Mines de St Etienne-Centre National de la Recherche Scientifique (CNRS)-Université Blaise Pascal - Clermont-Ferrand 2 (UBP), and Université Blaise Pascal - Clermont-Ferrand 2 (UBP)-Université d'Auvergne - Clermont-Ferrand I (UdA)-SIGMA Clermont (SIGMA Clermont)-Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Centre National de la Recherche Scientifique (CNRS)
Subjects: Control and Optimization, Computer Networks and Communications, Computer science, Distributed computing, 02 engineering and technology, security, lcsh:Technology, Formal proof, Hop (networking), [INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI], overhead of protection, 0202 electrical engineering, electronic engineering, information engineering, wireless sensor networks, formal verification, Instrumentation, Formal verification, business.industry, lcsh:T, ComputerSystemsOrganization_COMPUTER-COMMUNICATIONNETWORKS, 020206 networking & telecommunications, Cryptographic protocol, Key distribution in wireless sensor networks, authentication, multi-hop, Authentication protocol, 020201 artificial intelligence & image processing, Challenge–response authentication, business, Wireless sensor network, Computer network
Abstract: International audience; Designing secure authentication mechanisms in wireless sensor networks in order to associate a node to a secure network is not an easy task due to the limitations of this type of networks. In this paper, we propose different multi-hop node authentication protocols for wireless sensor networks. For each protocol, we provide a formal proof to verify the security of our proposals using Scyther, which is an automatic cryptographic protocols verification tool. We also provide implementation results in terms of execution time consumption obtained by real measurements on TelosB motes. These protocols offer different security mechanisms depending on the design of the protocol itself. Moreover, we evaluate the overhead of protection of each solution by studying the effect on execution time overhead of each protocol. Finally, we propose a mechanism to detect possible attack based on our evaluation results.
Published: 2014
Full Text: View/download PDF

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

Author: Marie-Laure Potet, Pascal Lafourcade, Maxime Puys, VERIMAG (VERIMAG - IMAG), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019]), Laboratoire d'Informatique, de Modélisation et d'optimisation des Systèmes (LIMOS), SIGMA Clermont (SIGMA Clermont)-Université d'Auvergne - Clermont-Ferrand I (UdA)-Ecole Nationale Supérieure des Mines de St Etienne-Centre National de la Recherche Scientifique (CNRS)-Université Blaise Pascal - Clermont-Ferrand 2 (UBP), ANR-11-LABX-0025,PERSYVAL-lab,Systemes et Algorithmes Pervasifs au confluent des mondes physique et numérique(2011), and Université Blaise Pascal - Clermont-Ferrand 2 (UBP)-Université d'Auvergne - Clermont-Ferrand I (UdA)-SIGMA Clermont (SIGMA Clermont)-Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Centre National de la Recherche Scientifique (CNRS)
Subjects: Authentication, Otway–Rees protocol, business.industry, Computer science, 02 engineering and technology, Cryptographic protocol, Stuxnet, Computer security, computer.software_genre, [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL], [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], SCADA, 020204 information systems, 0202 electrical engineering, electronic engineering, information engineering, 020201 artificial intelligence & image processing, The Internet, Message authentication code, [INFO.INFO-ES]Computer Science [cs]/Embedded Systems, business, Formal verification, computer, Computer network
Abstract: International audience; Industrial systems are publicly the target of cyberattacks since Stuxnet [1]. 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.
Published: 2016
Full Text: View/download PDF

273. k-Times Full Traceable Ring Signature

Author: Pascal Lafourcade, Xavier Bultel, Université Clermont Auvergne [2017-2020] (UCA [2017-2020]), Laboratoire d'Informatique, de Modélisation et d'Optimisation des Systèmes (LIMOS), Ecole Nationale Supérieure des Mines de St Etienne-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])-Centre National de la Recherche Scientifique (CNRS), and Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])-Centre National de la Recherche Scientifique (CNRS)
Subjects: Ring (mathematics), Theoretical computer science, Computer science, Group (mathematics), 020206 networking & telecommunications, 0102 computer and information sciences, 02 engineering and technology, Construct (python library), Computer security model, Computer security, computer.software_genre, 01 natural sciences, Signature (logic), Random oracle, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Ring signature, 010201 computation theory & mathematics, 0202 electrical engineering, electronic engineering, information engineering, computer, TRACE (psycholinguistics)
Abstract: International audience; —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.
Published: 2016
Full Text: View/download PDF

274. History-based MAC Protocol for Low Duty-Cycle Wireless Sensor Networks: the SLACK-MAC Protocol

Author: Alexandre Guitton, Affoua Therese Aby, Michel Misson, Pascal Lafourcade, Laboratoire d'Informatique, de Modélisation et d'optimisation des Systèmes (LIMOS), SIGMA Clermont (SIGMA Clermont)-Université d'Auvergne - Clermont-Ferrand I (UdA)-Ecole Nationale Supérieure des Mines de St Etienne-Centre National de la Recherche Scientifique (CNRS)-Université Blaise Pascal - Clermont-Ferrand 2 (UBP), Université Clermont Auvergne [2017-2020] (UCA [2017-2020]), ANR-16-IDEX-0001,CAP 20-25,CAP 20-25 (I-Site)(2016), Guitton, Alexandre, CAP 20-25 - - CAP 20-252016 - ANR-16-IDEX-0001 - IDEX - VALID, Université Blaise Pascal - Clermont-Ferrand 2 (UBP)-Université d'Auvergne - Clermont-Ferrand I (UdA)-SIGMA Clermont (SIGMA Clermont)-Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Centre National de la Recherche Scientifique (CNRS), and ANR-16-IDEX-0001,CAP 20-25,CAP 20-25(2016)
Subjects: Internet Protocol Control Protocol, Computer science, computer.internet_protocol, 02 engineering and technology, lcsh:Telecommunication, asynchronous MAC protocol, [INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI], lcsh:TK5101-6720, 0502 economics and business, 0202 electrical engineering, electronic engineering, information engineering, Protocol (science), [INFO.INFO-NI] Computer Science [cs]/Networking and Internet Architecture [cs.NI], business.industry, Link Control Protocol, 05 social sciences, Frame (networking), ComputerSystemsOrganization_COMPUTER-COMMUNICATIONNETWORKS, adaptive, 020206 networking & telecommunications, WSN, Asynchronous communication, Internetwork protocol, 050211 marketing, duty-cycle, business, Wireless sensor network, computer, Reverse Address Resolution Protocol, Computer network
Abstract: International audience; Wireless sensor networks (WSNs) are increasingly used in environmental monitoring applications. They are designed to operate for several months by featuring low activity cycles in order to save energy. In this paper, we propose a Medium Access Control (MAC) protocol for such WSNs with very low duty-cycles of 1% and less. Nodes are activated randomly and use a history of previous successful frame exchanges to decide their next activation time. We study the choice of the history size, and we compare the performance of our protocol with other protocols from the literature. We show by simulations and real experiments that with a limited history size of only six entries, our protocol achieves better performance than other protocols from the literature, while keeping the advantages of fully asynchronous protocols.
Published: 2016

275. On the existence and decidability of unique decompositions of processes in the applied π-calculus

Author: Yassine Lakhnech, Pascal Lafourcade, Jannik Dreier, Cristian Ene, Combination of approaches to the security of infinite states systems (CASSIS), Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174) (FEMTO-ST), Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Centre National de la Recherche Scientifique (CNRS)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Centre National de la Recherche Scientifique (CNRS)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), VERIMAG (VERIMAG - IMAG), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019]), Laboratoire d'Informatique, de Modélisation et d'optimisation des Systèmes (LIMOS), Université Blaise Pascal - Clermont-Ferrand 2 (UBP)-Université d'Auvergne - Clermont-Ferrand I (UdA)-SIGMA Clermont (SIGMA Clermont)-Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Centre National de la Recherche Scientifique (CNRS), ANR-10-VERS-0004,ProSe,Protocoles de sécurité : modèle formel, modèle calculatoire et implémentations(2010), Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Centre National de la Recherche Scientifique (CNRS)-Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL), and SIGMA Clermont (SIGMA Clermont)-Université d'Auvergne - Clermont-Ferrand I (UdA)-Ecole Nationale Supérieure des Mines de St Etienne-Centre National de la Recherche Scientifique (CNRS)-Université Blaise Pascal - Clermont-Ferrand 2 (UBP)
Subjects: Behavioural Equivalence, General Computer Science, Process calculus, 0102 computer and information sciences, 02 engineering and technology, Decidability, 01 natural sciences, Theoretical Computer Science, Equational Theory, Process Calculus, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Weak Bisimilarity, Prime factor, 0202 electrical engineering, electronic engineering, information engineering, Equational theory, Mathematics, Discrete mathematics, Cancellation, Word Problem, Undecidable problem, Applied π-Calculus, 010201 computation theory & mathematics, Pi calculus, Unique Decomposition, A-normal form, Normal Form, 020201 artificial intelligence & image processing, Word problem (mathematics), Strong Bisimilarity, Computer Science::Formal Languages and Automata Theory
Abstract: International audience; Unique decomposition has been a subject of interest in process algebra for a long time (for example in BPP [1] or CCS [2, 3]), as it provides a normal form and useful cancellation properties. We provide two parallel decomposition results for subsets of the applied π-calculus: we show that every closed normed (i.e. with a finite shortest complete trace) process P can be decomposed uniquely into prime factors P i with respect to strong labeled bisimilarity, i.e. such that P ∼ l P_1 | ... | P_n. Moreover, we prove that closed finite processes can be decomposed uniquely with respect to weak labeled bisimilarity. We also investigate whether efficient algorithms that compute the unique decompositions exist. The simpler problem of deciding whether a process is in its unique decomposition form is undecidable in general in both cases, due to potentially undecidable equational theories. Moreover, we show that the unique decomposition remains undecidable even given an equational theory with a decidable word problem.
Published: 2016
Full Text: View/download PDF

276. Two Secure Anonymous Proxy-based Data Storages

Author: Pascal Lafourcade, Xavier Bultel, Olivier Blazy, Mathématiques & Sécurité de l'information (XLIM-MATHIS), XLIM (XLIM), Université de Limoges (UNILIM)-Centre National de la Recherche Scientifique (CNRS)-Université de Limoges (UNILIM)-Centre National de la Recherche Scientifique (CNRS), Laboratoire d'Informatique, de Modélisation et d'optimisation des Systèmes (LIMOS), SIGMA Clermont (SIGMA Clermont)-Université d'Auvergne - Clermont-Ferrand I (UdA)-Ecole Nationale Supérieure des Mines de St Etienne-Centre National de la Recherche Scientifique (CNRS)-Université Blaise Pascal - Clermont-Ferrand 2 (UBP), ANR-16-IDEX-0001,CAP 20-25,CAP 20-25(2016), and Université Blaise Pascal - Clermont-Ferrand 2 (UBP)-Université d'Auvergne - Clermont-Ferrand I (UdA)-SIGMA Clermont (SIGMA Clermont)-Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Centre National de la Recherche Scientifique (CNRS)
Subjects: 021110 strategic, defence & security studies, business.industry, Computer science, standard model, Reverse proxy, 0211 other engineering and technologies, proxy, 02 engineering and technology, Computer security, computer.software_genre, Encryption, public key cryptography, Public-key cryptography, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Anonymous storage, Computer data storage, 0202 electrical engineering, electronic engineering, information engineering, 020201 artificial intelligence & image processing, Economic model, Proxy (statistics), business, computer
Abstract: Unidirectional proxy re-encryption (PRE) can be used to realize an efficient and secure shared storage. However, this type of storage does not yet protect its users' privacy: to retrieve some data a user must give his identity and his query to the proxy. We propose two secure data storage systems that allow authorized users to anonymously get access to the content of encrypted data on a storage. Each scheme corresponds to a certain economic model. In the first one, a user has to pay for each downloaded file, whereas in the second one, users pay each month a subscription to get an unlimited access to all their files.
Published: 2016
Full Text: View/download PDF

277. Formal Analysis of Key Management in mobile Wimax

Author: Noudjoud Kahya, Nacira Ghoualmi, pascal lafourcade, Roumaissa Khelf, Lafourcade, Pascal, CAP 20-25 - - CAP 20-252016 - ANR-16-IDEX-0001 - IDEX - VALID, Laboratoire d'Informatique, de Modélisation et d'Optimisation des Systèmes (LIMOS), Ecole Nationale Supérieure des Mines de St Etienne-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])-Centre National de la Recherche Scientifique (CNRS), ANR-16-IDEX-0001,CAP 20-25,CAP 20-25 (I-Site)(2016), Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])-Centre National de la Recherche Scientifique (CNRS), and ANR-16-IDEX-0001,CAP 20-25,CAP 20-25(2016)
Subjects: [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], mobile Wimax, TEK, ComputerSystemsOrganization_COMPUTER-COMMUNICATIONNETWORKS, attack, analyze formal, PKM, [INFO.INFO-CR] Computer Science [cs]/Cryptography and Security [cs.CR]
Abstract: International audience; The Mobile WiMAX IEEE 802.16e is a new technology supporting broadband wireless communication with fixed and mobile access. The standard offers high throughput broadband connections, supporting handover and roaming capabilities, and provides a security sub layer, which is responsible for secrecy, authentication and secure key exchange. In the area of security aspects, Mobile WiMAX exhibits vulnerabilities while adopting improved security architecture. Several versions of 802.16 networks were released. While the first versions have shown some security weaknesses that were later corrected by the recently released versions, the security mechanisms of 802.16 still remain vulnerable and the limited deployment of such technology is insufficient to satisfy the demands of security. This paper focuses on reducing the security vulnerabilities in the authorization protocol PKM and the generation of traffic encryption keys (TEKs). We propose the usage of 1. A formal analysis of the PKM protocol (authorization phase and exchange of TEKs phase) and 2.Device certificate for key exchange process to provide secure authentication and 3. Give a formal analysis of our new PKM protocol (authorization phase and exchange of TEKs phase). The formal analysis has been conducted using a specialized model checker Scyther, which provides formal proofs of the security protocol. The revised authentication protocol is expected to provide better secure platform for all process of PKM.
Published: 2016

278. Automated Verification of e-Cash Protocols

Author: Ali Kassem, Jannik Dreier, Pascal Lafourcade, Proof techniques for security protocols (PESTO), Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), VERIMAG (VERIMAG - IMAG), Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Grenoble (INPG)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Université Joseph Fourier - Grenoble 1 (UJF), Laboratoire d'Informatique, de Modélisation et d'Optimisation des Systèmes (LIMOS), Ecole Nationale Supérieure des Mines de St Etienne-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])-Centre National de la Recherche Scientifique (CNRS), ANR-16-IDEX-0001,CAP 20-25,CAP 20-25(2016), Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS), Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])-Centre National de la Recherche Scientifique (CNRS), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), and Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)
Subjects: Computer science, media_common.quotation_subject, Electronic cash, Double spending, 02 engineering and technology, E-Cash, Computer security, computer.software_genre, Intelligent verification, Double Spending, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], ProVerif, 0202 electrical engineering, electronic engineering, information engineering, Formal Verification, Formal verification, media_common, Protocol (science), Security properties, ComputingMilieux_THECOMPUTINGPROFESSION, 020206 networking & telecommunications, Applied π-Calculus, ComputingMilieux_MANAGEMENTOFCOMPUTINGANDINFORMATIONSYSTEMS, Exculpability, Privacy, Cash, ComputingMilieux_COMPUTERSANDSOCIETY, 020201 artificial intelligence & image processing, computer, Anonymity
Abstract: International audience; Electronic cash (e-cash) permits secure e-payments by providing security and anonymity similar to real cash. Several protocols have been proposed to meet security and anonymity properties of e-cash. However , there are no general formal definitions that allow the automatic verification of e-cash protocols. In this paper, we propose a formal framework to define and verify security properties of e-cash protocols. To this end, we model e-cash protocols in the applied π-calculus, and we formally define five relevant security properties. Finally, we validate our framework by analyzing, using the automatic tool ProVerif, four e-cash protocols: the online and the offline Chaum protocols, the Digicash protocol, and the protocol by Petersen and Poupard.
Published: 2016
Full Text: View/download PDF

279. Automated Proofs for Asymmetric Encryption

Author: Cristian Ene, Pascal Lafourcade, Marion Daubignard, Joudicaël Courant, Yassine Lakhnech, VERIMAG (VERIMAG - IMAG), Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Grenoble (INPG)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Université Joseph Fourier - Grenoble 1 (UJF), and Lafourcade, Pascal
Subjects: Theoretical computer science, Plaintext-aware encryption, Computer science, 0102 computer and information sciences, 02 engineering and technology, Computer security, computer.software_genre, Encryption, 01 natural sciences, 03 medical and health sciences, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Multiple encryption, Artificial Intelligence, 0202 electrical engineering, electronic engineering, information engineering, Optimal asymmetric encryption padding, [INFO.INFO-CR] Computer Science [cs]/Cryptography and Security [cs.CR], 030304 developmental biology, 0303 health sciences, business.industry, 020206 networking & telecommunications, Deterministic encryption, Computational Theory and Mathematics, 010201 computation theory & mathematics, Probabilistic encryption, 56-bit encryption, 40-bit encryption, business, computer, Software
Abstract: International audience; 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 cryp-tosystems 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.
Published: 2010
Full Text: View/download PDF

280. Survey of Distance Bounding Protocols and Threats

Author: Pascal Lafourcade, Agnès Brelurut, David Gerault, Laboratoire d'Informatique, de Modélisation et d'optimisation des Systèmes (LIMOS), Université Blaise Pascal - Clermont-Ferrand 2 (UBP)-Université d'Auvergne - Clermont-Ferrand I (UdA)-Sigma CLERMONT (Sigma CLERMONT)-Centre National de la Recherche Scientifique (CNRS)-Ecole Nationale Supérieure des Mines de St Etienne, Université Clermont Auvergne (UCA), ANR: 16-IDEX-0001,CAP 20-25,CAP 20-25 (I-Site)(2017), Université Blaise Pascal - Clermont-Ferrand 2 (UBP)-Université d'Auvergne - Clermont-Ferrand I (UdA)-SIGMA Clermont (SIGMA Clermont)-Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Centre National de la Recherche Scientifique (CNRS), Université Clermont Auvergne [2017-2020] (UCA [2017-2020]), ANR-16-IDEX-0001,CAP 20-25,CAP 20-25(2016), SIGMA Clermont (SIGMA Clermont)-Université d'Auvergne - Clermont-Ferrand I (UdA)-Ecole Nationale Supérieure des Mines de St Etienne-Centre National de la Recherche Scientifique (CNRS)-Université Blaise Pascal - Clermont-Ferrand 2 (UBP), and ANR-16-IDEX-0001,CAP 20-25,CAP 20-25 (I-Site)(2016)
Subjects: Engineering, NFC, Context (language use), 02 engineering and technology, Computer security, computer.software_genre, Relay attack, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Bounding overwatch, 0502 economics and business, Collusion Fraud, 0202 electrical engineering, electronic engineering, information engineering, Relay Attack, Wireless, Mafia Fraud, Threat Models, RFID, business.industry, 05 social sciences, Distance fraud, 020206 networking & telecommunications, Terrorist Fraud, 16. Peace & justice, Distance Bounding, Mount, Distance Fraud, Threat model, Terrorism, 050211 marketing, business, computer
Abstract: International audience; NFC and RFID are technologies that are more and more present in our life. These technologies allow a tag to communicate without contact with a reader. In wireless communication an intruder can always listen and forward a signal, so he can mount a so-called worm hole attack. In the last decades, several Distance Bounding (DB) protocols have been introduced to avoid such attacks. In this context, there exist several threat models: Terrorist Fraud, Mafia Fraud, Distance Fraud etc. We first show the links between the existing threat models. Then we list more than forty DB protocols and give the bounds of the best known attacks for different threat models. In some cases, we explain how we are able to improve existing attacks. Then, we present some advices to the designers of the DB protocols and to the intruders to mount some attacks.
Published: 2015
Full Text: View/download PDF

281. Performance Evaluations of Cryptographic Protocols Verification Tools Dealing with Algebraic Properties

Author: Pascal Lafourcade, Maxime Puys, Laboratoire d'Informatique, de Modélisation et d'optimisation des Systèmes (LIMOS), Université Blaise Pascal - Clermont-Ferrand 2 (UBP)-Université d'Auvergne - Clermont-Ferrand I (UdA)-SIGMA Clermont (SIGMA Clermont)-Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Centre National de la Recherche Scientifique (CNRS), VERIMAG (VERIMAG - IMAG), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019]), This research was conducted with the support of the 'Digital trust' Chair from theUniversity of Auvergne Foundation.This work has been partially supported by the LabEx PERSYVAL-Lab (ANR–11-LABX-0025)., ANR-11-LABX-0025,PERSYVAL-lab,Systemes et Algorithmes Pervasifs au confluent des mondes physique et numérique(2011), ANR-16-IDEX-0001,CAP 20-25,CAP 20-25(2016), and SIGMA Clermont (SIGMA Clermont)-Université d'Auvergne - Clermont-Ferrand I (UdA)-Ecole Nationale Supérieure des Mines de St Etienne-Centre National de la Recherche Scientifique (CNRS)-Université Blaise Pascal - Clermont-Ferrand 2 (UBP)
Subjects: Algebraic properties, Protocol (science), 021110 strategic, defence & security studies, Cryptographic primitive, Exponentiation, Theoretical computer science, Selection (relational algebra), Computer science, 05 social sciences, 0211 other engineering and technologies, 02 engineering and technology, Benchmarking, Construct (python library), Cryptographic protocol, Verification Tools for Cryptographic Protocols, 050601 international relations, [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL], 0506 political science, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], [INFO.INFO-ES]Computer Science [cs]/Embedded Systems, Performances' Evaluations, Algebraic Properties
Abstract: International audience; There exist several automatic verification tools of cryptographic protocols, but only few of them are able to check protocols in presence of algebraic properties. Most of these tools are dealing either with Exclusive-Or (XOR) and exponentiation properties, so-called Diffie-Hellman (DH). In the last few years, the number of these tools increased and some existing tools have been updated. Our aim is to compare their performances by analysing a selection of cryptographic protocols using XOR and DH. We compare execution time and memory consumption for different versions of the following tools OFMC, CL-Atse, Scyther, Tamarin, TA4SP, and extensions of ProVerif (XOR-ProVerif and DH-ProVerif). Our evaluation shows that in most of the cases the new versions of the tools are faster but consume more memory. We also show how the new tools: Tamarin, Scyther and TA4SP, can be compared to previous ones. We also discover and understand for the protocol IKEv2-DS a difference of modelling by the authors of different tools, which leads to different security results. Finally, for Exclusive-Or and Diffie-Hellman properties, we construct two families of protocols P xori and P dhi that allow us to clearly see for the first time the impact of the number of operators and variables in the tools' performances.
Published: 2015
Full Text: View/download PDF

282. Monitoring Electronic Exams

Author: Ali Kassem, Pascal Lafourcade, Yliès Falcone, VERIMAG (VERIMAG - IMAG), Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Grenoble (INPG)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Université Joseph Fourier - Grenoble 1 (UJF), Compiler Optimization and Run-time Systems (CORSE), Inria Grenoble - Rhône-Alpes, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire d'Informatique de Grenoble (LIG), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF), Laboratoire d'Informatique de Grenoble (LIG), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF), Université Grenoble Alpes [2016-2019] (UGA [2016-2019]), Laboratoire d'Informatique, de Modélisation et d'optimisation des Systèmes (LIMOS), SIGMA Clermont (SIGMA Clermont)-Université d'Auvergne - Clermont-Ferrand I (UdA)-Ecole Nationale Supérieure des Mines de St Etienne-Centre National de la Recherche Scientifique (CNRS)-Université Blaise Pascal - Clermont-Ferrand 2 (UBP), ANR-16-IDEX-0001,CAP 20-25,CAP 20-25(2016), Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS), Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS), Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS), and Université Blaise Pascal - Clermont-Ferrand 2 (UBP)-Université d'Auvergne - Clermont-Ferrand I (UdA)-SIGMA Clermont (SIGMA Clermont)-Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Centre National de la Recherche Scientifique (CNRS)
Subjects: Java, ComputingMilieux_THECOMPUTINGPROFESSION, Event (computing), business.industry, Computer science, [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE], Automaton, Linear temporal logic, ComputingMilieux_COMPUTERSANDEDUCATION, [INFO.INFO-ES]Computer Science [cs]/Embedded Systems, Software engineering, business, computer, Simulation, computer.programming_language
Abstract: International audience; Universities and other educational organizations are adopting computer based assessment tools (herein called e-exams) to reach larger and ubiquitous audiences. While this makes examination tests more accessible, it exposes them to unprecedented threats not only from candidates but also from authorities , which organize exams and deliver marks. Thus, e-exams must be checked to detect potential irregularities. In this paper, we propose several monitors, expressed as Quantified Event Automata (QEA), to monitor the main properties of e-exams. Then, we implement the monitors using MarQ, a recent Java tool designed to support QEAs. Finally, we apply our monitors to logged data from real e-exams conducted by Université Joseph Fourier at pharmacy faculty, as a part of Epreuves Classantes Nationales informatisées , a pioneering project which aims to realize all french medicine exams electronically by 2016. Our monitors found discrepancies between the specification and the implementation.
Published: 2015
Full Text: View/download PDF

283. Key Management inWireless Sensor Networks

Author: Gerard Chalhoub, Pascal Lafourcade, Ismail Mansour, Laboratoire d'Informatique, de Modélisation et d'optimisation des Systèmes (LIMOS), Université Blaise Pascal - Clermont-Ferrand 2 (UBP)-Université d'Auvergne - Clermont-Ferrand I (UdA)-SIGMA Clermont (SIGMA Clermont)-Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Centre National de la Recherche Scientifique (CNRS), and SIGMA Clermont (SIGMA Clermont)-Université d'Auvergne - Clermont-Ferrand I (UdA)-Ecole Nationale Supérieure des Mines de St Etienne-Centre National de la Recherche Scientifique (CNRS)-Université Blaise Pascal - Clermont-Ferrand 2 (UBP)
Subjects: Control and Optimization, Computer Networks and Communications, Computer science, Cryptography, security, lcsh:Technology, multihop, [INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI], wireless sensor network, formal proof, Mobile wireless sensor network, Elliptic curve cryptography, Key management, Instrumentation, business.industry, lcsh:T, ComputerSystemsOrganization_COMPUTER-COMMUNICATIONNETWORKS, Cryptographic protocol, revocation, Key distribution in wireless sensor networks, Symmetric-key algorithm, renewing, authentication, business, verification, Wireless sensor network, Computer network
Abstract: International audience; Wireless sensor networks are a challenging field of research when it comes to security issues. Using low cost sensor nodes with limited resources makes it difficult for cryptographic algorithms to function without impacting energy consumption and latency. In this paper, we focus on key management issues in multi-hop wireless sensor networks. These networks are easy to attack due to the open nature of the wireless medium. Intruders could try to penetrate the network, capture nodes or take control over particular nodes. In this context, it is important to revoke and renew keys that might be learned by malicious nodes. We propose several secure protocols for key revocation and key renewal based on symmetric encryption and elliptic curve cryptography. All protocols are secure, but have different security levels. Each proposed protocol is formally proven and analyzed using Scyther, an automatic verification tool for cryptographic protocols. For efficiency comparison sake, we implemented all protocols on real testbeds using TelosB motes and discussed their performances.
Published: 2015
Full Text: View/download PDF

284. Formal Analysis of E-Cash Protocols

Author: Pascal Lafourcade, Jannik Dreier, Ali Kassem, Combination of approaches to the security of infinite states systems (CASSIS), Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174) (FEMTO-ST), Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Centre National de la Recherche Scientifique (CNRS)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Centre National de la Recherche Scientifique (CNRS)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), VERIMAG (VERIMAG - IMAG), Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS), Laboratoire d'Informatique, de Modélisation et d'optimisation des Systèmes (LIMOS), Université Blaise Pascal - Clermont-Ferrand 2 (UBP)-Université d'Auvergne - Clermont-Ferrand I (UdA)-SIGMA Clermont (SIGMA Clermont)-Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Centre National de la Recherche Scientifique (CNRS), Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Centre National de la Recherche Scientifique (CNRS)-Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Grenoble (INPG)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Université Joseph Fourier - Grenoble 1 (UJF), SIGMA Clermont (SIGMA Clermont)-Université d'Auvergne - Clermont-Ferrand I (UdA)-Ecole Nationale Supérieure des Mines de St Etienne-Centre National de la Recherche Scientifique (CNRS)-Université Blaise Pascal - Clermont-Ferrand 2 (UBP), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), and Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)
Subjects: Computer science, media_common.quotation_subject, Electronic cash, Double spending, 02 engineering and technology, E-Cash, Computer security, computer.software_genre, Double Spending, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Formal Analysis, 0202 electrical engineering, electronic engineering, information engineering, ProVerif, media_common, Security properties, Protocol (science), 020206 networking & telecommunications, Cryptographic protocol, Payment, Applied π-Calculus, ComputingMilieux_MANAGEMENTOFCOMPUTINGANDINFORMATIONSYSTEMS, Exculpability, Privacy, Cash, ComputingMilieux_COMPUTERSANDSOCIETY, 020201 artificial intelligence & image processing, computer
Abstract: International audience; Electronic cash (e-cash) aims at achieving client privacy at payment, similar to real cash. Several security protocols have been proposed to ensure privacy in e-cash, as well as the necessary unforgery properties. In this paper, we propose a formal framework to define, analyze, and verify security properties of e-cash systems. To this end, we model e-cash systems in the applied π-calculus, and we define two client privacy properties and three properties to prevent forgery. Finally, we apply our definitions to an e-cash protocol from the literature proposed by Chaum et al., which has two variants and a real implementation based on it. Using ProVerif, we demonstrate that our framework is suitable for an automated analysis of this protocol.
Published: 2015
Full Text: View/download PDF

285. Architectures PKI et communications sécurisées

Author: Jean-Guillaume Dumas, Pascal Lafourcade, Patrick Redon, Calculs Algébriques et Systèmes Dynamiques (CASYS), Laboratoire Jean Kuntzmann (LJK), Centre National de la Recherche Scientifique (CNRS)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Université Joseph Fourier - Grenoble 1 (UJF)-Université Pierre Mendès France - Grenoble 2 (UPMF)-Centre National de la Recherche Scientifique (CNRS)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Université Joseph Fourier - Grenoble 1 (UJF)-Université Pierre Mendès France - Grenoble 2 (UPMF), Laboratoire d'Informatique, de Modélisation et d'optimisation des Systèmes (LIMOS), SIGMA Clermont (SIGMA Clermont)-Université d'Auvergne - Clermont-Ferrand I (UdA)-Ecole Nationale Supérieure des Mines de St Etienne-Centre National de la Recherche Scientifique (CNRS)-Université Blaise Pascal - Clermont-Ferrand 2 (UBP), ANR-11-LABX-0025,PERSYVAL-lab,Systemes et Algorithmes Pervasifs au confluent des mondes physique et numérique(2011), ANR-16-IDEX-0001,CAP 20-25,CAP 20-25(2016), Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS), and Université Blaise Pascal - Clermont-Ferrand 2 (UBP)-Université d'Auvergne - Clermont-Ferrand I (UdA)-SIGMA Clermont (SIGMA Clermont)-Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Centre National de la Recherche Scientifique (CNRS)
Subjects: [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], [INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI], transactions électroniques, sécurité, Infrastructures à clefs publiques
Abstract: National audience; Cet ouvrage s’adresse aux étudiants de master (mathématiques appliquées, informatique…), aux élèves-ingénieurs, aux enseignants-chercheurs et ingénieurs en sécurité numérique.Son objectif est de fournir une approche compréhensible des techniques, technologies et enjeux liés aux infrastructures de gestion de clefs publiques (PKI, Public Key Infrastructure).L’originalité de cet ouvrage est de présenter les principes mathématiques et informatiques qui fondent les PKI, mais aussi de donner une approche pratique de leur déploiement : il présente les dernières recommandations nationales (RGS) eteuropéennes (e-IDAS) ainsi que de nombreuses applications, comme la gestion de la sécurité des navigateurs Internet et des systèmes d’exploitation ou encore de la monnaie électronique Bitcoin.L’accent est mis sur une présentation détaillée et approfondie, alliant fondements théoriques, protocoles cryptographiques en vigueur et standards les plus récents.Cet ouvrage comporte également plus de 50 exercices corrigés originaux.
Published: 2015

286. Les émulateurs pédagogiques: une source d’innovations qui se construit à l’Université Joseph Fourier de Grenoble

Author: Christian Hoffmann, Anne Briançon-Marjollet, Philippe Brulard, Jean-Luc Cracowski, Julien Douady, Myriam Houssay-Holzschuch, pascal lafourcade, Isabelle Le Brun, Signe Seidelin, Sophie Térouanne, Hélium : du fondamental aux applications (HELFA), Institut Néel (NEEL), Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS), Education, Cultures et Politiques (ECP), Université Lumière - Lyon 2 (UL2)-Université Jean Monnet [Saint-Étienne] (UJM), Hypoxie : Physiopathologie Respiratoire et Cardiovasculaire (HP2), Université Joseph Fourier - Grenoble 1 (UJF)-Institut National de la Santé et de la Recherche Médicale (INSERM), Université Joseph Fourier - Grenoble 1 (UJF), Laboratoire Interdisciplinaire de Physique [Saint Martin d’Hères] (LIPhy), Université Joseph Fourier - Grenoble 1 (UJF)-Centre National de la Recherche Scientifique (CNRS), Pacte, Laboratoire de sciences sociales (PACTE), Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF)-Sciences Po Grenoble - Institut d'études politiques de Grenoble (IEPG)-Centre National de la Recherche Scientifique (CNRS), Université Grenoble Alpes [2016-2019] (UGA [2016-2019]), Grenoble Institut des Neurosciences (GIN), and Nano-Optique et Forces (NOF)
Subjects: valeurs, accompagnement, Enseignants, [SHS.EDU]Humanities and Social Sciences/Education, identité, innovation
Abstract: International audience; Nous décrivons et analysons dans cette communication le fonctionnement d’un groupe d’enseignants et d’enseignants-chercheurs qui contribue au développement professionnel de chacun de ses membres d’une part, et qui devient une source durable d’innovations pédagogiques dans notre établissement d’autre part.
Published: 2015

287. Comment s'exercer à apprendre ?

Author: pascal lafourcade, Isabelle Le Brun, Laboratoire d'Informatique, de Modélisation et d'Optimisation des Systèmes (LIMOS), Ecole Nationale Supérieure des Mines de St Etienne-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])-Centre National de la Recherche Scientifique (CNRS), ANR-16-IDEX-0001,CAP 20-25,CAP 20-25 (I-Site)(2016), Lafourcade, Pascal, CAP 20-25 - - CAP 20-252016 - ANR-16-IDEX-0001 - IDEX - VALID, Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])-Centre National de la Recherche Scientifique (CNRS), and ANR-16-IDEX-0001,CAP 20-25,CAP 20-25(2016)
Subjects: [SCCO.NEUR]Cognitive science/Neuroscience, [SCCO.NEUR] Cognitive science/Neuroscience, [SCCO.PSYC] Cognitive science/Psychology, [SCCO.PSYC]Cognitive science/Psychology, ComputingMilieux_MISCELLANEOUS
Abstract: International audience
Published: 2015

288. A Framework for Analyzing Verifiability in Traditional and Electronic Exams

Author: Ali Kassem, Pascal Lafourcade, Gabriele Lenzini, Rosario Giustolisi, Jannik Dreier, Eidgenössische Technische Hochschule - Swiss Federal Institute of Technology [Zürich] (ETH Zürich), University of Luxembourg [Luxembourg], VERIMAG (VERIMAG - IMAG), Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Grenoble (INPG)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Université Joseph Fourier - Grenoble 1 (UJF), Laboratoire d'Informatique, de Modélisation et d'optimisation des Systèmes (LIMOS), SIGMA Clermont (SIGMA Clermont)-Université d'Auvergne - Clermont-Ferrand I (UdA)-Ecole Nationale Supérieure des Mines de St Etienne-Centre National de la Recherche Scientifique (CNRS)-Université Blaise Pascal - Clermont-Ferrand 2 (UBP), Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS), and Université Blaise Pascal - Clermont-Ferrand 2 (UBP)-Université d'Auvergne - Clermont-Ferrand I (UdA)-SIGMA Clermont (SIGMA Clermont)-Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Centre National de la Recherche Scientifique (CNRS)
Subjects: Computer science [C05] [Engineering, computing & technology], ComputingMilieux_THECOMPUTINGPROFESSION, Computer science, 4. Education, Massive open online course, ComputingMilieux_LEGALASPECTSOFCOMPUTING, Cryptographic protocol, Sciences informatiques [C05] [Ingénierie, informatique & technologie], Computer security, computer.software_genre, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Trustworthiness, ComputingMilieux_COMPUTERSANDEDUCATION, Verifiable secret sharing, Set (psychology), computer, Meaning (linguistics)
Abstract: International audience; The main concern for institutions that organize exams is to detect when students cheat. Actually more frauds are possible and even authorities can be dishonest. If institutions wish to keep exams a trustworthy business, anyone and not only the authorities should be allowed to look into an exam's records and verify the presence or the absence of frauds. In short, exams should be verifiable. However, what verifiability means for exams is unclear and no tool to analyze an exam's verifiability is available. In this paper we address both issues: we formalize several individual and universal verifiability properties for traditional and electronic exams, so proposing a set of verifiability properties and clarifying their meaning, then we implement our framework in ProVerif, so making it a tool to analyze exam verifiability. We validate our framework by analyzing the verifiability of two existing exam systems – an electronic and a paper-and-pencil system.
Published: 2015
Full Text: View/download PDF

289. Formal Security Analysis of Traditional and Electronic Exams

Author: Jannik Dreier, Ali Kassem, Rosario Giustolisi, Pascal Lafourcade, Gabriele Lenzini, and Peter Y. A. Ryan
Subjects: Security analysis, ComputingMilieux_THECOMPUTINGPROFESSION, business.industry, Process (engineering), Computer science, 4. Education, Cheating, media_common.quotation_subject, Internet privacy, 020206 networking & telecommunications, 02 engineering and technology, Computer security, computer.software_genre, Authentication (law), 020204 information systems, Honesty, ComputingMilieux_COMPUTERSANDEDUCATION, 0202 electrical engineering, electronic engineering, information engineering, The Internet, business, computer, Formal verification, Formal description, media_common
Abstract: Nowadays, students can be assessed not only by means of pencil-and-paper tests, but also by electronic exams which they take in examination centers or even from home. Electronic exams are appealing as they can reach larger audiences, but they are exposed to new threats that can potentially ruin the whole exam business. These threats are amplified by two issues: the lack of understanding of what security means for electronic exams (except the old concern about students cheating), and the absence of tools to verify whether an exam process is secure. This paper addresses both issues by introducing a formal description of several fundamental authentication and privacy properties, and by establishing the first theoretical framework for an automatic analysis of exam security. It uses the applied \(\pi \)-calculus as a framework and ProVerif as a tool. Three exam protocols are checked in depth: two Internet exam protocols of recent design, and the pencil-and-paper exam used by the University of Grenoble. The analysis highlights several weaknesses. Some invalidate authentication and privacy even when all parties are honest; others show that security depends on the honesty of parties, an often unjustified assumption in modern exams.
Published: 2015
Full Text: View/download PDF

290. SLACK-MAC: Adaptive MAC Protocol for Low Duty-Cycle Wireless Sensor Networks

Author: Thérèse Aby, Alexandre Guitton, pascal lafourcade, Michel Misson, Université Clermont Auvergne [2017-2020] (UCA [2017-2020]), Laboratoire d'Informatique, de Modélisation et d'Optimisation des Systèmes (LIMOS), Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])-Centre National de la Recherche Scientifique (CNRS), ANR-16-IDEX-0001,CAP 20-25,CAP 20-25(2016), Ecole Nationale Supérieure des Mines de St Etienne-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])-Centre National de la Recherche Scientifique (CNRS), ANR-16-IDEX-0001,CAP 20-25,CAP 20-25 (I-Site)(2016), Guitton, Alexandre, and CAP 20-25 - - CAP 20-252016 - ANR-16-IDEX-0001 - IDEX - VALID
Subjects: asynchronous MAC protocol, [INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI], [INFO.INFO-NI] Computer Science [cs]/Networking and Internet Architecture [cs.NI], ComputerSystemsOrganization_COMPUTER-COMMUNICATIONNETWORKS, adaptive, duty-cycle, WSN
Abstract: International audience; Wireless sensor networks (WSNs) are increasingly used in environmental monitoring applications. They are designed to operate for several months by featuring low activity cycles, in order to save energy. In this paper, we propose a MAC protocol for such WSNs with duty-cycles of 1%. Initially, nodes are activated randomly and independently, then they use the knowledge of previous successful frame exchanges to compute their next activation times. We study the choice of the history size, and we compare the performance of our protocol with other protocols from the literature. We show that with a limited history size of only six entries, we significantly improve the performance of existing protocols, while keeping the advantages of fully asynchronous protocols.
Published: 2015

291. Physical Zero-Knowledge Proofs for Akari, Takuzu, Kakuro and KenKen

Author: Xavier Bultel and Jannik Dreier and Jean-Guillaume Dumas and Pascal Lafourcade, Bultel, Xavier, Dreier, Jannik, Dumas, Jean-Guillaume, Lafourcade, Pascal, Xavier Bultel and Jannik Dreier and Jean-Guillaume Dumas and Pascal Lafourcade, Bultel, Xavier, Dreier, Jannik, Dumas, Jean-Guillaume, and Lafourcade, Pascal
Abstract: Akari, Takuzu, Kakuro and KenKen are logic games similar to Sudoku. In Akari, a labyrinth on a grid has to be lit by placing lanterns, respecting various constraints. In Takuzu a grid has to be filled with 0's and 1's, while respecting certain constraints. In Kakuro a grid has to be filled with numbers such that the sums per row and column match given values; similarly in KenKen a grid has to be filled with numbers such that in given areas the product, sum, difference or quotient equals a given value. We give physical algorithms to realize zero-knowledge proofs for these games which allow a player to show that he knows a solution without revealing it. These interactive proofs can be realized with simple office material as they only rely on cards and envelopes. Moreover, we formalize our algorithms and prove their security.
Published: 2016
Full Text: View/download PDF

292. Formal Verification of e-Reputation Protocols

Author: Yassine Lakhnech, Pascal Lafourcade, Ali Kassem, VERIMAG (VERIMAG - IMAG), Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS), Laboratoire d'Informatique, de Modélisation et d'Optimisation des Systèmes (LIMOS), Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])-Centre National de la Recherche Scientifique (CNRS), ANR-16-IDEX-0001,CAP 20-25,CAP 20-25(2016), Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Grenoble (INPG)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Université Joseph Fourier - Grenoble 1 (UJF), Ecole Nationale Supérieure des Mines de St Etienne-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])-Centre National de la Recherche Scientifique (CNRS), Lafourcade, Pascal, and CAP 20-25 - - CAP 20-252016 - ANR-16-IDEX-0001 - IDEX - VALID
Subjects: Correctness, Applied Pi-Calculus, Computer science, media_common.quotation_subject, 0211 other engineering and technologies, 02 engineering and technology, Computer security, computer.software_genre, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Formal specification, 0202 electrical engineering, electronic engineering, information engineering, ProVerif, Formal verification, Formal Verification, [INFO.INFO-CR] Computer Science [cs]/Cryptography and Security [cs.CR], media_common, 021110 strategic, defence & security studies, Authentication, 020206 networking & telecommunications, Formal methods, Reputation Protocols, Reputation system, Privacy, ComputingMilieux_COMPUTERSANDSOCIETY, Verifiability, computer, Anonymity, Reputation
Abstract: International audience; Reputation systems are often useful in large online communities in which most of the users are unknown to each others. They are good tools to force the users to act in truthfulness way. However, for reputation systems to work effectively users have to be willing to provide rates. In order to incentivize the users to provide honest rates, a reputation system have to ensure their privacy and anonymity. In the other hand, users are also concerned about verifying the correctness of the reputation score. In the applied pi-calculus, we define a formal framework and several fundamental privacy, authentication, and verifiability properties suitable for the security analysis of e-reputation protocols. As proof of concept, using ProVerif, we analyze a simple additive decentralized reputation protocol proposed to ensure rate privacy if all users are honest.
Published: 2014

293. Secure Multihop Key Establishment Protocols for Wireless Sensor Networks

Author: Gerard Chalhoub, Ismail Mansour, Pascal Lafourcade, Laboratoire d'Informatique, de Modélisation et d'optimisation des Systèmes (LIMOS), SIGMA Clermont (SIGMA Clermont)-Université d'Auvergne - Clermont-Ferrand I (UdA)-Ecole Nationale Supérieure des Mines de St Etienne-Centre National de la Recherche Scientifique (CNRS)-Université Blaise Pascal - Clermont-Ferrand 2 (UBP), Laboratoire d'Informatique, de Modélisation et d'Optimisation des Systèmes (LIMOS), Ecole Nationale Supérieure des Mines de St Etienne-Centre National de la Recherche Scientifique (CNRS)-Université Clermont Auvergne [2017-2020] (UCA [2017-2020]), Lafourcade, Pascal, Université Blaise Pascal - Clermont-Ferrand 2 (UBP)-Université d'Auvergne - Clermont-Ferrand I (UdA)-SIGMA Clermont (SIGMA Clermont)-Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Centre National de la Recherche Scientifique (CNRS), and Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])-Centre National de la Recherche Scientifique (CNRS)
Subjects: Authentication, business.industry, Computer science, Wireless Sensor Net- work, ComputerSystemsOrganization_COMPUTER-COMMUNICATIONNETWORKS, 020206 networking & telecommunications, Context (language use), Cryptography, 02 engineering and technology, key establishment, Key distribution in wireless sensor networks, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Secure communication, 0202 electrical engineering, electronic engineering, information engineering, Security, Overhead (computing), 020201 artificial intelligence & image processing, Elliptic curve cryptography, business, Wireless sensor network, Multihop, Formal Verification, Computer network, [INFO.INFO-CR] Computer Science [cs]/Cryptography and Security [cs.CR]
Abstract: International audience; Designing secure communication protocols is not an easy task. Cryptography is often necessary but does not always guarantee the security of protocols as several famous examples attest in the literature. Moreover, in the context of Wireless Sensor Networks (WSNs) the design is even more difficult due to the limited resources of sensor nodes that add extra constraints to take into account. During the life time of a secure WSN, one of the first crucial steps is the key establishment between two nodes. In this paper we propose four secure multihop key establishment protocols based on elliptic curve cryptography (ECC). For each protocol, we make a formal security proof using the automatic tool Scyther. Then, in order to evaluate their performances, we implemented them on testbeds using TelosB motes and TinyOS. Results allow us to estimate the overhead of our key establishment methods.
Published: 2014

294. A More Realistic Model for Verifying Route Validity in Ad-Hoc Networks

Author: Ali Kassem, Pascal Lafourcade, and Yassine Lakhnech
Subjects: Routing protocol, Protocol (science), Wireless ad hoc network, Computer science, business.industry, Distributed computing, ComputerSystemsOrganization_COMPUTER-COMMUNICATIONNETWORKS, Topology (electrical circuits), Cryptographic protocol, Network topology, Mathematical proof, Path (graph theory), business, Computer network
Abstract: Many cryptographic protocols aim at ensuring the route validity in ad-hoc networks, i.e. the established route representing an exists path in the network . However, flaws have been found in some protocols that are claimed secure (e.g. the attack on SRP applied to DSR). Some formal models and reduction proofs have been proposed to give more guarantees when verifying route validity and facilitate verification process. The existing approaches assume the cooperative attacker model. In this paper, we consider the non-cooperative attacker model, and we show that verifying the route validity under the non-cooperative model requires to verify only five topologies, each containing four nodes, and to consider only three malicious (compromised) nodes. Furthermore, we prove that a protocol is secure for any topology under the non-cooperative model, if and only if, it is secure for any topology under the cooperative model.
Published: 2014
Full Text: View/download PDF

295. Secure Auctions without Cryptography

Author: Pascal Lafourcade, Hugo Jonker, Jannik Dreier, Combination of approaches to the security of infinite states systems (CASSIS), Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174) (FEMTO-ST), Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Centre National de la Recherche Scientifique (CNRS)-Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL), Open Universiteit Nederland [Heerlen], Laboratoire d'Informatique, de Modélisation et d'optimisation des Systèmes (LIMOS), SIGMA Clermont (SIGMA Clermont)-Université d'Auvergne - Clermont-Ferrand I (UdA)-Ecole Nationale Supérieure des Mines de St Etienne-Centre National de la Recherche Scientifique (CNRS)-Université Blaise Pascal - Clermont-Ferrand 2 (UBP), Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Centre National de la Recherche Scientifique (CNRS)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Centre National de la Recherche Scientifique (CNRS)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), and Université Blaise Pascal - Clermont-Ferrand 2 (UBP)-Université d'Auvergne - Clermont-Ferrand I (UdA)-SIGMA Clermont (SIGMA Clermont)-Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Centre National de la Recherche Scientifique (CNRS)
Subjects: TheoryofComputation_MISCELLANEOUS, 021110 strategic, defence & security studies, Cryptographic primitive, SIMPLE (military communications protocol), Computer science, business.industry, 0211 other engineering and technologies, Wooden box, Cryptography, 02 engineering and technology, Cryptographic protocol, Computer security, computer.software_genre, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], 020204 information systems, 0202 electrical engineering, electronic engineering, information engineering, Public verifiability, Common value auction, business, Protocol (object-oriented programming), computer
Abstract: International audience; An auction is a simple way of selling and buying goods. Modern auction protocols often rely on complex cryptographic operations to ensure manifold security properties such as bidder-anonymity or bid-privacy, non-repudiation, fairness or public verifiability of the result. This makes them difficult to understand for users who are not experts in cryptography. We propose two physical auction protocols inspired by Sako’s cryptographic auction protocol. In contrast to Sako’s protocol, they do not rely on cryptographic operations, but on physical properties of the manipulated mechanical objects to ensure the desired security properties. The first protocol only uses standard office material, whereas the second uses a special wooden box. We validate the security of our solutions using ProVerif.
Published: 2014
Full Text: View/download PDF

296. Foundations and Practice of Security : 4th Canada-France MITACS Workshop, FPS 2011, Paris, France, May 12-13, 2011, Revised Selected Papers

Author: Joaquin Garcia-Alfaro, Pascal Lafourcade, Joaquin Garcia-Alfaro, and Pascal Lafourcade
Subjects: Kongress--2011.--Paris, Conference proceedings, Computer security--Congresses, Computer security, Chiffrierung, Chipkarte, Computersicherheit, Datensicherung, Formale Methode, Informationssystem
Abstract: This book constitutes the carefully refereed and revised selected papers of the 4th Canada-France MITACS Workshop on Foundations and Practice of Security, FPS 2011, held in Paris, France, in May 2011. The book contains a revised version of 10 full papers, accompanied by 3 keynote addresses, 2 short papers, and 5 ongoing research reports. The papers were carefully reviewed and selected from 30 submissions. The topics covered are pervasive security and threshold cryptography; encryption, cryptanalysis and automatic verification; and formal methods in network security.
Published: 2012

297. Automated Security Proofs for Almost-Universal Hash for MAC Verification

Author: Pascal Lafourcade, Yassine Lakhnech, Martin Gagné, VERIMAG (VERIMAG - IMAG), Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Grenoble (INPG)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Université Joseph Fourier - Grenoble 1 (UJF), Laboratoire d'Informatique, de Modélisation et d'Optimisation des Systèmes (LIMOS), Ecole Nationale Supérieure des Mines de St Etienne-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])-Centre National de la Recherche Scientifique (CNRS), Lafourcade, Pascal, Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS), and Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])-Centre National de la Recherche Scientifique (CNRS)
Subjects: Computer science, Hash function, Cryptography, 0102 computer and information sciences, Merkle tree, Encryption, 01 natural sciences, Random oracle, Secure Hash Standard, 03 medical and health sciences, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Collision attack, SHA-2, Cryptographic hash function, Message authentication code, Security of cryptographic hash functions, [INFO.INFO-CR] Computer Science [cs]/Cryptography and Security [cs.CR], 030304 developmental biology, Block cipher, Secure Hash Algorithm, 0303 health sciences, business.industry, Pass the hash, PMAC, MDC-2, Hash-based message authentication code, 010201 computation theory & mathematics, Hash chain, business, Computer network
Abstract: International audience; Message authentication codes (MACs) are an essential primitive in cryptography. They are used to ensure the integrity and authenticity of a message, and can also be used as a building block for larger schemes, such as chosen-ciphertext secure encryption, or identity-based encryption. We present a method for automatically proving the security for block-cipher-based and hash-based MACs in the ideal cipher model. Our method proceeds in two steps, following the traditional method for constructing MACs. First, the 'front end' of the MAC produces a short digest of the long message, then the 'back end' provides a mixing step to make the output of the MAC unpredictable for an attacker. We develop a Hoare logic for proving that the front end of the MAC is an almost-universal hash function. The programming language used to specify these functions is quite expressive. As a result, our logic can be used to prove functions based on block ciphers and hash functions. Second, we provide a list of options for the back end of the MAC, each consisting of only two or three instructions, each of which can be composed with an almost-universal hash function to obtain a secure MAC. Using our method, we implemented a tool that can prove the security of many CBC-based MACs (DMAC, ECBC, FCBC and XCBC to name only a few), PMAC and HMAC.
Published: 2013

298. Brandt's Fully Private Auction Protocol Revisited

Author: Pascal Lafourcade, Jean-Guillaume Dumas, Jannik Dreier, Distributed and Complex Systems, VERIMAG (VERIMAG - IMAG), Université Joseph Fourier - Grenoble 1 (UJF)-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA)-Université Joseph Fourier - Grenoble 1 (UJF)-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA), Calculs Algébriques et Systèmes Dynamiques (CASYS), Laboratoire Jean Kuntzmann (LJK), Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF)-Institut Polytechnique de Grenoble - Grenoble Institute of Technology-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA)-Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF)-Institut Polytechnique de Grenoble - Grenoble Institute of Technology-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA), Laboratoire d'Informatique, de Modélisation et d'Optimisation des Systèmes (LIMOS), Ecole Nationale Supérieure des Mines de St Etienne-Université Clermont Auvergne (UCA)-Centre National de la Recherche Scientifique (CNRS), Amr Youssef and Abderrahmane Nitaj and Aboul Ella Hassanien, ANR-11-LABX-0025-01,PERSYVAL-lab,Systèmes et Algorithmes Pervasifs au confluent des mondes physique et numérique(2011), Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Grenoble (INPG)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Université Joseph Fourier - Grenoble 1 (UJF)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Grenoble (INPG)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Université Joseph Fourier - Grenoble 1 (UJF), Centre National de la Recherche Scientifique (CNRS)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Université Joseph Fourier - Grenoble 1 (UJF)-Université Pierre Mendès France - Grenoble 2 (UPMF)-Centre National de la Recherche Scientifique (CNRS)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Université Joseph Fourier - Grenoble 1 (UJF)-Université Pierre Mendès France - Grenoble 2 (UPMF), Ecole Nationale Supérieure des Mines de St Etienne-Centre National de la Recherche Scientifique (CNRS)-Université Clermont Auvergne [2017-2020] (UCA [2017-2020]), ANR-11-LABX-0025,PERSYVAL-lab,Systemes et Algorithmes Pervasifs au confluent des mondes physique et numérique(2011), Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS), Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS), Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Université Clermont Auvergne [2017-2020] (UCA [2017-2020])-Centre National de la Recherche Scientifique (CNRS), Combination of approaches to the security of infinite states systems (CASSIS), Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174) (FEMTO-ST), Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Centre National de la Recherche Scientifique (CNRS)-Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Laboratoire d'Informatique, de Modélisation et d'optimisation des Systèmes (LIMOS), SIGMA Clermont (SIGMA Clermont)-Université d'Auvergne - Clermont-Ferrand I (UdA)-Ecole Nationale Supérieure des Mines de St Etienne-Centre National de la Recherche Scientifique (CNRS)-Université Blaise Pascal - Clermont-Ferrand 2 (UBP), Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Grenoble (INPG)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Université Joseph Fourier - Grenoble 1 (UJF), This work was partly supported by the ANR projects ProSe (decision ANR-2010-VERS-004-01), HPAC (ANR-11-BS02-013) and the support of the 'Digital Trust' Chair from the University of Auvergne Foundation., ANR-10-VERS-0004,ProSe,Protocoles de sécurité : modèle formel, modèle calculatoire et implémentations(2010), ANR-11-BS02-0013,HPAC,Calcul Algébrique Haute-Performance(2011), Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Centre National de la Recherche Scientifique (CNRS)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Centre National de la Recherche Scientifique (CNRS)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Inria Nancy - Grand Est, Université Blaise Pascal - Clermont-Ferrand 2 (UBP)-Université d'Auvergne - Clermont-Ferrand I (UdA)-SIGMA Clermont (SIGMA Clermont)-Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Centre National de la Recherche Scientifique (CNRS), and Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)
Subjects: FOS: Computer and information sciences, TheoryofComputation_MISCELLANEOUS, Computer Science - Cryptography and Security, Computer Networks and Communications, Computer science, Privacy-Enhancing Technology, 0211 other engineering and technologies, Protocol analysis, 0102 computer and information sciences, 02 engineering and technology, Applied Cryptography, Mathematical proof, Computer security, computer.software_genre, 01 natural sciences, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Computer Science - Computer Science and Game Theory, 0202 electrical engineering, electronic engineering, information engineering, Common value auction, Safety, Risk, Reliability and Quality, Protocol (object-oriented programming), ElGamal encryption, 021110 strategic, defence & security studies, Authentication, Auctions, Homomorphic encryption, TheoryofComputation_GENERAL, Cryptographic protocol, Hardware and Architecture, 010201 computation theory & mathematics, Privacy, 020201 artificial intelligence & image processing, Zero-knowledge proof, Anonymity, Cryptographic Protocols, Cryptography and Security (cs.CR), computer, Zero-knowledge proofs, Software, Computer Science and Game Theory (cs.GT)
Abstract: Auctions have a long history, having been recorded as early as 500 B.C. Nowadays, electronic auctions have been a great success and are increasingly used. Many cryptographic protocols have been proposed to address the various security requirements of these electronic transactions, in particular to ensure privacy. Brandt 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. Additionally we discuss some issues with verifiability as well as attacks on non-repudiation, fairness and the privacy of individual bidders exploiting authentication problems., Comment: Africacrypt 2013, Le Caire : Egypt (2013)
Published: 2013
Full Text: View/download PDF

299. Defining Verifiability in e-Auction Protocols

Author: Pascal Lafourcade, Jannik Dreier, Hugo Jonker, Combination of approaches to the security of infinite states systems (CASSIS), Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174) (FEMTO-ST), Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Centre National de la Recherche Scientifique (CNRS)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Centre National de la Recherche Scientifique (CNRS)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Open Universiteit Nederland [Heerlen], Laboratoire d'Informatique, de Modélisation et d'optimisation des Systèmes (LIMOS), Université Blaise Pascal - Clermont-Ferrand 2 (UBP)-Université d'Auvergne - Clermont-Ferrand I (UdA)-SIGMA Clermont (SIGMA Clermont)-Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Centre National de la Recherche Scientifique (CNRS), ACM, Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Centre National de la Recherche Scientifique (CNRS)-Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL), and SIGMA Clermont (SIGMA Clermont)-Université d'Auvergne - Clermont-Ferrand I (UdA)-Ecole Nationale Supérieure des Mines de St Etienne-Centre National de la Recherche Scientifique (CNRS)-Université Blaise Pascal - Clermont-Ferrand 2 (UBP)
Subjects: Computer science, 0211 other engineering and technologies, Protocol analysis, 02 engineering and technology, applied pi, Computer security, computer.software_genre, Formal Methods, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], 0202 electrical engineering, electronic engineering, information engineering, Common value auction, auctions, formal verification, Formal verification, e-Auction, Protocol (science), Computer science [C05] [Engineering, computing & technology], 021110 strategic, defence & security studies, Stakeholder, Protocol Analysis, TheoryofComputation_GENERAL, Formal methods, Sciences informatiques [C05] [Ingénierie, informatique & technologie], 020201 artificial intelligence & image processing, Verifiable secret sharing, Verifiability, verifiability, computer
Abstract: 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.
Published: 2013
Full Text: View/download PDF

300. Verifiability in e-Auction Protocols

Author: Jannik Dreier, Hugo Jonker, pascal lafourcade, Combination of approaches to the security of infinite states systems (CASSIS), Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174) (FEMTO-ST), Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Centre National de la Recherche Scientifique (CNRS)-Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL), Open Universiteit Nederland [Heerlen], Laboratoire d'Informatique, de Modélisation et d'optimisation des Systèmes (LIMOS), SIGMA Clermont (SIGMA Clermont)-Université d'Auvergne - Clermont-Ferrand I (UdA)-Ecole Nationale Supérieure des Mines de St Etienne-Centre National de la Recherche Scientifique (CNRS)-Université Blaise Pascal - Clermont-Ferrand 2 (UBP), ANR-16-IDEX-0001,CAP 20-25,CAP 20-25(2016), Dreier, Jannik, CAP 20-25 - - CAP 20-252016 - ANR-16-IDEX-0001 - IDEX - VALID, Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Centre National de la Recherche Scientifique (CNRS)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Centre National de la Recherche Scientifique (CNRS)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), and Université Blaise Pascal - Clermont-Ferrand 2 (UBP)-Université d'Auvergne - Clermont-Ferrand I (UdA)-SIGMA Clermont (SIGMA Clermont)-Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Centre National de la Recherche Scientifique (CNRS)
Subjects: [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], [INFO.INFO-CR] Computer Science [cs]/Cryptography and Security [cs.CR]
Abstract: 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 perform a detailed study of the verifiability for three examples. We provide an analysis of the protocol by Sako in the applied π-calculus with help of ProVerif, finding it to be correct. Additionally we identify issues with two other protocols.
Published: 2013

Catalog

Books, media, physical & digital resources

See catalog results

Searchworks

Select search scope, currently: Articles Catalog books, media & more in Jio Institute collections Articles journal articles & other e-resources

Search

Search Constraints

Refine your results

Search Limiters

Topic

Publication Year Range

Language

Category

Publication Type

Journal

Database

Publisher

422 results on '"Pascal Lafourcade"'

Search Results

Catalog

Select search scope, currently: Articles

Catalog

books, media & more in Jio Institute collections

Articles

journal articles & other e-resources