Computer-aided analysis of security protocols heavily relies on equational theories to model cryptographic primitives. Most automated verifiers for security protocols focus on equational theories that satisfy the Finite Variant Property (FVP), for which solving unification is decidable. However, they either require to prove FVP by hand or at least to provide a representation as an$E$-convergent rewrite system, usually$E$being at most the equational theory for an associative and commutative function symbol (AC). The verifier ProVerif is probably the only exception amongst these tools as it automatically proves FVP without requiring a representation, but on a small class of equational theories. In this work, we propose a novel semi-decision procedure for proving FVP, without the need for a specific representation, and for a class of theories that goes beyond the ones expressed by an$E$-convergent rewrite system. We implemented a prototype and successfully applied it on several theories from the literature.

The Squirrel Prover is a proof assistant designed for the computational verification of cryptographic protocols. It implements a probabilistic logic that captures cryptographic and probabilistic arguments used in security proofs. This logic operates in the asymptotic security setting, which limits the expressiveness of formulas and proofs. As a consequence, it can only prove security for finite interactions with a protocol, falling outside of the polynomial-level of security usually expected by cryptographers. We lift all these limitations by moving to a concrete security setting. We extend the logic with concrete security predicates, and design a corresponding proof system. We show the usefulness of these extensions on a case study, and through a novel proof-transformation result which shows that a large class of asymptotic logic security proofs can be automatically rewritten into concrete logic security proofs, improving security bounds exponentially.

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.

Abstract Classification algorithms/tools become more and more powerful and pervasive. Yet, for some use cases, it is necessary to be able to protect data privacy while benefiting from the functionalities they provide. Among the tools that may be used to ensure such privacy, we are focusing in this paper on functional encryption. These relatively new cryptographic primitives enable the evaluation of functions over encrypted inputs, outputting cleartext results. Theoretically, this property makes them well-suited to process classification over encrypted data in a privacy by design’ rationale, enabling to perform the classification algorithm over encrypted inputs (i.e. without knowing the inputs) while only getting the input classes as a result in the clear. In this paper, we study the security and privacy issues of classifiers using today practical functional encryption schemes. We provide an analysis of the information leakage about the input data that are processed in the encrypted domain with state-of-the-art functional encryption schemes. This study, based on experiments ran on MNIST and Census Income datasets, shows that neural networks are able to partially recover information that should have been kept secret. Hence, great care should be taken when using the currently available functional encryption schemes to build privacy-preserving classification services. It should be emphasized that this work does not attack the cryptographic security of functional encryption schemes, it rather warns the community against the fact that they should be used with caution for some use cases and that the current state-ofthe-art may lead to some operational weaknesses that could be mitigated in the future once more powerful functional encryption schemes are available.

Post-quantum cryptography gets increasing attention lately, as we have to prepare alternative cryptographic solutions that will resist attacks from quantum computers. A very large effort is being done to replace the usual primitives such as encryption, signature or authentication. This effort also pulls new cryptographic features such as Somewhat or Fully Homomorphic Encryption schemes, based on lattices. Since their introduction in 2009, lots of the burden has been overcome and real applications now become possible. However many papers suffer from the fast constant pace of evolution on the attack side, so their parameter analysis is usually incomplete or obsolete. In this work we present a thorough study of two schemes that have proven their worth: FV and SHIELD, providing a deep analysis of how to setup and size their parameters, to ensure both correctness and security. Our overall aim is to provide easy-to-use guidelines for implementation purposes.

Somewhat Homomorphic Encryption (SHE) schemes allow to carry out operations on data in the cipher domain. In a cloud computing scenario, personal information can be processed secretly, inferring a high level of confidentiality. For many years, practical parameters of SHE schemes were overestimated, leading to only consider the FFT algorithm to accelerate SHE in hardware. Nevertheless, recent work demonstrates that parameters can be lowered without compromising the security [1]. Following this trend, this work investigates the benefits of using Karatsuba algorithm instead of FFT for the Fan-Vercauteren (FV) Homomorphic Encryption scheme. The proposed accelerator relies on an hardware/software co-design approach, and is designed to perform fast arithmetic operations on degree 2,560 polynomials with 135 bits coefficients, allowing to compute small algorithms homomorphically. Compared to a functionally equivalent design using FFT, our accelerator performs an homomorphic multiplication in 11.9 ms instead of 15.46 ms, and halves the size of logic utilization and registers on the FPGA.

In this work, we study the practical security of inner-product functional encryption. We left behind the mathematical security proof of the schemes, provided in the literature, and focus on what attackers can use in realistic scenarios without tricking the protocol, and how they can retrieve more than they should be able to. This study is based on the proposed protocol from [1]. We generalize the scenario to an attacker possessing n secret keys. We propose attacks based on machine learning, and experiment them over the MNIST dataset [2].

Somewhat Homomorphic Encryption (SHE) schemes can be used to carry out operations on ciphered data. In a cloud computing scenario, personal information can be processed secretly, inferring a high level of confidentiality. The principle limitation of SHE is the size of ciphertext compared to the size of the message. This issue can be addressed by using a batching technique that “packs” several messages into one ciphertext. However, this method leads to important drawbacks in standard implementations. This paper presents a fast hardware/software co-design implementation of an encryption procedure using the Karatsuba algorithm. Our hardware accelerator is 1.5 times faster than the state of the art for 1 encryption and 4 times faster for 4 encryptions.

Somewhat Homomorphic Encryption (SHE) schemes allow to carry out operations on data in the cipher domain. In a cloud computing scenario, personal information can be processed secretly, inferring a high level of confidentiality. Most practical Somewhat Homomorphic Encryption (SHE) schemes require the implementation of fast polynomial arithmetic, that is why hardware accelerators usually target the FFT/NTT algorithm. This paper proposes a co-design hardware/software approach to accelerate SHE using Karatsuba algorithm. Depending on the needs, Karatsuba algorithm allows to implement additional computations to the hardware in order to reduce software computation time. Our accelerator is designed to speed up arithmetic on degree 2560 polynomials with 125 bits coefficients. We provide 3 different approaches: An area efficient design, a balanced design, and a performance-oriented design. Our accelerator performs a polynomial multiplication in respectively 2.46 ms, 1.70 ms and 1.24 ms, and a relinearization operation in 2.28 ms, 1.53 ms and 1.1 ms, while a functionally equivalent design using the FFT [1] performs the multiplication in 1.96 ms and the relinearization in 4.79 ms for hardware resources consumption equivalent to the balanced design.

To design robust symmetric encryption schemes, we need to use Boolean functions with suitable properties. Among the security criteria these functions need to fulfill, we can mention algebraic immunity. A lot of papers study how to construct suitable functions, but some of them assume the validity of Tu-Deng's combinatorial conjecture [2] to estimate the algebraic immunity of the Boolean functions they design. In this paper we prove two new results about this conjecture and point out a new family of integers that satisfy it.

International audience

This article proposes a theory of watermarking security based on a cryptanalysis point of view. The main idea is that information about the secret key leaks from the observations, for instance watermarked pieces of content, available to the opponent. Tools from information theory (Shannon's mutual information and Fisher's information matrix) can measure this leakage of information. The security level is then defined as the number of observations the attacker needs to successfully estimate the secret key. This theory is applied to two common watermarking methods: the substitutive scheme and the spread spectrum based techniques. Their security levels are calculated against three kinds of attack

We introduce a new approach for the study of weight distributions of cosets of the Reed-Muller code of order 1. Our approach is based on the method introduced by Kasami (1968), using Pless (1963) identities. By interpreting some equations, we obtain a necessary condition for a coset to have a "high" minimum weight. Most notably, we are able to distinguish such cosets which have three weights only. We then apply our results to the problem of the nonlinearity of Boolean functions. We particularly study the links between this criterion and the propagation characteristics of a function.

We present architectures for the secure delivery of images over open networks, such as the Internet or broadcast networks. Those systems integrate access control mechanisms and tracking procedures, once the pictorial material has been accessed. We show how these architectures have been tested in the context of the connection of cultural databases to the Internet (AQUARELLE system) and in the context of broadcasting of high-value TV programs (OCTALIS system used during the football World Cup). This work shows the interest for a global integrated design of delivery systems in which watermarking, monitoring, and public key infrastructures based on trusted third parties are designed according to coherent functional models.

We study a family of particular cosets of the first-order Reed-Muller code R(1,m): those generated by special codewords, the idempotents. Thus we obtain new maximal weight distributions of cosets of R(1,7) and 84 distinct almost maximal weight distributions of cosets of R(1,9), that is, with minimum weight 240. This leads to crypotographic applications in the context of stream ciphers.