Author: "Proof techniques for security protocols (PESTO)" - Searchworks@Jio Institute Digital Library Search Results

Your search keyword '"Proof techniques for security protocols (PESTO)"' showing total 190 results

Start Over Author "Proof techniques for security protocols (PESTO)"

190 results on '"Proof techniques for security protocols (PESTO)"'

1. A formal analysis of the Neuchâtel e-voting protocol

Author: Véronique Cortier, David Galindo, Mathieu Turuani, 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), 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), 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), University of Birmingham [Birmingham], European Project: 645865,H2020 ERC,ERC-2014-CoG,SPOOC(2015), 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 ), Proof techniques for security protocols ( PESTO ), 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 ), 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 ), European Project : 645865,H2020 ERC,ERC-2014-CoG,SPOOC ( 2015 ), 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)-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 Centre National de la Recherche Scientifique (CNRS)
Subjects: Computer science, Electronic voting, media_common.quotation_subject, Internet privacy, [ INFO.INFO-CR ] Computer Science [cs]/Cryptography and Security [cs.CR], ComputingMilieux_LEGALASPECTSOFCOMPUTING, 02 engineering and technology, Computer security, computer.software_genre, Symbolic data analysis, Politics, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Server, Voting, 0202 electrical engineering, electronic engineering, information engineering, 0501 psychology and cognitive sciences, Protocol (object-oriented programming), media_common, business.industry, 05 social sciences, 020206 networking & telecommunications, 16. Peace & justice, Ballot, business, computer, 050104 developmental & child psychology
Abstract: International audience; Remote electronic voting is used in several countries for legally binding elections. Unlike academic voting protocols, these systems are not always documented and their security is rarely analysed rigorously. In this paper, we study a voting system that has been used for electing political representatives and in citizen-driven referenda in the Swiss canton of Neuchâtel. We design a detailed model of the protocol in ProVerif for both privacy and verifiability properties. Our analysis mostly confirms the security of the underlying protocol: we show that the Neuchâtel protocol guarantees ballot privacy, even against a corrupted server; it also ensures cast-as-intended and recorded-as-cast verifiability, even if the voter's device is compromised. To our knowledge, this is the first time a full-fledged automatic symbolic analysis of an e-voting system used for politically-binding elections has been realized.
Published: 2018

2. Hash Gone Bad: Automated discovery of protocol attacks that exploit hash function weaknesses

Author: Cheval, Vincent, Cremers, Cas, Dax, Alexander, Hirschi, Lucca, Jacomme, Charlie, Kremer, Steve, Programming securely with cryptography (PROSECCO), Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Helmholtz Center for Information Security [Saarbrücken] (CISPA), 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), ANR-20-CHIA-0024,ASAP,Des outils pour la vérification symbolique automatisée de protocoles cryptographiques déployés(2020), and ANR-22-PECY-0006,SVP,Verification of Security Protocols(2022)
Subjects: [INFO]Computer Science [cs]
Abstract: International audience; Most cryptographic protocols use cryptographic hash functions as a building block. The security analyses of these protocols typically assume that the hash functions are perfect (such as in the random oracle model). However, in practice, most widely deployed hash functions are far from perfect-and as a result, the analysis may miss attacks that exploit the gap between the model and the actual hash function used. We develop the first methodology to systematically discover attacks on security protocols that exploit weaknesses in widely deployed hash functions. We achieve this by revisiting the gap between theoretical properties of hash functions and the weaknesses of real-world hash functions, from which we develop a lattice of threat models. For all of these threat models, we develop fine-grained symbolic models. Our methodology's fine-grained models cannot be directly encoded in existing state-of-the-art analysis tools by just using their equational reasoning. We therefore develop extensions for the two leading tools, TAMARIN and PROVERIF. In extensive case studies using our methodology, the extended tools rediscover all attacks that were previously reported for these protocols and discover several new variants.
Published: 2023

3. A comprehensive, formal and automated analysis of the EDHOC protocol

Author: Jacomme, Charlie, Klein, Elise, Kremer, Steve, Racouchot, Maïwenn, Programming securely with cryptography (PROSECCO), Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Helmholtz Center for Information Security [Saarbrücken] (CISPA), 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), This work has been partly supported by the ANR Research and teaching chair in AI ASAP (ANR-20-CHIA-0024) and ANR France 2030 project SVP (ANR-22-PECY-0006)., ANR-20-CHIA-0024,ASAP,Des outils pour la vérification symbolique automatisée de protocoles cryptographiques déployés(2020), and ANR-22-PECY-0006,SVP,Verification of Security Protocols(2022)
Subjects: [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR]
Abstract: International audience; EDHOC is a key exchange proposed by IETF's Lightweight Authenticated Key Exchange (LAKE) Working Group (WG). Its design focuses on small message sizes to be suitable for constrained IoT communication technologies. In this paper we provide an in-depth formal analysis of EDHOC-draft version 12, taking into account the different proposed authentication methods and various options. For our analysis we use the SAPIC + protocol platform that allows to compile a single specification to 3 state-of-the-art protocol verification tools (PROVERIF, TAMARIN and DEEPSEC) and take advantage of the strengths of each of the tools. In our analysis we consider a large variety of compromise scenarios, and also exploit recent results that allow to model existing weaknesses in cryptographic primitives, relaxing the perfect cryptography assumption, common in symbolic analysis. While our analysis confirmed security for the most basic threat models, a number of weaknesses were uncovered in the current design when more advanced threat models were taken into account. These weaknesses have been acknowledged by the LAKE WG and the mitigations we propose (and prove secure) have been included in version 14 of the draft.
Published: 2023

4. Inferring RPO Symbol Ordering

Author: Du, Wei, Narendran, Paliath, Rusinowitch, Michael, University at Albany [SUNY], State University of New York (SUNY), 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), Veena Ravishankar, and Christophe Ringeissen
Subjects: [INFO]Computer Science [cs]
Abstract: International audience; We study the recursive path ordering (RPO) in the context of string-rewriting systems. We are interested in finding a symbol ordering in RPO such that for every rule in the rewriting system, the left hand side is higher than the right hand side. We show that this SYMBOL-ORDER problem is NP-complete by a reduction from the 2-3-SAT problem. We also work on the one-rule case and show a polynomial time algorithm for such systems.
Published: 2023

5. Polite Combination of Algebraic Datatypes

Author: Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark Barrett, Computer Science Department [Stanford], Stanford University, Department of Computer Science at Bar Ilan University, Bar-Ilan University [Israël], 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), Massachusetts Institute of Technology, Computer Science and Artificial Intelligence Laboratory, Université de Liège, Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Max-Planck-Institut für Informatik (MPII), and Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est
Subjects: Algebraic datatypes, Satisfiability Modulo Theories, Polite combination, Computational Theory and Mathematics, Artificial Intelligence, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Automated reasoning, Theory combination, Software
Abstract: International audience; Algebraic datatypes, and among them lists and trees, have attracted a lot of interest in automated reasoning and Satisfiability Modulo Theories (SMT). Since its latest stable version, the SMT-LIB standard defines a theory of algebraic datatypes, which is currently supported by several mainstream SMT solvers. In this paper, we study this particular theory of datatypes and prove that it is strongly polite, showing how it can be combined with other arbitrary disjoint theories using polite combination. The combination method uses a new, simple, and natural notion of additivity that enables deducing strong politeness from (weak) politeness.
Published: 2022
Full Text: View/download PDF

6. Tamarin: Verification of Large-Scale, Real-World, Cryptographic Protocols

Author: Basin, David, Cremers, Cas, Dreier, Jannik, Sasse, Ralf, Institute of Information Security [ETH Zürich], Department of Computer Science [ETH Zürich] (D-INFK), Eidgenössische Technische Hochschule - Swiss Federal Institute of Technology [Zürich] (ETH Zürich)- Eidgenössische Technische Hochschule - Swiss Federal Institute of Technology [Zürich] (ETH Zürich), Helmholtz Center for Information Security [Saarbrücken] (CISPA), 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), and 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)
Subjects: [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Computer Networks and Communications, Electrical and Electronic Engineering, Law
Abstract: International audience; Tamarin is a mature, state-of-the-art tool for cryptographic protocol verification. We introduce Tamarin and survey some of the larger, tour-de-force results achieved with it. We also show how Tamarin can formalize a wide range of protocols, adversary models, and properties, and scale to substantial, real-world, verification problems.
Published: 2022
Full Text: View/download PDF

7. Is the JCJ voting system really coercion-resistant?

Author: Cortier, Veronique, Gaudry, Pierrick, Yang, Quentin, 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), Cryptology, arithmetic : algebraic methods for better algorithms (CARAMBA), 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), and ANR-22-PECY-0006,SVP,Verification of Security Protocols(2022)
Subjects: JCJ turvaprotokoll, coercion-resistance, E-voting, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Chide, mõjutuskindlus, JCJ protocol
Abstract: Coercion-resistance is a security property of electronic voting, often considered as a must-have for high-stake elections. The JCJ voting scheme, proposed in 2005 by Juels, Catalano and Jakobsson, is still the reference paradigm when designing a coercion-resistant protocol. We highlight a weakness in JCJ that is also present in all the systems following its general structure. This comes from the procedure that precedes the tally, where the trustees remove the ballots that should not be counted. This phase leaks more information than necessary, leading to potential threats for the coerced voters. Fixing this leads to the notion of cleansing-hiding, that we apply to form a variant of JCJ that we call CHide. One reason for the problem not being seen before is the fact that the associated formal definition of coercion-resistance was too weak. We therefore propose a definition that takes into account more behaviors such as revoting or the addition of fake ballots by authorities. We then prove that CHide is coercion-resistant for this definition.
Published: 2023

8. Belenios with cast as intended

Author: Cortier, Véronique, Debant, Alexandre, Gaudry, Pierrick, Glondu, Stéphane, 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), Cryptology, arithmetic : algebraic methods for better algorithms (CARAMBA), 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), and ANR-22-PECY-0006,SVP,Verification of Security Protocols(2022)
Subjects: belenios, e-voting, cast-as-intended, [INFO]Computer Science [cs]
Abstract: International audience; We propose the BeleniosCaI protocol, a variant of Belenios which brings the cast-as-intended property, in addition to other existing security properties. Our approach is based on a 2-part checksum that the voting device commits to, before being challenged to reveal one of them chosen at random by the voter. It requires only one device on the voter's side and does not rely on previously sent data like with return codes. Compared to the classical Benaloh auditor cast approach, we still have cast-as-intended with only some probability, but the voter's journey is more linear, and the audited ballot is really the one that is cast. We formally prove the security of BeleniosCaI w.r.t. end-to-end verifiability and privacy in a symbolic model, using the ProVerif tool.
Published: 2023

9. Typing High-Speed Cryptography against Spectre v1

Author: Shivakumar, B.A., Barthe, G., Grégoire, B., Laporte, V., Oliviera, T., Priya, S., Schwabe, P., Tabary-Maujean, L., Max Planck Institute for Security and Privacy [Bochum] (MPI Security and Privacy), Institute IMDEA Software [Madrid], Sûreté du logiciel et Preuves Mathématiques Formalisées (STAMP), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), 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), Radboud University [Nijmegen], Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), IEEE, ANR-22-PECY-0006,SVP,Verification of Security Protocols(2022), and European Project: 805031,EPOQUE
Subjects: [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], Digital Security
Abstract: International audience; The current gold standard of cryptographic software is to write efficient libraries with systematic protections against timing attacks. In order to meet this goal, cryptographic engineers increasingly use high-assurance cryptography tools. These tools guide programmers and provide rigorous guarantees that can be verified independently by library users. However, high-assurance tools reason about overly simple execution models that elide transient execution leakage. Thus, implementations validated by high-assurance cryptography tools remain potentially vulnerable to transient execution attacks such as Spectre or Meltdown. Moreover, proposed countermeasures are not used in practice due to performance overhead. We propose, analyze, implement and evaluate an approach for writing efficient cryptographic implementations that are protected against Spectre v1 attacks. Our approach ensures speculative constant-time, an information flow property which guarantees that programs are protected against Spectre v1. Speculative constant-time is enforced by means of a (valuedependent) information flow type system. The type system tracks security levels depending on whether execution is misspeculating. We implement our approach in the Jasmin framework for high-assurance cryptography, and use it for protecting all implementations of an experimental cryptographic library that includes highly optimized implementations of symmetric primitives, of elliptic-curve cryptography, and of Kyber, a latticebased KEM recently selected by NIST for standardization. The performance impact of our protections is very low; for example, less than 1% for Kyber and essentially zero for X25519.
Published: 2023
Full Text: View/download PDF

10. Privacy Preserving Recommendations for Social Networks

Author: Kamalkumar Macwan, Abdessamad Imine, Michael Rusinowitch, 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), LUE Digitrust, and Rusinowitch, Michaël
Subjects: Local Differential Privacy, Social Network, [INFO]Computer Science [cs], [INFO] Computer Science [cs], Recommendation, Differential Privacy, Attribute Privacy
Abstract: International audience; Social recommendation is an advanced service of social networking platforms that is provided to their users. Social recommendation uses profiles and connections to generate personalized suggestions of contents, advertisements, people, pages, or interest groups. Since individual sensitive information is possibly involved in elaborating a recommendation, it may be inferred by an adversary in some situations. In this work, we design a differentially private setting to prevent social recommendations from disclosing sensitive information. Our recommendation system targets users of online social networks by leveraging their attributes and relationships.Unlike other approaches, we rely on both profile similarity and homophily properties. Therefore, our system estimates the frequency of friends who share some attribute values and applies non-negative matrix factorization to derive recommendations such as hobbies, movies.We demonstrate the effectiveness of the proposed approach through experiments on real-world datasets and evaluation according to utility measures.
Published: 2022

11. Reversing, Breaking, and Fixing the French Legislative Election E-Voting Protocol

Author: Debant, Alexandre, Hirschi, Lucca, 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), and 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)
Subjects: [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], security protocols, software analysis, e-voting, security and privacy
Abstract: We conduct a security analysis of the e-voting protocol used for the largest political election using e-voting in the world, the 2022 French legislative election for the citizens overseas. Due to a lack of system and threat model specifications, we built and contributed such specifications by studying the French legal framework and by reverse-engineering the code base accessible to the voters. Our analysis reveals that this protocol is affected by two design-level and implementation-level vulnerabilities. We show how those allow a standard voting server attacker and even more so a channel attacker to defeat the election integrity and ballot privacy due to 6 attack variants. We propose and discuss 5 fixes to prevent those attacks. Our specifications, the attacks, and the fixes were acknowledged by the relevant stakeholders during our responsible disclosure. Our attacks are in the process of being prevented with our fixes for future elections. Beyond this specific protocol, we draw general conclusions and lessons from this instructive experience where an e-voting protocol meets the real-world constraints of a large-scale and political election. Responsible Disclosure and Acknowledgments We conducted this security analysis through passive analysis only; we never attacked voting servers. Therefore, we could not alter the integrity or the security of the election. Moreover, all the vulnerabilities reported in this document have been reported to the relevant stakeholders at least 3 months before publication. We thank those stakeholders, i.e., Europe and Foreign Affairs French Ministry (EFA French Ministry), Agence nationale de la sécurité des systèmes d'information (ANSSI), Voxaly Docaposte, and the researchers running the 3 rd-party services (Stéphane Glondu, Pierrick Gaudry, and Véronique Cortier) for their help and discussions after we sent them our findings. In particular, we would like to thank again the role of ANSSI in the responsible disclosure process, which has always be a key player in promoting transparency and openness. This is greatly appreciated given the context of this work. Finally, we would like to thank our colleagues Myrto Arapinis, Hugo Labrande, and Emmanuel Thomé for their help to collect data about the French Legislative E-Voting Protocol (FLEP).
Published: 2022

12. Verifiable Decryption in the Head

Author: Kristian Gjøsteen, Thomas Haines, Johannes Müller, Peter Rønne, Tjerand Silde, Norwegian University of Science and Technology (NTNU), Australian National University (ANU), University of Luxembourg [Luxembourg], 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), and ANR-22-PECY-0006,SVP,Verification of Security Protocols(2022)
Subjects: [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], MPC-in-the-Head, lattice-based crypto, verifiable decryption, Zero-Knowledge Proofs, distributed decryption
Abstract: International audience; In this work we present a new approach to verifiable decryption which converts a 2-party passively secure distributed decryption protocol into a 1-party proof of correct decryption. This leads to an efficient and simple verifiable decryption scheme for lattice-based cryptography, especially for large sets of ciphertexts; it has small size and lightweight computations as we reduce the need of zero-knowledge proofs for each ciphertext. We believe the flexibility of the general technique is interesting and provides attractive trade-offs between complexity and security, in particular for the interactive variant with smaller soundness. Finally, the protocol requires only very simple operations, making it easy to correctly and securely implement in practice. We suggest concrete parameters for our protocol and give a proof of concept implementation, showing that it is highly practical.
Published: 2022
Full Text: View/download PDF

13. Themis

Author: Bougon, Mikaël, Chabanne, Hervé, Cortier, Véronique, Debant, Alexandre, Dottax, Emmanuelle, Dreier, Jannik, Gaudry, Pierrick, Turuani, Mathieu, Idemia, 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), Cryptology, arithmetic : algebraic methods for better algorithms (CARAMBA), 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), and ANR-22-PECY-0006,SVP,Verification of Security Protocols(2022)
Subjects: [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR]
Abstract: International audience; We propose an on-site voting system Themis, that aims at improving security when local authorities are not fully trusted. Voters vote thanks to voting sheets as well as smart cards that produce encrypted ballots. Electronic ballots are systematically audited, without compromising privacy. Moreover, the system includes a precise dispute resolution procedure identifying misbehaving parties. We conduct a full formal analysis of Themis using ProVerif, with a novel approach in order to cover the modular arithmetic needed in our protocol. In order to evaluate the usability of our system, we organized a voting experiment on a (small) group of voters.
Published: 2022
Full Text: View/download PDF

14. Enforcing Fine-grained Constant-time Policies

Author: Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya, Max Planck Institute for Security and Privacy [Bochum] (MPI Security and Privacy), Institute IMDEA Software [Madrid], Sûreté du logiciel et Preuves Mathématiques Formalisées (STAMP), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), 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), and 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)
Subjects: [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], Secure Compilation, Cryptographic Constant-Time
Abstract: International audience; Cryptographic constant-time (CT) is a popular programming discipline used by cryptographic libraries to protect themselves against timing attacks. The CT discipline aims to enforce that program execution does not leak secrets, where leakage is defined by a formal leakage model. In practice, different leakage models coexist, sometimes even within a single library, both to reflect different architectures and to accommodate different security-efficiency trade-offs. Constant-timeness is popular and can be checked automatically by many tools. However, most sound tools are focused on a baseline (BL) leakage model. In contrast, (sound) verification methods for other leakage models are less developed, in part because these models require modular arithmetic reasoning. In this paper, we develop a systematic, sound, approach for enforcing fine-grained constant-time policies beyond the BL model. Our approach combines two main ingredients: a verification infrastructure, which proves that source programs are constant-time, and a compiler infrastructure, which provably preserves constant-timeness for these fine-grained policies. By making these infrastructures parametric in the leakage model, we achieve the first approach that supports fine-grained constant-time policies. We implement the approach in the Jasmin framework for high-assurance cryptography, and we evaluate our approach with examples from the literature: OpenSSL and wolfSSL. We found a bug in OpenSSL and provided a formally verified fix.
Published: 2022
Full Text: View/download PDF

15. Features and usage of Belenios in 2022

Author: Véronique Cortier, Pierrick Gaudry, Stéphane Glondu, 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), Cryptology, arithmetic : algebraic methods for better algorithms (CARAMBA), 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), Service Expérimentation et Développement [Nancy] (SED), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), and ANR-20-CHIA-0024,ASAP,Des outils pour la vérification symbolique automatisée de protocoles cryptographiques déployés(2020)
Subjects: [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Belenios, interneti teel hääletamine, Internet voting, avatud lähtekood, Open-Source
Abstract: International audience; Belenios is an open-source Internet voting protocol associated to a free voting platform, launched in 2015. A detailed overview of the protocol has been presented in [6] in 2019 and its complete, up-todate specification is public [7]. Since 2019, the use of Belenios has significantly increased with more than 1,400 elections organized each year in 2020 and 2021, and a total of more than 100,000 received ballots. We report here on the new features added to Belenios since 2019 that include weighted votes, flexible counting methods (e.g. Condorcet or STV) thanks to mixnets, and crowdsourced translation with the support of more than 10 languages. Moreover, we have improved the auditability of Belenios in practice, both for voters and authorities.
Published: 2022

16. Time, Privacy, Robustness, Accuracy: Trade-Offs for the Open Vote Network Protocol

Author: Fatima-Ezzahra El Orche, Rémi Géraud-Stewart, Peter B. Rønne, Gergei Bana, David Naccache, Peter Y. A. Ryan, Marco Biroli, Megi Dervishi, Hugo Waltsburger, University of Luxembourg [Luxembourg], Qualcomm Technologies, Inc., 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), University of Missouri [Columbia] (Mizzou), University of Missouri System, CentraleSupélec, and ANR-22-PECY-0006,SVP,Verification of Security Protocols(2022)
Subjects: [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], E-Voting, denial of service, decentralised voting, open vote network
Abstract: The open vote network ( [10]) is a secure two-round multi-party protocol facilitating the computation of a sum of integer votes without revealing their individual values. This is done without a central authority trusted for privacy, and thus allows decentralised and anonymous decision-making efficiently. As such, it has also been implemented in other settings such as financial applications, see e.g. [15, 17].An inherent limitation of is its lack of robustness against denial-of-service attacks, which occur when at least one of the voters participates in the first round of the protocol but (maliciously or accidentally) not in the second. Unfortunately, such a situation is likely to occur in any real-world implementation of the protocol with many participants. This could incur serious time delays from either waiting for the failing parties and perhaps having to perform extra protocol rounds with the remaining participants.This paper provides a solution to this problem by extending with mechanisms tolerating a number of unresponsive participants, the basic idea being to run several sub-elections in parallel. The price to pay is a carefully controlled privacy loss, an increase in computation, and a statistical loss in accuracy, which we demonstrate how to measure precisely.
Published: 2022
Full Text: View/download PDF

17. Automatic generation of sources lemmas in TAMARIN: towards automatic proofs of security protocols

Author: Cortier, Véronique, Delaune, Stéphanie, Dreier, Jannik, Klein, Elise, 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), Security & PrIvaCY (SPICY), SYSTÈMES LARGE ÉCHELLE (IRISA-D1), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), 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)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT), ANR-17-CE39-0004,TECAP,Analyse de protocoles - unir les outils existants(2017), ANR-20-CE39-0009,SEVERITAS,Systèmes de tests et evaluations sûrs et vérifiables(2020), European Project: 714955,H2020,ERC-2016-STG,POPSTAR(2017), and European Project: 645865,H2020 ERC,ERC-2014-CoG,SPOOC(2015)
Subjects: [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Tamarin Prover, Formal Verification
Abstract: International audience; TAMARIN is a popular tool dedicated to the formal analysis of security protocols. One major strength of the tool is that it offers an interactive mode, allowing to go beyond what pushbutton tools can typically handle. TAMARIN is for example able to verify complex protocols such as TLS, 5G, or RFID protocols. However, one of its drawback is its lack of automation. For many simple protocols, the user often needs to help TAMARIN by writing specific lemmas, called "sources lemmas", which requires some knowledge of the internal behaviour of the tool. In this paper, we propose a technique to automatically generate sources lemmas in TAMARIN. Following the intuition of manually written sources lemmas, our lemmas try to keep track of the origin of a term by looking into emitted messages or facts. We prove formally that our lemmas indeed hold, for arbitrary protocols that make use of cryptographic primitives that can be modelled with a subterm convergent equational theory (modulo associativity and commutativity). We have implemented our approach within TAMARIN. Our experiments show that, in most examples of the literature, we are now able to generate suitable sources lemmas automatically, in replacement of the handwritten lemmas. As a direct application, many simple protocols can now be analysed fully automatically, while they previously required user interaction.
Published: 2022
Full Text: View/download PDF

18. Graph-Embedded Term Rewrite Systems and Applications (A Preliminary Report)

Author: Dwyer Satterfield, Saraid, Erbatur, Serdar, Marshall, Andrew, Ringeissen, Christophe, University of Mary Washington, University of Texas at Dallas [Richardson] (UT Dallas), 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), David Cerna, and Barbara Morawska
Subjects: [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
Abstract: International audience
Published: 2022

19. Sapic+ : protocol verifiers of the world, unite!

Author: Cheval, Vincent, Jacomme, Charlie, Kremer, Steve, Künnemann, Robert, Programming securely with cryptography (PROSECCO), Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Helmholtz Center for Information Security [Saarbrücken] (CISPA), 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), and 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)
Subjects: [INFO]Computer Science [cs]
Abstract: International audience; Symbolic security protocol verifiers have reached a high degree of automation and maturity. Today, experts can model real-world protocols, but this often requires model-specific encodings and deep insight into the strengths and weaknesses of each of those tools. With Sapic+ , we introduce a protocol verification platform that lifts this burden and permits choosing the right tool for the job, at any development stage. We build on the existing compiler from Sapic to Tamarin, and extend it with automated translations from Sapic+ to ProVerif and DeepSec, as well as powerful, protocol-independent optimizations of the existing translation. We prove each part of these translations sound. A user can thus, with a single Sapic+ file, verify reachability and equivalence properties on the specified protocol, either using ProVerif, Tamarin or DeepSec. Moreover, the soundness of the translation allows to directly assume results proven by another tool which allows to exploit the respective strengths of each tool. We demonstrate our approach by analyzing various existing models. This includes a large case study of the 5G authentication protocols, previously analyzed in Tamarin. Encoding this model in Sapic + we demonstrate the effectiveness of our approach. Moreover, we study four new case studies: the LAKE and the Privacy-Pass protocols, both under standardization, the SSH protocol with the agent-forwarding feature, and the recent KEMTLS protocol, a post-quantum version of the main TLS key exchange.
Published: 2022

20. A small bound on the number of sessions for security protocols

Author: Cortier, Véronique, Dallon, Antoine, Delaune, Stéphanie, 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), 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), 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), DGA Maîtrise de l'information (DGA.MI), Direction générale de l'Armement (DGA), SYSTÈMES LARGE ÉCHELLE (IRISA-D1), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), 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), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Bretagne Sud (UBS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT), 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)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Security & PrIvaCY (SPICY), and Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA)
Subjects: [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], ComputingMilieux_MISCELLANEOUS
Abstract: International audience; Bounding the number of sessions is a long-standing problem in the context of security protocols. It is well known that even simple properties like secrecy are undecidable when an unbounded number of sessions is considered. Yet, attacks on existing protocols only require a few sessions.In this paper, we propose a sound algorithm that computes a sufficient set of scenarios that need to be considered to detect an attack. Our approach can be applied for both reachability and equivalence properties, for protocols with standard primitives thatare type-compliant (unifiable messages have the same type). Moreover, when equivalence properties are considered, else branches are disallowed, and protocols are supposed to be simple (an attacker knows from which role and session a message comes from).Since this class remains undecidable, ouralgorithm may return an infinite set. However, our experiments show that on most basic protocols of the literature, our algorithm computesa small number of sessions (a dozen). As a consequence, tools for a bounded number of sessions like DeepSec can then be used to conclude that a protocol is secure for an unbounded number of sessions.
Published: 2022

21. An Extensive Formal Analysis of Multi-factor Authentication Protocols

Author: Steve Kremer, Charlie Jacomme, École normale supérieure - Cachan (ENS Cachan), 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), ANR-14-CE28-0030,Sequoia,Propriété de sécurité, équivalence de processes et vérification automatique(2014), European Project: 645865,H2020 ERC,ERC-2014-CoG,SPOOC(2015), Laboratoire Spécification et Vérification (LSV), and Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)
Subjects: General Computer Science, Computer science, Protocol analysis, 0102 computer and information sciences, 02 engineering and technology, Computer security, computer.software_genre, Security token, 01 natural sciences, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], 0202 electrical engineering, electronic engineering, information engineering, Message authentication code, 0501 psychology and cognitive sciences, Safety, Risk, Reliability and Quality, Password, Protocol (science), Authentication, 05 social sciences, 020206 networking & telecommunications, Cryptographic protocol, Multi-factor authentication, Telecommunications network, Phishing, 010201 computation theory & mathematics, Authentication protocol, Threat model, computer, 050104 developmental & child psychology
Abstract: Passwords are still the most widespread means for authenticating users, even though they have been shown to create huge security problems. This motivated the use of additional authentication mechanisms in so-called multi-factor authentication protocols. In this article, we define a detailed threat model for this kind of protocol: While in classical protocol analysis attackers control the communication network, we take into account that many communications are performed over TLS channels, that computers may be infected by different kinds of malware, that attackers could perform phishing, and that humans may omit some actions. We formalize this model in the applied pi calculus and perform an extensive analysis and comparison of several widely used protocols—variants of Google 2-step and FIDO’s U2F (Yubico’s Security Key token). The analysis is completely automated, generating systematically all combinations of threat scenarios for each of the protocols and using the P ROVERIF tool for automated protocol analysis. To validate our model and attacks, we demonstrate their feasibility in practice, even though our experiments are run in a laboratory environment. Our analysis highlights weaknesses and strengths of the different protocols. It allows us to suggest several small modifications of the existing protocols that are easy to implement, as well as an extension of Google 2-step that improves security in several threat scenarios.
Published: 2021
Full Text: View/download PDF

22. A Decidable Class of Security Protocols for Both Reachability and Equivalence Properties

Author: Stéphanie Delaune, Véronique Cortier, Vaishnavi Sundararajan, 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), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), 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)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT), Security & PrIvaCY (SPICY), SYSTÈMES LARGE ÉCHELLE (IRISA-D1), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-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)-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), The research leading to these results has received funding from the European Research Council under the European Union’s horizon 2020 research and innovation program (ERC grant agreement n◦ 714955-POPSTAR and ERC grant agreement n◦ 645865-SPOOC), as well as from the French National Research Agency (ANR) under the project TECAP., ANR-17-CE39-0004,TECAP,Analyse de protocoles - unir les outils existants(2017), European Project: 714955,H2020,ERC-2016-STG,ERC-POPSTAR(2017), European Project: 645865,H2020 ERC,ERC-2014-CoG,SPOOC(2015), 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), and Université de Rennes (UNIV-RENNES)-CentraleSupélec-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique)
Subjects: Theoretical computer science, Cryptographic primitive, Computer science, business.industry, Verification, Privacy properties, 020207 software engineering, 0102 computer and information sciences, 02 engineering and technology, Cryptographic protocol, Encryption, 01 natural sciences, Security protocols, Decidability, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Dependency graph, Computational Theory and Mathematics, 010201 computation theory & mathematics, Artificial Intelligence, Reachability, 0202 electrical engineering, electronic engineering, information engineering, Equivalence (formal languages), business, Software, Cryptographic nonce
Abstract: International audience; We identify a new decidable class of security protocols, both for reachability and equivalence properties. Our result holds for an unbounded number of sessions and for protocols with nonces. It covers all standard cryptographic primitives. Our class sets up three main assumptions. (i) Protocols need to be "simple", meaning that an attacker can precisely identify from which participant and which session a message originates from. We also consider protocols with no else branches (only positive test). (ii) Protocols should be type-compliant, which is intuitively guaranteed as soon as two encrypted messages of the protocol cannot be confused. (iii) Finally, we define the notion of a dependency graph, which, given a protocol, characterises how actions depend on the other ones (both sequential dependencies and data dependencies are taken into account). Whenever the graph is acyclic, then the protocol falls into our class. We show that many protocols of the literature belong to our decidable class, including for example some of the protocols embedded in the biometric passport.
Published: 2020
Full Text: View/download PDF

23. Inferring attributes with picture metadata embeddings

Author: Michaël Rusinowitch, Abdessamad Imine, Bizhan Alipour Pijani, 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), IMPACT-DIGITRUST, ANR-15-IDEX-0004,LUE,Isite LUE(2015), 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), and 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)
Subjects: Network reliability, Computer science, Embedded systems, Closeness, Image sharing, Inference, Ocean Engineering, 02 engineering and technology, privacy, [INFO.INFO-SI]Computer Science [cs]/Social and Information Networks [cs.SI], gender inference, [INFO.INFO-AI]Computer Science [cs]/Artificial Intelligence [cs.AI], [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Redundancy, Mode (computer interface), 020204 information systems, 0202 electrical engineering, electronic engineering, information engineering, Leverage (statistics), Emojis, Social network, graph embedding, inference attack, Information retrieval, Robotics, 16. Peace & justice, Metadata, picture, 020201 artificial intelligence & image processing
Abstract: International audience; Users in online social networks are vulnerable to attribute inference attacks due to some published data. Thus, the picture owner's gender has a strong influence on individuals' emotional reactions to the photo. In this work, we present a graph-embedding approach for gender inference attacks based on pictures meta-data such as (i) alt-texts generated by Facebook to describe the content of images, and (ii) Emojis/Emoticons posted by friends, friends of friends or regular users as a reaction to the picture. Specifically, we apply a semi-supervised technique, node2vec, for learning a mapping of pictures meta-data to a low-dimensional vector space. Next, we study in this vector space the gender closeness of users who published similar photos and/or received similar reactions. We leverage this image sharing and reaction mode of Facebook users to derive an efficient and accurate technique for user gender inference. Experimental results show that privacy attack often succeeds even when other information than pictures published by their owners is either hidden or unavailable.
Published: 2020
Full Text: View/download PDF

24. Le vote électronique - les défis du secret et de la transparence

Author: Cortier, Véronique, Gaudry, Pierrick, 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), Cryptology, arithmetic : algebraic methods for better algorithms (CARAMBA), and 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)
Subjects: [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR]
Abstract: Préface de Gérard Berry; National audience
Published: 2022

25. Proving Unlinkability using ProVerif through Desynchronized Bi-Processes

Author: Baelde, David, Debant, Alexandre, Delaune, Stéphanie, Security & PrIvaCY (SPICY), SYSTÈMES LARGE ÉCHELLE (IRISA-D1), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Université de Rennes 1 (UR1), 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 (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Rennes 1 (UR1), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT), 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), 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)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), ANR-20-CHIA-0024,ASAP,Des outils pour la vérification symbolique automatisée de protocoles cryptographiques déployés(2020), and ANR-22-PECY-0006,SVP,Verification of Security Protocols(2022)
Subjects: symbolic models, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], formal methods, unlinkability
Abstract: Unlinkability is a privacy property of crucial importance for several systems such as mobile phones or RFID chips. Analysing this security property is very complex, and highly error-prone. Therefore, formal verification with machine support is desirable. Unfortunately, existing techniques are not sufficient to directly apply verification tools to automatically prove unlinkability.In this paper, we overcome this limitation by defining a simple. transformation that will exploit several features recently introduced in the tool ProVerif. This transformation, together with some generic axioms, allow the tool to successfully conclude on several case studies. We have implemented our approach, effectively obtaining direct proofs of unlinkability on several protocols that were, until now, out of reach of automatic verification tools. Moreover, our approach is not specific to unlinkability and could, in principle, be useful in other contexts.
Published: 2022

26. A Logic and an Interactive Prover for the Computational Post-Quantum Security of Protocols

Author: Cas Cremers, Caroline Fontaine, Charlie Jacomme, Helmholtz Center for Information Security [Saarbrücken] (CISPA), Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), 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), and 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)
Subjects: [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR]
Abstract: International audience; We provide the first mechanized post-quantum sound security protocol proofs. We achieve this by developing PQ-BC, a computational first-order logic that is sound with respect to quantum attackers, and corresponding mechanization support in the form of the PQ-Squirrel prover. Our work builds on the classical BC logic [7] and its mechanization in the Squirrel [5] prover. Our development of PQ-BC requires making the BC logic sound for a single interactive quantum attacker. We implement the PQ-Squirrel prover by modifying Squirrel, relying on the soundness results of PQ-BC and enforcing a set of syntactic conditions; additionally, we provide new tactics for the logic that extend the tool’s scope. Using PQ-Squirrel, we perform several case studies, thereby giving the first mechanical proofs of their computational post-quantum security. These include two generic constructions of KEM based key exchange, two sub-protocols from IKEv1 and IKEv2, and a proposed post-quantum variant of Signal’s X3DH protocol. Additionally, we use PQ-Squirrel to prove that several classical Squirrel case studies are already post-quantum sound.
Published: 2022

27. Automatically Distributing and Updating In-Network Management Rules for Software Defined Networks

Author: Ahmad Abboud, Remi Garcia, Abdelkader Lahmadi, Michael Rusinowitch, Adel Bouhoula, Mondher Ayadi, NUMERYX, Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria), Resilience and Elasticity for Security and ScalabiliTy of dynamic networked systems (RESIST), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Networks, Systems and Services (LORIA - NSS), 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), Department of Computing and Games, Teesside University, Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Proof techniques for security protocols (PESTO), 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), and Arabian Gulf University, Kingdom of Bahrain
Subjects: [INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI], [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], [INFO.INFO-MO]Computer Science [cs]/Modeling and Simulation
Abstract: International audience
Published: 2022
Full Text: View/download PDF

28. Attribute inference attacks on social media publications

Author: Pijani, Bizhan Alipour, 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), Université de Lorraine, Michaël Rusinowitch, Abdessamad Imine, and ANR-15-IDEX-0004,LUE,Isite LUE(2015)
Subjects: Private attribute, Attribut Privé, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Online Social Networks, Privacy, Réseaux Sociaux en Ligne, Machine learning, Online Inference Attacks, Attaques par Inférence en Ligne, [INFO]Computer Science [cs], Apprentissage automatique, [INFO.INFO-SI]Computer Science [cs]/Social and Information Networks [cs.SI], Privacité
Abstract: Online Social Networks (OSN) are full of personal information such as gender, age, relationship status. The popularity and growth of OSN have rendered their platforms vulnerable to malicious activities and increased user privacy concerns. The privacy settings available in OSN do not prevent users from attribute inference attacks where an attacker seeks to illegitimately obtain their personal attributes (such as the gender attribute) from publicly available information. Disclosure of personal information can have serious outcomes such as personal spam, bullying, profile cloning for malicious activities, or sexual harassment. Existing inference techniques are either based on the target user behavior analysis through their liked pages and group memberships or based on the target user friend list. However, in real cases, the amount of available information to an attacker is small since users have realized the vulnerability of standard attribute inference attacks and concealed their generated information. To increase awareness of OSN users about threats to their privacy, in this thesis, we introduce a new class of attribute inference attacks against OSN users. We show the feasibility of these attacks from a very limited amount of data. They are applicable even when users hide all their profile information and their own comments. Our proposed methodology is to analyze Facebook picture metadata, namely (i) alt-text generated by Facebook to describe picture contents, and (ii) commenters’ words and emojis preferences while commenting underneath the picture, to infer sensitive attributes of the picture owner. We show how to launch these inference attacks on any Facebook user by i) handling online newly discovered vocabulary using a retrofitting process to enrich a core vocabulary that was built during offline training and ii) computing several embeddings for textual units (e.g., word, emoji), each one depending on a specific attribute value. Finally, we introduce ProPic, a protection mechanism that selects comments to be hidden in a computationally efficient way while minimizing utility loss according to a semantic measure. The proposed mechanism can help end-users to check their vulnerability to inference attacks and suggests comments to be hidden in order to mitigate the attacks. We have determined the success of the attacks and the protection mechanism by experiments on real data.; Les réseaux sociaux contiennent de nombreuses informations personnelles telles que le genre, l'âge ou le statut d'une relation. Leur popularité et leur importance en font des cibles privilégiés pour des activités malveillantes menaçant la vie privée des utilisateurs. Les paramètres de sécurité disponibles sur les réseaux sociaux n'empêchent pas les attaques par inférence d'attribut, qui consistent pour l'attaquant à obtenir des données privées (comme le genre) à partir d'informations publiques. La divulgation d'une information personnelle peut avoir des conséquences négatives comme devenir la cible de spams, de harcèlements, ou se faire cloner son profil. Les techniques d'inférence les plus connues s'appuient soit sur l'analyse du comportement de l'utilisateur cible à travers ses préférences (e.g., likes) et ses groupes, soit sur ses listes d'amis. Cependant, en pratique, les informations disponibles pour ces attaques sont souvent limitées car beaucoup d'utilisateurs ont pris conscience des menaces et préfèrent protéger leurs données. Pour que les usagers des réseaux sociaux comprennent mieux les risques encourus par leur vie privée, dans cette thèse nous introduisons une nouvelle classe d'attaques par inférence sur les attributs de ces usagers. Nous montrons que ces attaques nécessitent très peu d'information. Elles s'appliquent même à des usagers qui protègent les éléments de leur profil ainsi que leurs commentaires. La méthode que nous proposons consiste à analyser les métadatas d'une image publiée sur Facebook, à savoir i) les tags engendrés par Facebook pour décrire les images (e.g., pour les usagers malvoyants), et ii) les commentaires sous formes textuelle ou d'émojis déposés sous l'image. Nous montrons comment réaliser ces attaques sur un utilisateur de Facebook en i) appliquant une technique de retrofitting pour traiter le vocabulaire rencontré en ligne et qui ne figurait pas dans la base d'apprentissage et ii) en calculant plusieurs plongements pour les unités textuelles (e.g., mot, emoji) chacun dépendant d'une valeur spécifique d'un attribut. Finalement nous proposons ProPic, un mécanisme de protection qui sélectionne de manière rapide des commentaires à cacher toute en minimisant la perte d'utilité, définie par une mesure sémantique. Le système permet aux utilisateurs de vérifier s'ils sont vulnérables à des attaques par inférence et, le cas échéant de suggérer les commentaires à cacher pour prévenir ces attaques. Nous avons pu vérifier l'efficacité de l'approche par des expérimentations sur des données réelles.
Published: 2022

29. Differentially Private Friends Recommendation

Author: Kamalkumar Macwan, Abdessamad Imine, Michael Rusinowitch, Rusinowitch, Michaël, 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), and LUE Digitrust
Subjects: Social Networks, [INFO]Computer Science [cs], Recommendation, Differential Privacy, [INFO] Computer Science [cs], Link Privacy
Abstract: International audience; Most recommendation systems in social networks provide users with relevant new friend suggestions by processing their personal information or their current friends lists. However, providing such recommendations may leak users' private information. We present a new differentially private recommendation algorithm that preserves the privacy of both attribute values and friend links. The algorithm mainly proceeds by adding calibrated noise to an adequate matrix representation of the social network. To get a good trade-off between privacy and accuracy, the required amount of noise should be limited and therefore we need to mitigate the prohibitive sensitivity of the matrix representation. For that, we apply a graph projection technique to control the size of friends lists. The effectiveness of our approach is demonstrated by experiments on real-world datasets and comparison with existing methods.
Published: 2022
Full Text: View/download PDF

30. On Privacy of Multidimensional Data Against Aggregate Knowledge Attacks

Author: Laouir, Ala Eddine, Imine, Abdessamad, Designing the Future of Computational Models (MOCQUA), 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), Proof techniques for security protocols (PESTO), and Projet DigiTrust, LUE
Subjects: Cell suppression, [INFO.INFO-DB]Computer Science [cs]/Databases [cs.DB], Data cubes, Cube compression, Cell perturbation, [INFO]Computer Science [cs], Privacy preservation
Abstract: International audience; In this paper, we explore the privacy problem of individuals in publishing data cubes using SUM queries, where a malicious user is expected to have an aggregate knowledge (e.g., average information) over the data ranges. We propose an efficient solution that maximizes the utility of SUM queries while mitigating inference attacks from aggregate knowledge. Our solution combines cube compression (i.e., suppression of data cells) and data perturbation. First, we give a formal statement for the privacy of aggregate knowledge based on data suppression. Next, we develop a Linear Programming (LP) model to determine the number of data cells to be removed and a heuristic method to effectively suppress data cells. To overcome the limitation of data suppression, we complement it with suitable data perturbation. Through empirical evaluation on benchmark data cubes, we show that our solution gives best performance in terms of utility and privacy.
Published: 2022
Full Text: View/download PDF

31. Combined Hierarchical Matching: the Regular Case

Author: Erbatur, Serdar, Marshall, Andrew M., Ringeissen, Christophe, University of Texas at Dallas [Richardson] (UT Dallas), University of Mary Washington, 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), and Felty, Amy P.
Subjects: [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Matching, Theory of computation → Equational logic and rewriting, equational theories, Theory of computation → Automated reasoning, combination problem
Abstract: Matching algorithms are often central sub-routines in many areas of automated reasoning. They are used in areas such as functional programming, rule-based programming, automated theorem proving, and the symbolic analysis of security protocols. Matching is related to unification but provides a somewhat simplified problem. Thus, in some cases, we can obtain a matching algorithm even if the unification problem is undecidable. In this paper we consider a hierarchical approach to constructing matching algorithms. The hierarchical method has been successful for developing unification algorithms for theories defined over a constructor sub-theory. We show how the approach can be extended to matching problems which allows for the development, in a modular way, of hierarchical matching algorithms. Here we focus on regular theories, where both sides of each equational axiom have the same set of variables. We show that the combination of two hierarchical matching algorithms leads to a hierarchical matching algorithm for the union of regular theories sharing only a common constructor sub-theory., LIPIcs, Vol. 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), pages 6:1-6:22
Published: 2022
Full Text: View/download PDF

32. Machine-Checked Proofs of Privacy Against Malicious Boards for Selene & Co

Author: Constantin Catalin Dragan, Francois Dupressoir, Ehsan Estaji, Kristian Gjosteen, Thomas Haines, Peter Y.A. Ryan, Peter B. Ronne, Morten Rotvold Solberg, University of Surrey (UNIS), University of Bristol [Bristol], University of Luxembourg [Luxembourg], NTNU Samfunnsforskning AS / NTNU Social Research, Norwegian University of Science and Technology [Trondheim] (NTNU), Norwegian University of Science and Technology (NTNU)-Norwegian University of Science and Technology (NTNU), Australian National University (ANU), 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), and ANR-22-PECY-0006,SVP,Verification of Security Protocols(2022)
Subjects: [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR]
Abstract: International audience; Privacy is a notoriously difficult property to achieve in complicated systems and especially in electronic voting schemes. Moreover, electronic voting schemes is a class of systems that require very high assurance. The literature contains a number of ballot privacy definitions along with security proofs for common systems. Some machine-checked security proofs have also appeared. We define a new ballot privacy notion that captures a larger class of voting schemes. This notion improves on the state of the art by taking into account that verification in many schemes will happen or must happen after the tally has been published, not before as in previous definitions. As a case study we give a machine-checked proof of privacy for Selene, which is a remote electronic voting scheme which offers an attractive mix of security properties and usability. Prior to our work, the computational privacy of Selene has never been formally verified. Finally, we also prove that MiniVoting and Belenios satisfies our definition.
Published: 2022
Full Text: View/download PDF

33. Symbolic protocol verification with dice: process equivalences in the presence of probabilities (extended version)

Author: Cheval, Vincent, Crubillé, Raphaëlle, Kremer, Steve, Kremer, Steve, Programming securely with cryptography (PROSECCO), Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Laboratoire d'Informatique et Systèmes (LIS), Aix Marseille Université (AMU)-Université de Toulon (UTLN)-Centre National de la Recherche Scientifique (CNRS), 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), This work has been partly supported by the ANR Research and teaching chair in AI ASAP and by ANR TECAP (decision number ANR-17-CE39-0004-03)., ANR-20-CHIA-0024,ASAP,Des outils pour la vérification symbolique automatisée de protocoles cryptographiques déployés(2020), and ANR-22-PECY-0006,SVP,Verification of Security Protocols(2022)
Subjects: [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], [INFO.INFO-CR] Computer Science [cs]/Cryptography and Security [cs.CR]
Abstract: Symbolic protocol verification generally abstracts probabilities away, considering computations that succeed only with negligible probability, such as guessing random numbers or breaking an encryption scheme, as impossible. This abstraction, sometimes referred to as the perfect cryptography assumption, has shown very useful as it simplifies automation of the analysis. However, probabilities may also appear in the control flow where they are generally not negligible. In this paper we consider a framework for symbolic protocol analysis with a probabilistic choice operator: the probabilistic applied pi calculus. We define and explore the relationships between several behavioral equivalences. In particular we show the need to require randomized schedulers-indeed we exhibit a counterexample to one of the main results in a previous work that relied on non-randomized ones. As in other frameworks that mix both non-deterministic and probabilistic choices, schedulers may sometimes be unrealistically powerful. We therefore consider two subclasses of processes that avoid this problem. When considering purely non-deterministic protocols, as is done in classical symbolic verification, we show that a probabilistic adversary has-maybe surprisingly-a strictly superior distinguishing power for may testing, which, when the number of sessions is bounded, we show to coincide with purely possibilistic similarity. Finally, we consider fully probabilistic protocols and show that trace equivalence corresponds to a notion of may testing with purely probabilistic attackers. We also briefly discuss complexity and automation for these subclasses when the number of sessions is bounded.
Published: 2022

34. Efficient Rules Management Algorithms in Software Defined Networking

Author: Abboud, Ahmad, 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), Resilience and Elasticity for Security and ScalabiliTy of dynamic networked systems (RESIST), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Networks, Systems and Services (LORIA - NSS), University of Lorraine, Michaël Rusinowitch, Institut National de Recherche en Informatique et en Automatique (Inria), Numerys Technologies, Université de Lorraine, and Abdelkader Lahmadi
Subjects: Réseaux définis par logiciel, Minimisation des paquets, Software defined networks, Placement des règles, Packet minimization, [INFO]Computer Science [cs], Rule placement, Filtrage des paquets, Packet filtering
Abstract: In software-defined networks (SDN), the filtering requirements for critical applications often vary according to flow changes and security policies. SDN addresses this issue with a flexible software abstraction, allowing simultaneous and convenient modification and implementation of a network policy on flow-based switches.With the increase in the number of entries in the ruleset and the size of data that traverses the network each second, it remains crucial to minimize the number of entries and accelerate the lookup process. On the other hand, attacks on Internet have reached a high level. The number keeps increasing, which increases the size of blacklists and the number of rules in firewalls. The limited storage capacity requires efficient management of that space. In the first part of this thesis, our primary goal is to find a simple representation of filtering rules that enables more compact rule tables and thus is easier to manage while keeping their semantics unchanged. The construction of rules should be obtained with reasonably efficient algorithms too. This new representation can add flexibility and efficiency in deploying security policies since the generated rules are easier to manage. A complementary approach to rule compression would be to use multiple smaller switch tables to enforce access-control policies in the network. However, most of them have a significant rules replication, or even they modify the packet's header to avoid matching a rule by a packet in the next switch. The second part of this thesis introduces new techniques to decompose and distribute filtering rule sets over a given network topology. We also introduce an update strategy to handle the changes in network policy and topology. In addition, we also exploit the structure of a series-parallel graph to efficiently resolve the rule placement problem for all-sized networks intractable time.; Au sein des réseaux définis par logiciel (SDN), les exigences de filtrage pour les applications critiques varient souvent en fonction des changements de flux et des politiques de sécurité. SDN résout ce problème avec une abstraction logicielle flexible, permettant la modification et la mise en \oe{}uvre simultanées et pratiques d'une politique réseau sur les routeurs.Avec l'augmentation du nombre de règles de filtrage et la taille des données qui traversent le réseau chaque seconde, il est crucial de minimiser le nombre d'entrées et d'accélérer le processus de recherche. D'autre part, l'accroissement du nombre d'attaques sur Internet s'accompagne d'une augmentation de la taille des listes noires et du nombre de règles des pare-feux. Leur capacité de stockage limitée nécessite une gestion efficace de l'espace. Dans la première partie de cette thèse, nous proposons une représentation compacte des règles de filtrage tout en préservant leur sémantique. La construction de cette représentation est obtenue par des algorithmes raisonnablement efficaces. Cette technique permet flexibilité et efficacité dans le déploiement des politiques de sécurité puisque les règles engendrées sont plus faciles à gérer.Des approches complémentaires à la compression de règles consistent à décomposer et répartir les tables de règles, pour implémenter, par exemple, des politiques de contrôle d'accès distribué.Cependant, la plupart d'entre elles nécessitent une réplication importante de règles, voire la modification des en-têtes de paquets. La deuxième partie de cette thèse présente de nouvelles techniques pour décomposer et distribuer des ensembles de règles de filtrage sur une topologie de réseau donnée. Nous introduisons également une stratégie de mise à jour pour gérer les changements de politique et de topologie du réseau. De plus, nous exploitons également la structure de graphe série-parallèle pour résoudre efficacement le problème de placement de règles.
Published: 2021

35. A privacy attack on the Swiss Post e-voting system

Author: Cortier, Véronique, Debant, Alexandre, Gaudry, Pierrick, 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), Cryptology, arithmetic : algebraic methods for better algorithms (CARAMBA), 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), Université de Lorraine, CNRS, Inria, LORIA, ANR-20-CHIA-0024,ASAP,Des outils pour la vérification symbolique automatisée de protocoles cryptographiques déployés(2020), and IACR
Subjects: [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR]
Abstract: International audience; The SwissPost e-voting system is currently proposed under the scrutiny of the community, before being deployed in 2022 for political elections in several Swiss Cantons. We explain how real world constraints led to shortcomings that allowed a privacy attack to be mounted. More precisely, dishonest authorities can learn the vote of several voters of their choice, without being detected, even when the requested threshold of honest authorities act as prescribed.
Published: 2021

36. Structured Leakage and Applications to Cryptographic Constant-Time and Cost

Author: Swarn Priya, Benjamin Grégoire, Gilles Barthe, Vincent Laporte, Institute IMDEA Software [Madrid], Max Planck Institute for Security and Privacy [Bochum] (MPI Security and Privacy), Sûreté du logiciel et Preuves Mathématiques Formalisées (STAMP), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), 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), and 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)
Subjects: Semantics (computer science), Computer science, Cryptography, 02 engineering and technology, computer.software_genre, Operational semantics, Security and privacy, law.invention, Formal methods and theory of security, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], 03 medical and health sciences, Constant (computer programming), law, 0202 electrical engineering, electronic engineering, information engineering, Transformer, ComputingMilieux_MISCELLANEOUS, 030304 developmental biology, Leakage (electronics), 0303 health sciences, Sequence, [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], business.industry, 020207 software engineering, Computer engineering, Logic and verification, Compiler, business, computer
Abstract: International audience; Many security properties of interest are captured by instrumented semantics that model the functional behavior and the leakage of programs. For several important properties, including cryptographic constant-time (CCT), leakage models are sufficiently abstract that one can define instrumented semantics for high-level and low-level programs. One important goal is then to relate leakage of source programs and leakage of their compilation---this can be used, e.g., to prove preservation of CCT. To simplify this task, we put forward the idea of structured leakage. In contrast to the usual modeling of leakage as a sequence of observations, structured leakage is tightly coupled with the operational semantics of programs. This coupling greatly simplifies the definition of leakage transformers that map the leakage of source programs to leakage of their compilation and yields more precise statements about the preservation of security properties. We illustrate our methods on the Jasmin compiler and prove preservation results for two policies of interest: CCT and cost.
Published: 2021
Full Text: View/download PDF

37. Verifying Table-Based Elections

Author: Jannik Dreier, Saša Radomirović, Sofia Giampietro, David Basin, Institute of Information Security [ETH Zürich], Department of Computer Science [ETH Zürich] (D-INFK), Eidgenössische Technische Hochschule - Swiss Federal Institute of Technology [Zürich] (ETH Zürich)- Eidgenössische Technische Hochschule - Swiss Federal Institute of Technology [Zürich] (ETH Zürich), 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), and Heriot-Watt University [Edinburgh] (HWU)
Subjects: Protocol (science), Correctness, Electronic voting, Computer science, business.industry, media_common.quotation_subject, Cryptography, 02 engineering and technology, Elections, 16. Peace & justice, Computer security, computer.software_genre, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Protocol verification, 020204 information systems, Secrecy, 0202 electrical engineering, electronic engineering, information engineering, Key (cryptography), Table (database), Verifiability, 020201 artificial intelligence & image processing, Simplicity, business, computer, media_common
Abstract: International audience; Verifiability is a key requirement for electronic voting. However, the use of cryptographic techniques to achieve it usually requires specialist knowledge to understand; hence voters cannot easily assess the validity of such arguments themselves. To address this, solutions have been proposed using simple tables and checks, which require only simple verification steps with almost no cryptography. This simplicity comes at a cost: numerous verification checks must be made on the tables to ensure their correctness, raising the question whether the success of all the small verification steps entails the overall goal of end-to-end verifiability while preserving vote secrecy. Do the final results reflect the voters' will? Moreover, do the verification steps leak information about the voters' choices? In this paper, we provide mathematical foundations and an associated methodology for defining and proving verifiability and voter privacy for table-based election protocols. We apply them to three case studies: the Eperio protocol, Scantegrity, and Chaum's Random-Sample Election protocol. Our methodology helps us, in all three cases, identify previously unknown problems that allow an election authority to cheat and modify the election outcome. Furthermore, it helps us formulate and verify the corrected versions.
Published: 2021
Full Text: View/download PDF

38. FAIRiser vos données : mémorandum

Author: Idmhand, Fatiha, Galleron, Ioana, Laouir, Ala Eddine, Echavarria, Andres, Passion, Laurent, Centre de recherches latino-américaines - ARCHIVOS (CRLA - ARCHIVOS), Institut des textes et manuscrits modernes (ITEM), Université de Poitiers-Centre National de la Recherche Scientifique (CNRS)-Département Littératures et langage - ENS Paris (LILA), École normale supérieure - Paris (ENS Paris), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-École normale supérieure - Paris (ENS Paris), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Université de Poitiers-Centre National de la Recherche Scientifique (CNRS)-Département Littératures et langage - ENS Paris (LILA), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL), Consortium CAHIER (CAHIER), Huma-Num : la TGIR des humanités numériques (Huma-Num), Aix Marseille Université (AMU)-Centre National de la Recherche Scientifique (CNRS)-Aix Marseille Université (AMU)-Centre National de la Recherche Scientifique (CNRS), Lattice - Langues, Textes, Traitements informatiques, Cognition - UMR 8094 (Lattice), Université Sorbonne Nouvelle - Paris 3-Université Sorbonne Paris Cité (USPC)-Centre National de la Recherche Scientifique (CNRS)-Université Paris sciences et lettres (PSL)-Département Littératures et langage - ENS Paris (LILA), Université Paris sciences et lettres (PSL), 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), Centre National de la Recherche Scientifique (CNRS), CAHIER - Consortium CAHIER, Université de Poitiers-Centre National de la Recherche Scientifique (CNRS)-Département Littératures et langage (LILA), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Université de Poitiers-Centre National de la Recherche Scientifique (CNRS)-Département Littératures et langage (LILA), Département Littératures et langage (LILA), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Centre National de la Recherche Scientifique (CNRS)-Université Sorbonne Paris Cité (USPC)-Université Sorbonne Nouvelle - Paris 3, École normale supérieure - Paris (ENS-PSL), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-École normale supérieure - Paris (ENS-PSL), Équipe humanités numériques (ITEM – HuNu), Département Littératures et langage - ENS Paris (LILA), 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: [INFO.INFO-TT]Computer Science [cs]/Document and Text Processing, [SHS.STAT]Humanities and Social Sciences/Methods and statistics, [SHS.LITT]Humanities and Social Sciences/Literature, [INFO.INFO-CY]Computer Science [cs]/Computers and Society [cs.CY], [INFO.INFO-DS]Computer Science [cs]/Data Structures and Algorithms [cs.DS], [INFO.INFO-WB]Computer Science [cs]/Web, [INFO.INFO-MM]Computer Science [cs]/Multimedia [cs.MM], [INFO.INFO-NA]Computer Science [cs]/Numerical Analysis [cs.NA], [INFO.INFO-SI]Computer Science [cs]/Social and Information Networks [cs.SI]
Published: 2021

39. Implementing Security Protocol Monitors

Author: Yannick Chevalier, Michaël Rusinowitch, Logique, Interaction, Langue et Calcul (IRIT-LILaC), Institut de recherche en informatique de Toulouse (IRIT), Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées-Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse - Jean Jaurès (UT2J)-Université Toulouse III - Paul Sabatier (UT3), Université Fédérale Toulouse Midi-Pyrénées-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées, 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), Université Toulouse Capitole (UT Capitole), Université de Toulouse (UT)-Université de Toulouse (UT)-Université Toulouse - Jean Jaurès (UT2J), Université de Toulouse (UT)-Université Toulouse III - Paul Sabatier (UT3), Université de Toulouse (UT)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université de Toulouse (UT)-Toulouse Mind & Brain Institut (TMBI), Université Toulouse - Jean Jaurès (UT2J), Université de Toulouse (UT)-Université de Toulouse (UT)-Université Toulouse III - Paul Sabatier (UT3), Université de Toulouse (UT)-Université Toulouse Capitole (UT Capitole), and Université de Toulouse (UT)
Subjects: Protocol (science), FOS: Computer and information sciences, Computer Science - Cryptography and Security, Computer science, business.industry, 02 engineering and technology, Cryptographic protocol, 16. Peace & justice, computer.software_genre, Set (abstract data type), 03 medical and health sciences, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], 0302 clinical medicine, [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], 020204 information systems, 0202 electrical engineering, electronic engineering, information engineering, Compiler, business, computer, Implementation, Cryptography and Security (cs.CR), 030217 neurology & neurosurgery, Computer network
Abstract: Cryptographic protocols are often specified by narrations, i.e., finite sequences of message exchanges that show the intended execution of the protocol. Another use of narrations is to describe attacks. We propose in this paper to compile, when possible, attack describing narrations into a set of tests that honest participants can perform to exclude these executions. These tests can be implemented in monitors to protect existing implementations from rogue behaviour., Comment: In Proceedings SCSS 2021, arXiv:2109.02501
Published: 2021
Full Text: View/download PDF

40. Formal verification of a constant-time preserving C compiler

Author: David Pichardie, Benjamin Grégoire, Gilles Barthe, Alix Trieu, Vincent Laporte, Rémi Hutin, Sandrine Blazy, Institute IMDEA Software [Madrid], Max Planck Institute for Security and Privacy [Bochum] (MPI Security and Privacy), Software certification with semantic analysis (CELTIQUE), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), 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)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-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)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT), Sûreté du logiciel et Preuves Mathématiques Formalisées (STAMP), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), 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), École normale supérieure - Rennes (ENS Rennes), Aarhus University [Aarhus], This work is supported by DFF project 6108-00363 from The Danish Council for Independent Research for the Natural Sciences (FNU), by the Office of Naval Research under projects N00014-12-1-0914, N00014-15-1-2750 and N00014-19-1-2292, and by a European Research Council (ERC) Consolidator Grant for the project 'VESTA', funded under the European Union’s Horizon 2020 Framework Programme (grant agreement no. 772568)., European Project: 772568,VESTA(2018), 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), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-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)-École normale supérieure - Rennes (ENS Rennes)-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes 1 (UR1), 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: 0303 health sciences, [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], Computer science, Programming language, business.industry, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Optimizing compiler, 020207 software engineering, Cryptography, 02 engineering and technology, Reuse, computer.software_genre, Operational semantics, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], 03 medical and health sciences, Constant (computer programming), 0202 electrical engineering, electronic engineering, information engineering, Code (cryptography), Compiler, Safety, Risk, Reliability and Quality, business, computer, Formal verification, Software, 030304 developmental biology
Abstract: Timing side-channels are arguably one of the main sources of vulnerabilities in cryptographic implementations. One effective mitigation against timing side-channels is to write programs that do not perform secret-dependent branches and memory accesses. This mitigation, known as "cryptographic constant-time", is adopted by several popular cryptographic libraries. This paper focuses on compilation of cryptographic constant-time programs, and more specifically on the following question: is the code generated by a realistic compiler for a constant-time source program itself provably constant-time? Surprisingly, we answer the question positively for a mildly modified version of the CompCert compiler, a formally verified and moderately optimizing compiler for C. Concretely, we modify the CompCert compiler to eliminate sources of potential leakage. Then, we instrument the operational semantics of CompCert intermediate languages so as to be able to capture cryptographic constant-time. Finally, we prove that the modified CompCert compiler preserves constant-time. Our mechanization maximizes reuse of the CompCert correctness proof, through the use of new proof techniques for proving preservation of constant-time. These techniques achieve complementary trade-offs between generality and tractability of proof effort, and are of independent interest.
Published: 2019
Full Text: View/download PDF

41. New Privacy Threat on 3G, 4G, and Upcoming 5G AKA Protocols

Author: Lucca Hirschi, Ravishankar Borgaonkar, Altaf Shaik, Shinjo Park, Stiftelsen for INdustriell og TEknisk Forskning Digital [Trondheim] (SINTEF Digital), Department of Computer Science [ETH Zürich] (D-INFK), Eidgenössische Technische Hochschule - Swiss Federal Institute of Technology [Zürich] (ETH Zürich), 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), 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), 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), Technische Universität Berlin (TU), and Technical University of Berlin / Technische Universität Berlin (TU)
Subjects: Security analysis, Standardization, Exploit, Computer science, 02 engineering and technology, Computer security, computer.software_genre, GeneralLiterature_MISCELLANEOUS, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], 0202 electrical engineering, electronic engineering, information engineering, [INFO]Computer Science [cs], Protocol (object-oriented programming), General Environmental Science, Vulnerability (computing), Ethics, business.industry, Information technology, 020206 networking & telecommunications, QA75.5-76.95, BJ1-1725, Electronic computers. Computer science, General Earth and Planetary Sciences, 020201 artificial intelligence & image processing, Mobile telephony, business, computer, 5G
Abstract: Mobile communications are used by more than two-thirds of the world population who expect security and privacy guarantees. The 3rd Generation Partnership Project (3GPP) responsible for the worldwide standardization of mobile communication has designed and mandated the use of the AKA protocol to protect the subscribers’ mobile services. Even though privacy was a requirement, numerous subscriber location attacks have been demonstrated against AKA, some of which have been fixed or mitigated in the enhanced AKA protocol designed for 5G. In this paper, we reveal a new privacy attack against all variants of the AKA protocol, including 5G AKA, that breaches subscriber privacy more severely than known location privacy attacks do. Our attack exploits a new logical vulnerability we uncovered that would require dedicated fixes. We demonstrate the practical feasibility of our attack using low cost and widely available setups. Finally we conduct a security analysis of the vulnerability and discuss countermeasures to remedy our attack.
Published: 2019
Full Text: View/download PDF

42. Politeness for the Theory of Algebraic Datatypes (Extended Abstract)

Author: Yoni Zohar, Christophe Ringeissen, Clark Barrett, Ying Sheng, Jane Lange, Pascal Fontaine, Stanford University, 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), Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Université de Liège, Proof-oriented development of computer-based systems (MOSEL), Department of Formal Methods (LORIA - FM), 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), 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), 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)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft, 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)-Institut National de Recherche en Informatique et en Automatique (Inria)
Subjects: Computer science, Politeness, media_common.quotation_subject, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Disjoint sets, 16. Peace & justice, Computer Science::Computers and Society, Algebra, Cover (topology), Simple (abstract algebra), Satisfiability modulo theories, Computer Science::Logic in Computer Science, Natural (music), Computer Science::Programming Languages, Automated reasoning, Algebraic number, media_common
Abstract: International audience; Algebraic datatypes, and among them lists and trees, have attracted a lot of interest in automated reasoning and Satisfiability Modulo Theories (SMT). Since its latest stable version, the SMT-LIB standard defines a theory of algebraic datatypes, which is currently supported by several mainstream SMT solvers. In this paper, we study this particular theory of datatypes and prove that it is strongly polite, showing also how it can be combined with other arbitrary disjoint theories using polite combination. Our results cover both inductive and finite datatypes, as well as their union. The combination method uses a new, simple, and natural notion of additivity, that enables deducing strong politeness from (weak) politeness.
Published: 2021
Full Text: View/download PDF

43. Politeness and Stable Infiniteness: Stronger Together

Author: Andrew Reynolds, Clark Barrett, Cesare Tinelli, Yoni Zohar, Ying Sheng, Christophe Ringeissen, Stanford University, 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), University of Iowa [Iowa City], André Platzer, Geoff Sutcliffe, 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), and 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)
Subjects: FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Theoretical computer science, Smart contract, Politeness, Computer science, media_common.quotation_subject, Contrast (statistics), [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, Logic in Computer Science (cs.LO), 010201 computation theory & mathematics, Order (business), Satisfiability modulo theories, 0202 electrical engineering, electronic engineering, information engineering, Benchmark (computing), sort, Combination method, media_common
Abstract: International audience; We make two contributions to the study of polite combination in satisfiability modulo theories. The first contribution is a separation between politeness and strong politeness, by presenting a polite theory that is not strongly polite. This result shows that proving strong politeness (which is often harder than proving politeness) is sometimes needed in order to use polite combination. The second contribution is an optimization to the polite combination method, obtained by borrowing from the Nelson-Oppen method. In its non-deterministic form, the Nelson-Oppen method is based on guessing arrangements over shared variables. In contrast, polite combination requires an arrangement over \emph{all} variables of the shared sort (not just the shared variables). We show that when using polite combination, if the other theory is stably infinite with respect to a shared sort, only the shared variables of that sort need be considered in arrangements, as in the Nelson-Oppen method. Reasoning about arrangements of variables is exponential in the worst case, so reducing the number of variables that are considered has the potential to improve performance significantly. We show preliminary evidence for this in practice by demonstrating a speed-up on a smart contract verification benchmark.
Published: 2021
Full Text: View/download PDF

44. Fixing the Achilles Heel of E-Voting: The Bulletin Board

Author: Lucca Hirschi, David Basin, Lara Schmid, 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), and Eidgenössische Technische Hochschule - Swiss Federal Institute of Technology [Zürich] (ETH Zürich)
Subjects: Protocol (science), Electronic voting, Computer science, Cheating, media_common.quotation_subject, Probabilistic logic, 16. Peace & justice, Computer security, computer.software_genre, Bulletin board, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Voting, Verifiable secret sharing, Bulletin board system, computer, ComputingMilieux_MISCELLANEOUS, media_common
Abstract: The results of electronic elections should be verifiable so that any cheating is detected. To support this, many protocols employ an electronic bulletin board (BB) for publishing data that can be read by participants and used for verifiability checks. We demonstrate that the BB is itself a security-critical component that has often been treated too casually in previous designs and analyses. In particular, we present novel attacks on the e-voting protocols Belenios, Civitas, and Helios that violate some of their central security claims under realistic system assumptions. These attacks were outside the scope of prior security analyses as their verifiability notions assume an idealized BB.To enable the analysis of protocols under realistic assumptions about the BB, we introduce a new verifiability definition applicable to arbitrary BBs. We identify a requirement, called final-agreement, and formally prove that it is sufficient and, in most cases, necessary to achieve verifiability. We then propose a BB protocol that satisfies final-agreement under weak, realistic trust assumptions and provide a machine-checked proof thereof. Our protocol can replace existing BBs, enabling verifiability under much weaker trust assumptions.
Published: 2021
Full Text: View/download PDF

45. A toolbox for verifiable tally-hiding e-voting systems

Author: Cortier, Véronique, Gaudry, Pierrick, Yang, Quentin, 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), Cryptology, arithmetic : algebraic methods for better algorithms (CARAMBA), Department of Algorithms, Computation, Image and Geometry (LORIA - ALGO), 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)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria), 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), 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), and ANR-20-CHIA-0024,ASAP,Des outils pour la vérification symbolique automatisée de protocoles cryptographiques déployés(2020)
Subjects: [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], ComputingMilieux_COMPUTERSANDSOCIETY
Abstract: Cryptology ePrint Archive: Report 2021/491https://eprint.iacr.org/2021/491; International audience; In most verifiable electronic voting schemes, one key step is the tally phase, where the election result is computed from the encrypted ballots. A generic technique consists in first applying (verifiable) mixnets to the ballots and then revealing all the votes in the clear. This however discloses much more information than the result of the election itself (that is, the winners) and may offer the possibility to coerce voters. In this paper, we present a collection of building blocks for designing tally-hiding schemes based on multi-party computations. As an application, we propose the first tally-hiding schemes with no leakage for four important counting functions: D'Hondt, Condorcet, STV, and Majority Judgment. We also unveil unknown flaws or leakage in several previously proposed tally-hiding schemes.
Published: 2021

46. Vérification efficace d'équivalences observationnelles de processus cryptographiques : théorie et pratique

Author: Rakotonirina, Itsaka, 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), Université de Lorraine, Steve Kremer, Vincent Cheval, European Project: 645865,H2020 ERC,ERC-2014-CoG,SPOOC(2015), 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: Optimization, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Observational equivalences, Symétries, Analysis of cryptographic protocols, Analyse des protocoles cryptographiques, Optimisation, DeepSec, Équivalences observationnelles, Symmetries
Abstract: This thesis studies the analysis of cryptographic protocols. They are sequences of instructions permitting to interact with a recipient remotely while protecting the sensitive content of the communication from a potential malicious third party. Classical cases where the confidentiality and the integrity of the communication are critical are, among others, online payments and medical-service booking, or electronic voting. We study notions of security defined technically by observational equivalences (which includes among others confidentiality, anonymity or non-traceability). We designed a program, DeepSec, which, from the description of a protocol for a fixed number of participants, verifies in a fully-automated way whether the protocol offers a security guarantee of this type. We demonstrate the ability of this tool to analyse complex attack scenarios through several examples. After that, we present an optimization technique exploiting symmetries in security proofs. Typically, participants with similar roles in the protocol often have similar instructions to follow, inducing redundant work during the analysis. On several examples, using this technique allowed to reduce the analysis time of DeepSec by several orders of magnitude. Finally, we also studied the theoretical aspect the problem in order to determine to which extent DeepSec’s algorithm could be improved (can we make the tool faster?) or made more expressive (can we get rid of some of the limitations of the tool?). For that we carried out a complete analysis of the computational complexity of DeepSec’s algorithm, and integrated it to a detailed survey of the state of the art regarding complexity results in similar contexts. This meticulous survey allowed us to expose subtle variations in how the problem is formalised across the literature—sometimes impacting its complexity. We also include new results and improve some of the surveyed ones, resulting in a clearer understanding of the problem.; Cette thèse porte sur l’analyse des protocoles cryptographiques. Ce sont des suites d’instructions permettant d’interagir à distance avec un interlocuteur tout en protégeant le contenu sensible de la communication d’une potentielle tierce partie malveillante. Des cas classiques où la confidentialité et l’intégrité de la communication sont critiques sont, parmi d’autres, les paiements et services de santé en ligne, ou le vote électronique. Nous étudions les notions de sécurité définies techniquement par des équivalences observationnelles (ce qui inclut, entre autres, la confidentialité, l’anonymat ou la non-traçabilité). Nous avons conçu un programme, DeepSec, qui, à partir de la description d’un protocole pour un nombre fixé de participants, vérifie de manière entièrement automatisée si le protocole offre une garantie de sécurité donnée de ce type. Nous démontrons ensuite la capacité de cet outil à analyser des scenarios d’attaques complexes à travers plusieurs exemples. Dans un deuxième temps, nous présentons une technique d’optimisation reposant sur l’exploitation de symétries dans les preuves de sécurité. Typiquement, les participants ayant des rôles similaires dans le protocole ont souvent les mêmes instructions à suivre, ce qui induit des tâches redondantes lors de l’analyse. Sur plusieurs exemples, l’utilisation de cette technique d’optimisation a permis de réduire le temps d’analyse de DeepSec de plusieurs ordres de magnitude. Enfin, nous avons également étudié l’aspect théorique du problème afin de déterminer dans quelle mesure l’algorithme de DeepSec pouvait être amélioré (peut-on rendre l’outil plus rapide ?) ou rendu plus expressif (peut-on rendre l’outil capable d’analyser plus de protocoles, i.e., nous débarrasser de certaines de ses limitations ?). Nous avons pour cela fait une analyse de complexité calculatoire complète de l’algorithme de DeepSec, et l’avons intégré à une revue détaillée de l’état de l’art des résultats de complexité dans des contextes similaires. Cette revue minutieuse nous a permis de mettre au jour des variations subtiles dans la formalisation du problème à travers la littérature — parfois ayant un impact sur sa complexité. Nous y incluons de nouveaux résultats et améliorons certains ce ceux passés en revue, offrant une compréhension plus claire du problème.
Published: 2021

47. Les livraisons dangereuses

Author: Rakotonirina, Itsaka, 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), 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), and 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)
Subjects: [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Protocole cryptographique, Sécurité réseaux, Chiffrement, Primitive cryptographique
Abstract: National audience; Bientôt des échanges 100% sécurisés ? Découvrez la réponse dans cette histoire épistolaire de cryptographie et de gourmandise...
Published: 2021

48. FOX: Fooling with Explanations Privacy Protection with Adversarial Reactions in Social Media

Author: Noreddine Belhadj-Cheikh, Abdessamad Imine, Michael Rusinowitch, Rusinowitch, Michaël, 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), and 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)
Subjects: [INFO.INFO-SI] Computer Science [cs]/Social and Information Networks [cs.SI], Adversarial Machine Learning, 16. Peace & justice, Explainability, [INFO.INFO-SI]Computer Science [cs]/Social and Information Networks [cs.SI], 03 medical and health sciences, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], 0302 clinical medicine, Social Networks, 030502 gerontology, Privacy, 0305 other medical science, 030217 neurology & neurosurgery, [INFO.INFO-CR] Computer Science [cs]/Cryptography and Security [cs.CR]
Abstract: International audience; Social media data has been mined over the years to predict individual sensitive attributes such as political and religious beliefs. Indeed, mining such data can improve the user experience with personalization and freemium services. Still, it can also be harmful and discriminative when used to make critical decisions, such as employment. In this work, we investigate social media privacy protection against attribute inference attacks using machine learning explainability and adversarial defense strategies. More precisely, we propose FOX (FOoling with eXplanations), an adversarial attack framework to explain and fool sensitive attribute inference models by generating effective adversarial reactions. We evaluate the performance of FOX with other SOTA baselines in a black-box setting by attacking five gender attribute classifiers trained on Facebook pictures reactions, specifically (i) comments generated by Facebook users excluding the picture owner, and (ii) textual tags (i.e., alttext) generated by Facebook. Our experiments show that FOX successfully fools (about 99.7% and 93.2% of the time) the classifiers, outperforms the SOTA baselines and gives a good transferability of adversarial features.
Published: 2021

49. How to explain security protocols to your children

Author: Véronique Cortier, Itsaka Rakotonirina, 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), Max Planck Institute for Security and Privacy [Bochum] (MPI Security and Privacy), and ANR-20-CHIA-0024,ASAP,Des outils pour la vérification symbolique automatisée de protocoles cryptographiques déployés(2020)
Subjects: [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], 010201 computation theory & mathematics, 020204 information systems, 0202 electrical engineering, electronic engineering, information engineering, 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences
Abstract: International audience; Security protocols combine two key components: a logical structure (who answers what, under which conditions?) as well as cryptography (encryption, signature, hash,. . .). It is not so easy to explain their principles and weaknesses to a non expert audience. Why is something an attack or not? For which attacker? With what purpose? In this paper, we propose an approach to introduce security protocols to a general audience, including children or even scientists from different fields. Its goal is to convey the implicit assumptions of our community, such as threat models or the participants' behaviour. This all-public introduction can be thought of as a story but, interestingly, can also be implemented physically with boxes and padlocks: manipulation helps to understand how protocols operate, even permitting non-expert participants to design their own-and thus to size the challenges of this task.
Published: 2021
Full Text: View/download PDF

50. Divide-and-Learn: A Random Indexing Approach to Attribute Inference Attacks in Online Social Networks

Author: Sanaz Eidizadehakhcheloo, Bizhan Alipour Pijani, Abdessamad Imine, Michaël Rusinowitch, Università degli Studi di Roma 'La Sapienza' = Sapienza University [Rome], 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), Università degli Studi di Roma 'La Sapienza' = Sapienza University [Rome] (UNIROMA), TC 11, WG 11.3, and Ken Barker
Subjects: Information retrieval, Computer science, Emoji, Comparability, Inference, 02 engineering and technology, 16. Peace & justice, [INFO.INFO-SI]Computer Science [cs]/Social and Information Networks [cs.SI], [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Random indexing, Social Networks, Privacy, Attribute Inference Attack, 020204 information systems, 0202 electrical engineering, electronic engineering, information engineering, Targeted advertising, 020201 artificial intelligence & image processing, Random Indexing, Classifier (UML), Value (mathematics), Word (computer architecture)
Abstract: Part 6: Potpourri II; International audience; We present a Divide-and-Learn machine learning methodology to investigate a new class of attribute inference attacks against Online Social Networks (OSN) users. Our methodology analyzes commenters' preferences related to some user publications (e.g., posts or pictures) to infer sensitive attributes of that user. For classification performance, we tune Random Indexing (RI) to compute several embeddings for textual units (e.g., word, emoji), each one depending on a specific attribute value. RI guarantees the comparability of the generated vectors for the different values. To validate the approach, we consider three Facebook attributes: gender, age category and relationship status, which are highly relevant for targeted advertising or privacy threatening applications. By using an XGBoost classifier, we show that we can infer Facebook users' attributes from commenters' reactions to their publications with AUC from 94% to 98%, depending on the traits.
Published: 2021
Full Text: View/download PDF

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

Journal

Database

Publisher

190 results on '"Proof techniques for security protocols (PESTO)"'

Search Results

Catalog

Select search scope, currently: Articles

Catalog

books, media & more in Jio Institute collections

Articles

journal articles & other e-resources