Gilles Barthe
email: gilles.barthe@imdea.org

Xiong Fan
email: xfan@cs.cornell.edu

Joshua Gancher

Benjamin Grégoire
email: benjamin.gregoire@inria.fr

Charlie Jacomme
email: charlie.jacomme@lsv.fr

Elaine Shi
email: elaine@cs.cornell.edu

Symbolic Proofs for Lattice-Based Cryptography

Keywords: Security and privacy → Cryptography, Logic and verification, Symbolic proofs, provable security, lattice-based cryptography

ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

INTRODUCTION

Formal methods, and in particular formal verification, have long been used for building and checking mathematical claims of correctness or security for small but possibly very complex to moderately large and complex systems. In contrast to pen-and-paper counterparts, formally verified claims deliver higher assurance and independently verifiable proofs that can be replayed by third parties. Over the last 20 years, formal methods have been applied successfully to analyze the security of cryptographic protocols in the Dolev-Yao model [START_REF] Dolev | On the security of public key protocols[END_REF], an idealized model in which cryptographic constructions are treated algebraically. By abstracting away from the probabilistic nature of cryptographic constructions, the Dolev-Yao model has served as a suitable and practical foundation for highly or fully automated tools [START_REF] Armando | The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications[END_REF][START_REF] Blanchet | An Efficient Cryptographic Protocol Verifier Based on Prolog Rules[END_REF][START_REF] Schmidt | Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties[END_REF]]. These tools have subsequently been used for analyzing numerous cryptographic protocols, including recently TLS 1.3. [START_REF] Cremers | A Comprehensive Symbolic Analysis of TLS 1.3[END_REF][START_REF] Kobeissi | Automated Verification for Secure Messaging Protocols and Their Implementations: A Symbolic and Computational Approach[END_REF]. Unfortunately, the Dolev-Yao model is focused on cryptographic protocols and cannot be used for reasoning about cryptographic primitives. A related approach is to use so-called refinement types (a.k.a. logical assertions) for reasoning about implementations written in a functional programming language [START_REF] Swamy | Secure distributed programming with valuedependent types[END_REF]; this approach has also been used for analyzing TLS 1.3. [START_REF] Bhargavan | Implementing TLS with Verified Cryptographic Security[END_REF][START_REF] Delignat-Lavaud | Implementing and Proving the TLS 1.3 Record Layer[END_REF], but is also primarily limited to cryptographic protocols.

An alternative approach is to develop symbolic methods that reason directly in the computational model. This approach applies both to primitives and protocols, and instances of this approach have been instrumented in tools such as CertiCrypt [START_REF] Barthe | Formal certification of code-based cryptographic proofs[END_REF], CryptHOL [START_REF] Lochbihler | Probabilistic Functions and Cryptographic Oracles in Higher Order Logic[END_REF] CryptoVerif [START_REF] Blanchet | A Computationally Sound Mechanized Prover for Security Protocols[END_REF], EasyCrypt [START_REF] Barthe | EasyCrypt: A Tutorial[END_REF][START_REF] Barthe | Computer-Aided Security Proofs for the Working Cryptographer[END_REF], and FCF [START_REF] Petcher | The Foundational Cryptography Framework[END_REF] (see also [START_REF] Barthe | Computational indistinguishability logic[END_REF][START_REF] Impagliazzo | Logics for Reasoning about Cryptographic Constructions[END_REF] for further approaches not supported by tools). However, these tools require significant user interaction and expertise, in particular when used for reasoning about cryptographic primitives.

A promising approach for analyzing cryptographic primitives in the computational model is to combine computational logics and symbolic tools from the Dolev-Yao model. Prior work has demonstrated that this approach works well for padding-based (combining one-way trapdoor permutations and random oracles) [START_REF] Barthe | Fully automated analysis of padding-based encryption in the computational model[END_REF] and pairing-based cryptography [START_REF] Barthe | Automated Proofs of Pairing-Based Cryptography[END_REF]. Broadly speaking, computational logics formalize game-playing security proofs; each step of the proof corresponds to a hop, and symbolic side-conditions are used to ensure the validity of the hop. More specifically, computational logics, which can be seen as specializations of [START_REF] Barthe | Computational indistinguishability logic[END_REF], are used to capture computational security goals and to drive security proofs whereas side-conditions use symbolic tools such as deducibility and static equivalence to guarantee that the rules of the logic are applied correctly. In particular, a key idea of this approach is to use deducibility for controlling the application of rules for performing reductions to hardness assumptions, and for performing optimistic sampling, a particularly common and useful transformation which simplifies probabilistic experiments by allowing to replace, under suitable circumstances, sub-computations by uniform samplings.

The use of deducibility in side conditions, as opposed to arbitrary mathematical conditions, is a necessary step for automating application of proof rules, and more generally for automating complete proofs. However, the interest of this approach is conditioned by the ability to check the validity of deducibility problems. The problem of deciding deducibility has been studied extensively in the context of symbolic verification in the Dolev-Yao model, where deducibility formalizes the adversary knowledge [START_REF] Comon-Lundh | Intruder deductions, constraint solving and insecurity decision in presence of exclusive or[END_REF][START_REF] Kemmerer | Three systems for cryptographic protocol analysis[END_REF][START_REF] Lowe | Breaking and fixing the Needham-Schroeder Public-Key Protocol using FDR[END_REF][START_REF] Millen | Constraint Solving for Bounded-Process Cryptographic Protocol Analysis[END_REF][START_REF] Paulson | The Inductive Approach to Verifying Cryptographic Protocols[END_REF][START_REF] Rusinowitch | An NP Decision Procedure for Protocol Insecurity with XOR[END_REF][START_REF] Rusinowitch | Protocol insecurity with a finite number of sessions and composed keys is NP-complete[END_REF][START_REF] Schneider | Security Properties and CSP[END_REF]. This line of work has culminated in the design and implementations of decision procedures for classes of theories that either have some kind of normal form or satisfy a finite variant property. However, existing decidability results are primarily targeted towards algebraic theories that arise in the study of cryptographic protocols. In contrast, deducibility problems for cryptographic constructions require to reason about mathematical theories that may not have a natural notion of normal form or satisfy the finite variant property.

Thus, a main challenge for computational logics based on deducibility problems is to provide precise and automated methods for checking the latter. There are two possible approaches to address this challenge:

• heuristics: rather than deciding deducibility, one considers weaker conditions that are easier for verification. As demonstrated with AutoG&P, such an approach may work reasonably well in practice. However, it is not fully satisfactory. First, the heuristics may be incomplete and fail to validate correct instances. Second, advanced proof rules that perform multiple steps at once, and proof search procedures, which explores the space of valid derivations, become unpredictable, even for expert users. • (semi-)decision procedures based on computational mathematics: in this approach, one provides reductions from deducibility problems to computational problems in the underlying mathematical setting. Then, one can reuse (semi-)decision procedures for the computational problems to verify deducibility problems.

This approach offers some important advantages. First, it eliminates a potential source of incompleteness, and in particular the possibility that a proof step fails. Second, it is more predictable. Predictability is very important when a high level of automation is sought. Indeed, automation is often achieved through advanced tactics. When they involve multiple heuristics, the outcome of advanced tactics cannot be anticipated, which is a major hurdle to the adoption of formal verification tools. Third, it formalizes connections between known mathematical problems, which may have been extensively studied, and verification problems that may arise for the first time. Lastly, it encourages reusing existing algorithms and implementations.

The idea using methods from computational mathematics to reason about deducibility is natural. However, we are not aware of prior work that exploits this connection in relation with the use of deducibility in a computational logic.

Contributions

We propose symbolic methods for proving security of lattice-based cryptographic constructions. These constructions constitute a prime target for formal verification, due to their potential applications in post-quantum cryptography and their importance in the ongoing NIST effort to standardize post-quantum constructions; see e.g. [START_REF] Peikert | A Decade of Lattice Cryptography[END_REF] for a recent survey of the field.

In this paper, we define a logic for proving computational security of lattice-based cryptographic constructions. The logic follows the idea of combining computational proof rules with symbolic side-conditions, as in [START_REF] Barthe | Fully automated analysis of padding-based encryption in the computational model[END_REF][START_REF] Barthe | Automated Proofs of Pairing-Based Cryptography[END_REF]. One important feature of our logic is that the proof rule for assumptions supports information-theoretic and computational assumptions that are stated using adversaries with oracle accesses. This extension is critical to capture (advanced cases of) the Leftover Hash Lemma [START_REF] Impagliazzo | Pseudo-random Generation from one-way functions (Extended Abstracts)[END_REF]. The Leftover Hash Lemma is a powerful information-theoretical tool which allows to replace, under suitable conditions, a subcomputation by a sampling from a uniform distribution. The Leftover Hash Lemma is widely used in cryptographic proofs, in particular in the setting of lattice-based cryptography. We implement our logic in a tool called AutoLWE (https://github.com/autolwe/autolwe), and use the tool for proving (indistinguishability-based) security for several cryptographic constructions based on the Learning with Errors (LWE) assumption [START_REF] Regev | On lattices, learning with errors, random linear codes, and cryptography[END_REF].

More specifically, our examples include: dual Regev PKE [START_REF] Gentry | Trapdoors for hard lattices and new cryptographic constructions[END_REF], MP-PKE [START_REF] Micciancio | Trapdoors for Lattices: Simpler, Tighter, Faster, Smaller[END_REF], ABB-(H)IBE [START_REF] Agrawal | Efficient Lattice (H)IBE in the Standard Model[END_REF] and IPE [START_REF] Agrawal | Functional Encryption for Inner Product Predicates from Learning with Errors[END_REF]. All of our mechanized proofs are realistically efficient, running in at most three seconds (Fig. 12); efficiency in this setting is usually not an issue, since cryptographic constructions typically induce small instances of the deducibility problem. Recent progress on more advanced cryptographic constructions based on lattices, like attribute-based encryption [START_REF] Boneh | Fully Key-Homomorphic Encryption, Arithmetic Circuit ABE and Compact Garbled Circuits[END_REF] and predicate encryption [START_REF] Gorbunov | Predicate Encryption for Circuits from LWE[END_REF], are closely related to both the structure of the schemes and strategy in the proofs in [START_REF] Agrawal | Efficient Lattice (H)IBE in the Standard Model[END_REF][START_REF] Agrawal | Functional Encryption for Inner Product Predicates from Learning with Errors[END_REF][START_REF] Gentry | Trapdoors for hard lattices and new cryptographic constructions[END_REF]. The MP-PKE [START_REF] Micciancio | Trapdoors for Lattices: Simpler, Tighter, Faster, Smaller[END_REF] inspires development in some latticebased constructions, like homomorphic encryption [START_REF] Alperin | Faster Bootstrapping with Polynomial Error[END_REF] and deniable attribute-based encryption [START_REF] Daniel Apon | Deniable Attribute Based Encryption for Branching Programs from LWE[END_REF].

The technical core of our contributions are a set of (semi-)decision procedures for checking deducibility in the theory of Diffie-Hellman exponentiation, in its standard, bilinear and multilinear versions, and in the theories of fields, non-commutative rings, and matrices. In particular, we give decision procedures for checking deducibility in the theory of Diffie-Hellman exponentiation. This procedure has immediate applications to reasoning about security of cryptographic constructions based on bilinear and multilinear maps. The central idea behind our algorithm is to transform a deducibility problem into a problem from commutative algebra. The latter can be resolved through standard computations of Gröbner basis. Furthermore, we give a semi-decision procedure for checking deducibility in the theory of matrices. This has immediate applications to reasoning about security of lattice-based constructions. In this case, our algorithm extracts from a deducibility question a problem from non-commutative algebra. The problem can be resolved through semi-decision procedures based on non-commutative variants of Gröbner bases known as Subalgebra Analog of Gröbner Basis on Ideals (SAGBI) [START_REF] Nordbeck | Canonical Subalgebraic Bases in Non-commutative Polynomial Rings[END_REF].

EXAMPLE: DUAL REGEV ENCRYPTION

In this section, we describe an example public-key encryption scheme and show how it will be encoded in our formal system. We provide some mathematical background in Section 5.2. Recall that a public-key cryptosystem is given by three probabilistic algorithms (Setup, Enc, Dec) for generating keys, encryption, and decryption, such that with overwhelming probability, decryption is the inverse of encryption for valid key pairs. We consider the Dual Regev Encryption scheme [START_REF] Gentry | Trapdoors for hard lattices and new cryptographic constructions[END_REF], an optimization of Regev's original encryption [START_REF] Regev | On lattices, learning with errors, random linear codes, and cryptography[END_REF]. We focus on a simple version that encrypts single bits; however, standard techniques can be used to encrypt longer messages. Definition 2.1 (Dual Regev Encryption). Below, let λ = n be the security parameter, m = O (n log q), q = O (m) and χ (or χ n ) be discrete Gaussian distribution over Z (or Z n ).

• The key generation algorithm, KeyGen(1 λ ), chooses a uniformly sampled random matrix A ∈ Z n×m q and a vector r ∈ {-1, 1} m sampled uniformly, interpreted as a vector in Z m q . The public key is pk = (A, u), where u = Ar , and the secret key is sk = r .

• To encrypt a message b ∈ {0, 1}, the encryption algorithm Enc(pk, b) chooses a random vector s ∈ Z n q , a vector x 0 sampled from χ n and an integer x 1 sampled from χ . The ciphertext consists of the vector c 0 = s T A + x T 0 and the integer c 1 = s T u + x 1 + b ⌈q/2⌉, where T denotes the transpose operation on matrices.

• The decryption algorithm checks whether the value c 1 -⟨r , c 0 ⟩ is closer to 0 or b ⌈q/2⌉ modulo p, and returns 0 in the first case, and 1 in the second.

Decryption is correct with overwhelming probability, since we compute that c 1 -⟨r , c 0 ⟩ = x 1 + b ⌈q/2⌉ -⟨r, x 0 ⟩, so the norm of the term x 1 -⟨r , x 0 ⟩ will be much smaller than b ⌈q/2⌉.

Gentry, Peikert and Vaikuntanathan [START_REF] Gentry | Trapdoors for hard lattices and new cryptographic constructions[END_REF] show that Dual Regev Encryption achieves chosen-plaintext indistinguishability under the decisional LWE assumption, defined below. Traditionally, chosenplaintext indistinguishability is modeled by a probabilistic experiment, where an adversary proposes two messages m 0 and m 1 , and is challenged with a ciphertext c ⋆ corresponding to an encryption of message m b , where b is sampled uniformly at random. The adversary is then requested to return a bit b ′ . The winning condition for the experiment is b = b ′ , which models that the adversary guesses the bit b correctly. Formally, one defines the advantage of an adversary A against chosen-plaintext security as:

Adv cpa A = Pr G [ b = b ′ ] - 1 2
where G is the probabilistic experiment that models chosen-plaintext security and 1 2 represents the probability that a trivial adversary which flips a coin b ′ at random guesses the bit b correctly. We note that in our case, since the message space is {0, 1}, we can wlog set m 0 = 0 and m 1 = 1; thus, the adversary only needs to be queried once in this experiment.

The formal definition of G, instantiated to Dual Regev Encryption, is shown in Figure 1. We inline the key generation and encryption subroutines. In line 1, the public key (A, u) and its associated secret key r are randomly sampled. In lines 2 and 3, the message bit b is sampled uniformly, and the ciphertext (c 0 , c 1 ) of this message is generated. Finally, in line 4, the adversary outputs a bit b ′ , given as input the public key and the ciphertext. Now, we outline the hardness assumptions and lemmas used in the proof of Dual Regev Encryption.

Learning with Errors. The Learning With Errors (LWE) assumption [START_REF] Regev | On lattices, learning with errors, random linear codes, and cryptography[END_REF] is a computational assumption about the hardness of learning a linear function from noisy samples. We make use of the decisional variant, in which one distinguishes a polynomial number of "noisy" inner products with a secret vector from uniform.

Definition 2.2 (LWE). Let n, m, q, and χ be as in Definition 2.1. Given s ∈ Z n q , let LWE s, χ (dubbed the LWE distribution) be the probability distribution on Z n×m q × Z m q obtained by sampling A ∈ Z n×m q at uniform, sampling e from χ n , and returning the pair (A, s T A+e).

The decision-LWE q,n,m, χ problem is to distinguish LWE s, χ from uniform, where s is uniformly sampled.

We say the decision-LWE q,n,m, χ problem is infeasible if for all polynomial-time algorithms A, the advantage Adv lwe A (1 λ ) is negligibly close to 1/2 as a function of λ:

Adv lwe A (1 λ ) = |Pr[A solves LWE] -1/2|
The works of [START_REF] Brakerski | Classical hardness of learning with errors[END_REF][START_REF] Peikert | Public-key cryptosystems from the worst-case shortest vector problem: extended abstract[END_REF][START_REF] Regev | On lattices, learning with errors, random linear codes, and cryptography[END_REF] show that the LWE assumption is as hard as (quantum or classical) solving GapSVP and SIVP under various settings of n, q, m and χ .

Leftover Hash Lemma. Let A ∈ Z n×m q be a collection of m samples of uniform vectors from Z n q . The Leftover Hash Lemma (LHL) states that, given enough samples, the result of multiplying A with a random {-1, 1}-valued matrix R is statistically close to uniform. Additionally, this result holds in the presence of an arbitrary linear leakage of the elements of R. Specifically, the following leftover hash lemma is proved in [START_REF] Agrawal | Efficient Lattice (H)IBE in the Standard Model[END_REF] (Lemma 13). Lemma 2.3 (Leftover Hash Lemma). Let q, n, m be as in Definition 2.1. Let k be a polynomial of n. Then, the distributions {(A, AR, R T w)}

{(A, B, R T w)} are negligibly close in n, where A $ ← -Z n×m q in both dis- tributions, R $ ← -{0, 1} m×k , B $ ← -Z n×k
q , and w ∈ Z m q is any arbitrary vector.

Given the above, security of Dual Regev Encryption is stated as follows: Proposition 2.4 ( [START_REF] Gentry | Trapdoors for hard lattices and new cryptographic constructions[END_REF]). For any adversary A against chosenplaintext security of Dual Regev Encryption, there exists an adversary B against LWE, such that:

Game G pke org : A $ ← Z n×m q , r $ ← {-1, 1} m ; let u = Ar ; b $ ← {0, 1}, s $ ← Z n q , x 0 $ ← D Z m , x 1 $ ← D Z ; let c 0 = s T A + x 0 , c 1 = s T u + x 1 + b ⌈q/2⌉; b ′ ← A(A, u, c 0 , c 1 );
• Adv cpa A ≤ Adv lwe B + ϵ LH L ; • t A ≈ t B ;
where Adv lwe B denotes the advantage of B against decisional LWE problem, ϵ LH L is a function of the scheme parameters determined by the Leftover Hash Lemma, and t A and t B respectively denote the execution time of A and B.

Security proof. We now outline the proof of Proposition 2.4. The proof proceeds with a series of game transformations, beginning with the game in Figure 1. The goal is to transform the game into one in which the adversary's advantage is obviously zero. Each transformation is justified semantically either by semantic identities or by probabilistic assertions, such as the LWE assumption; in the latter case, the transformation incurs some error probability which must be recorded.

The first transformation performs an information-theoretic step based on the Leftover Hash Lemma. The Leftover Hash Lemma allows us to transform the joint distribution (A, Ar ) (where A and r are independently randomly sampled) into the distribution (A, u) (where u is a fresh, uniformly sampled variable). (This invocation does not use the linear leakage w from Lemma 2.3). In order to apply this lemma, we factor the security game from Figure 1 into one which makes use of A and u, but not r . That is, if G 0 is the original security game, then we have factored G into

G 0 = G ′ {A ← $ Z n×m q ; r ← $ {-1, 1} m ; let u = Ar } p ,
where G ′ {•} p is a game context with a hole at position p, such that G ′ does not make reference to r except in the definition of u. By the Leftover Hash Lemma, we may now move to the game:

G 1 = G ′ {A ← $ Z n×m q ; u ← $ Z n q } p .
This transformation effectively removes r from the security game, thus removing any contribution of the secret key r to the information gained by the adversary A. This transformation incurs the error probability ϵ LH L . The resultant game is shown in Figure 2. The second transformation performs a reduction step based on the LWE assumption. Indeed, note that after the first transformation, the ciphertexts (c 0 , c 1 ) contain an LWE distribution of dimension n × (m + 1), with the message bit added to c 1 . By applying LWE, we then may safely transform c 0 to be uniformly random, and c 1 to be uniformly random added to to the message bit. The resulting security game is shown in Figure 3. The next transformation applies a semantics-preserving transformation known as optimistic sampling. To remove the message bit from the adversary input, note that the term c 1 is equal to the sum of r 1 and b ⌈q/2⌉, where r 1 is uniformly sampled and does not appear anywhere else in the game. Because of this, we know that c 1 itself is uniformly random. Thus, we can safely rewrite the body of c 1 to be equal to a fresh uniformly sampled r 1 . The resulting game is shown in Figure 4. In this final game, there is no dependence between the challenge given to the adversary and the challenge b, so the probability that the adversary guesses b is upper bounded by 1 2 . The most important point about the above proof is that while the cryptographic theory underlying the Leftover Hash Lemma and Learning with Errors assumption is in nature analytic, the proof of security which uses them is only algebraic. That is, no complicated analytic arguments must be made in order to carry out the above proof; instead, each transformation is a straightforward syntactic transformation of the security game.

Game G 2 : A $ ← Z n×m q , u $ ← Z n q ; b $ ← {0, 1}, s $ ← Z n q , x 0 $ ← D Z m , x 1 $ ← D Z ; let c 0 = s T A + x 0 , c 1 = s T u + x 1 + b ⌈q/2⌉; b ′ ← A(A, u, c 0 , c 1 );
Game G 3 : A $ ← Z n×m q , u $ ← Z n q ; b $ ← {0, 1}, r 0 $ ← Z m q , r 1 $ ← Z q ; let c 0 = r 0 , c 1 = r 1 + b ⌈q/2⌉; b ′ ← A(A, u, c 0 , c 1 );
Game G 4 : A $ ← Z n×m q , u $ ← Z n q ; b $ ← {0, 1}, r 0 $ ← Z m q , r 1 $ ← Z q ; let c 0 = r 0 , c 1 = r 1 ; b ′ ← A(A, u, c 0 , c 1 );
Our logic is designed to handle game transformations such as the ones in the above proof. Our implemented security proof for Dual Regev Encryption is shown in Figure 5. In lines 1-3, we apply the Leftover Hash Lemma. The move tactic is used to reorder samplings in the security game, as long as the two reorderings are semantically equivalent. The assumption_decisional tactic is used to apply hardness assumptions and information-theoretic lemmas. Note that all required factorings of games in this proof are performed automatically, handled by our use of the SAGBI method in Section 4.3. This is reflected by the "!" at the end of the tactic, which asks the proof system to automatically factor the game. (More complicated applications of assumption_decisional do require the user to provide some hints to the proof system about how to factor the game. These hints are minimal, however.) The arrow -> after the tactic specifies that we wish to apply the transformation in the forward direction. (It is possible to apply the LHL and the LWE assumption in reverse, as well. This is used in later proofs.) Throughout, we use the // tactic to normalize the game. This tactic unfolds let bindings, and applies a syntactic normal form algorithm to all expressions in the game. The mat_fold and mat_unfold tactics are used to reason about uniformity of matrices of the form Z n×(m+k ) q : the mat_unfold tactic will separate a uniform sampling of type Z n×(m+k ) q into two uniform samplings of types Z n×m q and Z n×k q respectively; the mat_fold does the corresponding inverse operation.

The rnd tactic is used to reason about transformations of uniform samplings: given two functions f , f -1 which must be mutual inverses, the rnd tactic allows one to "pull" a uniform sampling through f -1 . This is used in two ways in the proof: on lines 13 and 15, we use rnd to show that instead of sampling a matrix, we may instead sample its transpose. Whenever the original matrix is used, we now take the transpose of the new sampled matrix. Similarly, on line 19 we use rnd to perform an optimistic sampling operation, in which B is transformed in order to remove the additive factor b?Mu(()):0_{1,1}. Here, Mu is an uninterpreted function from the unit type to 1 by 1 matrices, modelling the message content ⌈q/2⌉, and 0_{1,1} is the constant zero matrix of dimension 1 by 1. The notation _?_:_ is the standard ternary if-then-else construct; thus, we can model the expression b ⌈q/2⌉ present in the Dual Regev scheme as the expression b?Mu(()):0_{1,1}.

Finally, the indep! tactic is used to reason about games such as the game in Figure 4, in which the adversary trivially has no advantage. Detail about the proof rules present in our logic is given in Section 3.4.

LOGIC

Our logic reasons about probabilistic expressions P, built from atomic expressions of the form Pr G [ ϕ ], where G is a game, and ϕ is an event. Games are probabilistic programs with oracle and adversary calls, and ϕ is the winning condition of the game. The proof rules of the logic formalize common patterns of reasoning from the game-playing approach to security proofs. In their simpler form, proof steps will transform a proof goal Pr G [ ϕ ] ≤ p into a

Dimensions d ::= n dimension variable | d 1 + d 2 addition | 1 constant dimension 1 Types t ::= B boolean value | Z q prime field of order q | Z d 1 ×d 2 q integer matrix | list d t list | t × . . . × t tuple Expressions M ::= 0 null matrix | I identity matrix | [M] constant list | M + M addition | M × M multiplication | -M inverse | M ∥ M concatenation | sl M left projection | sr M right projection | M ⊤ transpose Figure 6: Syntax of expressions (selected) proof goal Pr G ′ [ ϕ ′ ] ≤ p ′ , with p = p ′ + c,
= let x = e assignment | x ← $ µ sampling from distr. | assert(ϕ) assertion | y ← A(x ) with - → O adversary call Oracle commands oc ::= let x = e assignment | x ← $ µ sampling from distr. | guard(b) guard Oracle definitions O ::= o(x ) = { - → oc; return e} Game definitions G ::= { - → дc; return e}; - → O
where A and O range over adversary and oracle names respectively.

Figure 7: Syntax of games includes vectors and matrices; new rules for probabilistic samplings and for oracle-relative assumptions (both in the informationtheoretic and computational forms). These extensions do not pose any foundational challenge, but must be handled carefully to obtain the best trade-off between generality and automation.

Games

Games consist of a security experiment in which an adversary with oracle access interacts with a challenger and of an assertion that determines the winning event.

Expressions. The expression language operates over booleans, lists, matrices, and integers modulo q, and includes the usual algebraic operations for integer modulo q and standard operators for manipulating lists and matrices. The operations for matrices include addition, multiplication and transposition, together with structural operations that capture the functionalities of block matrices, and can be used for (de)composing matrices from smaller matrices. concatenation, split left, and split right. The type of lists, list d , denotes a list of length d. Lists are manipulated symbolically, so do not support arbitrary destructuring. Lists may be constructed through the constant list operation [•], which takes a type τ to the type list d τ , for any d. All of the matrix operations are lifted pointwise to lists.

The syntax of expressions (restricted to expressions for matrices) is given in Figure 6. Selected typing rules for expressions are given in the Appendix, in Figure 13. Expressions are deterministic, and are interpreted as values over their intended types. Specifically, we first interpret dimensions as (positive) natural numbers. This fixes the interpretation of types. Expressions are then interpreted in the intended way; for instance, transposition is interpreted as matrix transposition, etc.

Games. Games are defined by a sequence of commands (random samplings, assignments, adversary calls) and by an assertion. The command defines the computational behavior of the experiment whereas the assertion defines the winning event. Each adversary call contains a list of oracles that are available to the adversary; oracles are also defined by a sequence of commands (random samplings, assignments, assert statements) and by a return expression. The grammars for oracle definitions and game definitions are given in Figure 7.

The operational behavior of oracles is defined compositionally from the operational behavior of commands:

• random sampling x ← $ µ: we sample a value from µ and store the result in the variable x; • assignments: let x = e: we evaluate the expression e and store the result in the variable x; • assertion guard(b): we evaluate b and return ⊥ if the result is false. Guards are typically used in decryption oracles to reject invalid queries.

In addition, we assume that every oracle O comes with a value δ O that fixes the maximal number of times that it can be called by an adversary. To enforce this upper bound, the execution is instrumented with a counter c O that is initially set to 0. Then, whenever the oracle is called, one checks c O ≥ δ o ; if so, then ⊥ is returned. Otherwise, the counter c O is increased, and the oracle body is executed. In order to interpret events, we further instrument the semantics of the game to record the sequence of interactions between the adversary and the oracle. Specifically, the semantics of oracles is instrumented with a query set variable Q O that is initially set to ∅. Then, for every call the query parameters are stored in Q O . (Following [START_REF] Barthe | Computational indistinguishability logic[END_REF] it would be more precise to hold a single list of queries, rather than a list of queries per oracle, but the latter suffices for our purposes.) Informally, adversaries are probabilistic computations that must execute within a specific amount of resources and are otherwise arbitrary. One simple way to give a semantics to adversaries is through syntax, i.e. by mapping adversary names to commands, and then interpret these commands using the afore described semantics. However, our language of games is too restrictive; therefore, we map adversary names to commands in a more expressive language, and then resort to the semantics of this richer language. For convenience of meta-theoretic proofs, e.g. soundness, it is preferable to choose a language that admits a set-theoretical semantics. For instance, one can use the probabilistic programming language pWhile to model the behavior of the adversaries.

The semantics of games is defined compositionally from the operational behavior of commands, oracles, and adversaries: • assertion assert(ϕ): we evaluate ϕ and abort if the result is false.

• adversary call y ← A (e) with -→ O: we evaluate e, call the adversary A with the result as input, and bind the output of the adversary to y. The adversary is provided with access to the oracles

- → O.
Finally, the interpretation of Pr G [ ϕ ] is to be the probability of ϕ in the sub-distribution obtained by executing G.

Throughout the paper, we assume that the games satisfy the following well-formedness conditions and (without loss of generality) hygiene conditions: (WF1) all variables must be used in scope; (WF2) commands must be well-typed; (Hyg1) adversary and oracle names are distinct; (Hyg2) bound variables are distinct.

Reasoning about expressions

Our indistinguishability logic makes use of two main relations between expressions: equality and deducibility. Equality is specified through a set of axioms E, from which further equalities can be derived using standard rules of equational reasoning: reflexivity, symmetry, transitivity of equality, functionality of operators, and finally instantiation of axioms. We write Γ ⊢ E e = e ′ if e and e ′ are provably equal from the axioms E and the set of equalities Γ. Throughout the paper, we implicitly assume that the set of axioms includes standard identities on matrices.

Deducibility is defined using the notion of contexts. A context C is an expression that only contains a distinguished variable

M + N , O, N ⊢ M × O with the context C (• 1 , • 2 , • 3 ) := (• 1 -• 3 ) × •2.

Strongest postcondition

A desirable property of any logic is that one can replace equals by equals. In particular, it should always be possible to replace an expression e by an expression e ′ that is provably equivalent to e. However, it is often desirable to use a stronger substitution property which allows to replace e by an expression e ′ that is provably equivalent to e relative to the context in which the replacement is to be performed. To achieve this goal, our proof system uses a strongest postcondition to gather all facts known at a position p in the main command. The computation of sp p (G) is done as usual, starting from the initial position of the program with the assertion true and adding at each step the assertion ϕ c corresponding to the current command c, where:

ϕ let x = e = x = e ϕ guard(b ) = b ϕ assert(e ) = e ϕ ∀/∃ b 1 , ...,b k . e = true

Judgment and proof rules

Our computational logic manipulates judgments of the form P ⪯ P ′ where P and P ′ are probability expressions drawn from the following grammar:

P, P ′ ::= ϵ | c | P + P ′ | P -P ′ | c × P | |P | | Pr G [ ϕ ],
where ϵ ranges over variables, c ranges over constants, |P | denotes absolute value, and Pr G [ ϕ ] denotes the success probability of event ϕ in game G. Constants include concrete values, e.g. 0 and 1 2 , as well as values whose interpretation will depend on the parameters of the scheme and the computational power of the adversary, e.g. its execution time or maximal number of oracle calls.

Proof rules are of the form

P 1 ⪯ ϵ 1 . . . P k ⪯ ϵ k P ⪯ ϵ
where P i s and P are probability expressions, ϵ i s are variables and finally ϵ is a probability expression built from variables and constants. Figure 8 present selected rules of the logic. In many cases, rules consider judgments of the form Pr G [ ϕ ] ⪯ ϵ; similar rules exist for judgments of the form Pr

G [ ϕ ] -Pr G ′ [ ϕ ′ ] ⪯ ϵ.
Rules [False] and [Case] formalize elementary axioms of probability theory. Rules [Refl] and [Add] formalize elementary facts about real numbers. Rule [Eq] can be used to replace a probability expression by another probability expression that is provably smaller within the theory of reals. For instance, derivations commonly use the identity

ϵ 1 ≤ |ϵ 1 -ϵ 2 | + ϵ 2 .
Rules [Swap], [Insert], [Subst] are used for rewriting games in a semantics-preserving way. Concretely, rule [Swap] swaps successive commands (at position p) that can be reordered (are dataflow independent in the programming language terminology). By chaining applications of the rule, one can achieve more general forms of code motion. Rule [Insert] inserts at position p command that does not carry any operational behaviour. Rule [Subst] substitutes at position p an expression e by another expression e ′ that is contextually equivalent at p, i.e. sp p (G) |= e = E e ′ holds.

The rule [Rand] performs a different transformation known as optimistic sampling. It replaces a uniform sampling from t by s ← $ t ′ ; return C[s]. To ensure that this transformation is correct, the rule checks that C is provably bijective at the program point where the transformation arises, using a candidate inverse context C ′ provided by the user. Rules [RFold] and [RUnfold] are dual and are used to manipulate random samplings of matrices. The rule [RFold] is used to turn two uniform samplings of matrices into one uniform sampling of the concatenation; conversely, the rule [RUnfold] may be used to turn one uniform sampling of a concatenation into uniform samplings of its component parts. (We also have similar rules [LFold] and [LUnfold] in order to manipulate the vertical component of the dimension.) These rules are primarily used to apply axioms which are stated about matrices of compound dimension.

The rule [Abstract] is used for applying computational assumptions. The rule can be used to instantiate a valid judgment with a concrete adversary. The side-conditions ensure that the experiments G 1 and G 2 are syntactically equivalent to the experiment The rule [Upto] rule is used for replacing guard(c ′ ) at position p in an oracle with guard(c). According to the usual principle for reasoning up to failure events, the rule yields two proof obligations: bound the probability of the original event and the probability that the adversary performs a query where the results of c and c ′ differ.

[False] Pr G [ false ] ⪯ 0 [Case] Pr G [ ϕ ∧ c ] ⪯ ϵ 1 Pr G [ ϕ ∧ ¬c ] ⪯ ϵ 2 Pr G [ ϕ ] ⪯ ϵ 1 + ϵ 2 [Refl] Pr G [ ϕ ] ⪯ Pr G [ ϕ ] [Add] P ⪯ ϵ 1 P ′ ⪯ ϵ 2 P + P ′ ⪯ ϵ 1 + ϵ 2 [Eq] P ⪯ ϵ ⊢ P ′ ≤ P P ′ ⪯ ϵ [Swap] Pr G {c ′ ; c } p [ ϕ ] ⪯ ϵ Pr G {c; c ′ } p [ ϕ ] ⪯ ϵ [Insert] Pr G {c; c ′ } p [ ϕ ] ⪯ ϵ Pr G {c ′ } p [ ϕ ] ⪯ ϵ c sampling, let, or guard(true) [Subst] Pr G {e } p [ ϕ ] ⪯ ϵ Pr G {e ′ } p [ ϕ ] ⪯ ϵ sp p (S E ) |= e = E e ′ [Abstract] Pr G ′ 1 [ ϕ 1 ] -Pr G ′ 2 [ ϕ 2 ] ⪯ ϵ Pr G 1 [ ϕ 1 ] -Pr G 2 [ ϕ 2 ] ⪯ ϵ G 1 ≡ G ′ 1 [B] G 2 ≡ G ′ 2 [B] [Rand] Pr G {s← $ t ′ ; let r = C[s]} p [ ϕ ] ⪯ ϵ Pr G {r ← $ t } p [ ϕ ] ⪯ ϵ sp p (G ) |= C ′ [C] = E • [RFold] Pr G {x ← $ Z d 1 ×(d 2 +d ′ 2 ) q ; let x 1 = sl x ; let x 2 = sr x } p [ ϕ ] ⪯ ϵ Pr G {x 1 ← $ Z d 1 ×d 2 q ; x 2 ← $ Z d 1 ×d ′ 2 q } p [ ϕ ] ⪯ ϵ [RUnfold] Pr G {x 1 ← $ Z d 1 ×d 2 q ; x 2 ← $ Z d 1 ×d ′ 2 q ; let x = x 1 ∥x 2 } p [ ϕ ] ⪯ ϵ Pr G {x ← $ Z d 1 ×(d 2 +d ′ 2 ) q } p [ ϕ ] ⪯ ϵ [Upto] Pr G {guard(c ) } p [ ϕ ] ⪯ ϵ 1 Pr G {guard(c ) } p [ ∃ x ∈ Q o . c (x ) c ′ (x ) ] ⪯ ϵ 2 Pr G {guard(c ′ ) } p [ ϕ ] ⪯ ϵ 1 + ϵ 2 p first position in o [Guess] Pr G; x ←A () [ ϕ ] ⪯ ϵ Pr G [ ∃ x ∈ Q o . ϕ ] ⪯ ϵ [Find] Pr G; x ←A ) [ ϕ 1 ∧ ϕ 2 ] ⪯ ϵ Pr G [ (∃ x ∈ Q o . ϕ 1 ) ∧ ϕ 2 ] ⪯ ϵ C efficient and sp |G | (G ) |= C[(e, x )] = E ϕ 1
The rules [Guess] and [Find] rules are used to deal with winning events involving existential quantification.

The logic also contains a rule for hybrid arguments. The rule is similar to [START_REF] Barthe | Automated Proofs of Pairing-Based Cryptography[END_REF] and omitted For lack of space.

Soundness

All proof rules of the logic are sound. To state soundness, we lift the interpretation of games to an interpretation of judgments and derivations. This is done by first defining a fixed interpretation of dimensions that is used for all the games of the derivation. Then, we define the interpretation of P inductively. We say that judgment P ⪯ P ′ is valid iff the inequality holds for every valid interpretation of P and P ′ . Finally, one can prove that P ⪯ P ′ is valid whenever P ⪯ P ′ is derivable in the logic.

Axioms Used

Here, we describe the axioms used to prove the schemes in Sections 2 and 5 secure. Each axiom is decisional, in that it is a claim about the closeness of two games. This is modeled by having both games end with a bit output b, so that each axiom is a claim of the form

Pr G 0 [ b ] -Pr G 1 [ b ] ⪯ ϵ.
This allows us to apply the [Abstract] rule from Figure 8.

3.6.1 Learning with Errors. Recall from Section 2 that the LWE assumption states that the distribution (A, s T A +e) is indistinguishable from uniform, where A and s are uniformly sampled elements of Z n×m q and Z n q respectively, and e is sampled from some given error distribution.

Our concrete encoding is given in Figure 9. Since our logic only deals with uniform samplings, in order to encode more complicated sampling algorithms such as the error distribution for LWE, we separate the sampling algorithm into a coin sampling stage and a deterministic stage. In the coin sampling stage, an element of {0, 1} c is sampled, where c is the number of coins the sampling algorithm will use. (Since the sampling algorithm is polynomial time, c will be a polynomial of the security parameter.) In the deterministic stage, we call an uninterpreted function (here, Chi) which uses the sampled coins to produce the output of the distribution.

In various applications of the LWE assumption, the parameter settings of Figure 9 will alter slightly -for instance, in the Dual Regev scheme from Section 2, we do not use m on the nose, but rather m + 1. This difference is immaterial to the validity of the assumption.

Game G LW E 0 : A $ ← Z n×m q ; s $ ← Z n q ; c e $ ← {0, 1} c Chi ; let e = Chi(c e ); b ← A(A, s T A + e); Game G LW E 1 : A $ ← Z n×m q ; u $ ← Z m q ; b ← A(A, u);
3.6.2 Leftover Hash Lemma. The most subtle part of our proofs is often not applying the LWE assumption, but rather applying the Leftover Hash Lemma. This is because the LHL is an informationtheoretic judgment rather than a computational one; informationtheoretic judgments enjoy stronger composition properties than computational judgments.

Recall that the (basic) LHL states that the distribution (A, AR, wR) is statistically close to the distribution (A, B, wR), where A is a uniformly random element of Z n×m q , R is a uniformly random element of {-1, 1} m×k (interpreted as a matrix), and w is a fixed arbitrary vector in Z m q . For the LHL to hold, however, we can actually relax the requirements on A: instead of A being sampled uniformly, we only require that A is sampled from a distribution which is statistically close to uniform.

In the literature, it is often the case that the lemma being applied is not the LHL on the nose, but rather this weakened (but still valid) form in which A only need to be close to uniform. In many of our proofs, this occurs because A is not uniformly sampled, but rather sampled using an algorithm, TrapGen, which produces a vector A statistically close to uniform along with a trapdoor T A , which is kepts secret from the adversary.

By combining the LHL with the TrapGen construction, we obtain the security games in Figure 10. Both games are displayed at once: the expressions which vary between the two games are annotated with which game they belong in. In order to model how R is sampled, we sample the component bits of R from {0, 1} d LH L , and apply a symbolic function, bitinj, which converts these component bits into a matrix. Note in this security game that w comes from a symbolic adversary, A 1 . This models the universal quantification of w in the LHL. Additionally, note that A 2 actually receives the trapdoor T A . This is counterintuitive, because adversaries in the cryptosystems do not have access to the trapdoor. However, remember that here we are constructing the adversary for the LHL; giving A 2 the trapdoor reflects the assertion that the distribution (A, AR, wR,T A ) is statistically close to the distribution (A, B, wR,T A ), which follows from the information theoretic nature of the LHL.

While we use the assumption from Figure 10 in our proofs, we also use several small variations which are also valid. One such variation is in the proof of Dual Regev, where we do not use the TrapGen algorithm, but rather sample A uniformly (and do not give the adversary T A ); additionally, we do not include this linear leakage w. Another such variation is used in our CCA proof from Section 5. In this instance, we do not transform AR to B, but rather

Game G LH L β : c $ ← {0, 1} d T G ; let (A,T A ) = TrapGen(c); r $ ← {0, 1} d LH L ; let R = bitinj(r ); if β =1 B $ ← Z n×m q ; w ← A 1 (); b ← A 2 (A, if β =0 AR if β =1
B , wR,T A , w); to AR + B (thus generalizing our [Rand] rule.) Additionally, we must state the LHL in the CCA proof to be relative to the decryption oracle, which makes use of R. This relativized lemma is still valid, however, since the decryption oracle does not leak any information about R. It will be interesting future work in order to unify these small variations of the LHL.

Distribution Equivalences.

In addition to the two main axioms above, we also rely on several opaque probabilistic judgments about distributions from which the adversary may sample, but are written in terms of private variables which the adversary may not access. For instance, in an Identity-Based Encryption scheme, the adversary could have access to a KeyGen oracle, which must use the master secret key in order to operate. This is the case in Section 5.2. In the concrete proof, there is a step in which we change the implementation of the KeyGen oracle from one uninterpreted function to another. Transformations of this sort are encoded using oracle-relative assumptions, which are generalizations of axioms in AutoG&P which allow adversaries to query oracles.

For example, in Figure 11, we state closeness of the distributions D 0 (s 0 , •) and D 1 (s 1 , •), where both s 0 and s 1 are unknown to the adversary. (As before, each distribution is separated into a coin sampling stage and a deterministic stage.) Note that s 0 and s 1 need not be of the same type, since the adversary does not see them. Jumping ahead in (H)IBE part in the case study, D 0 , D 1 correspond to the real/simulated key generation algorithms, where s 0 is the master secret key, and s 1 is the secret trapdoor information the simulator knows in order to answer secret key queries.

DECIDING DEDUCIBILITY

Several rules involve deducibility problems as side-conditions. For instance, in the [Abstract] rule from Fig 8, we may transform a bound involving G 1 and G 2 into a bound involving G ′ 1 and G ′ 2 , if there exists a common subgame B which can be used to factor the former pair into the latter. Finding this subgame B will induce deducibility subproblems. In order to automate the application of the rules, it is thus necessary to provide algorithms for checking whether deducibility problems are valid. As previously argued, it is desirable whenever possible that these algorithms are based on decision procedures rather than heuristics.

Game G 0 : In this section, we provide decision procedures for the theory of Diffie-Hellman exponentiation, both in its basic form and in its extension to bilinear groups, and for the theory of fields. The decision procedures for Diffie-Hellman exponentiation are based on techniques from Gröbner bases. In addition to being an important independent contribution on its own, the algorithms for Diffie-Hellman exponentiation also serve as a natural intermediate objective towards addressing the theory of matrices (although the problems are formally independent). For the latter, we require significantly more advanced algebraic tools. For the clarity of exposition, we proceed incrementally. Concretely, we start by considering the case of fields and non-commutative rings. We respectively provide a decision procedure and a semi-decision procedure. Subsequently, we give a reduction from deducibility for matrices to deducibility for non-commutative rings. The reduction yields a semi-decision procedure for matrices. The algorithms for non-commutative rings and matrices are based on so-called SAGBI [START_REF] Robbiano | Subalgebra bases[END_REF] (Subalgebra Analog to Gröbner Basis for Ideals) techniques, which as justified below provide a counterpart of Gröbner basis computations for subalgebras.

s 0 $ ← Z m q ; b ← A() with O (x ) = { c 0 $ ← {0, 1} d 0 ; ret D 0 (c 0 , s 0 , x ); } Game G 1 : s 1 $ ← Z k q ; b ← A() with O (x ) = { c 1 $ ← {0, 1} d 1 ; ret D 1 (c 1 , s 1 , x ); }

Diffie-Hellman exponentiation

Diffie-Hellman exponentiation is a standard theory that is used for analyzing key-exchange protocols based on group assumptions. It is also used, in its bilinear and multilinear version, in AutoG&P for proving security of pairing-based cryptography. In this setting, the adversary (also often called attacker in the symbolic setting) can multiply groups elements between them, i.e perform addition in the field, and can elevate a group element to some power he can deduce in the field. Previous work only provides partial solutions: for instance, Chevalier et al [START_REF] Chevalier | Deciding the Security of Protocols with Diffie-Hellman Exponentiation and Products in Exponents[END_REF] only consider products in the exponents, whereas Dougherty and Guttman [START_REF] Daniel | Decidability for Lightweight Diffie-Hellman Protocols[END_REF] only consider polynomials with maximum degree of 1 (linear expressions).

The standard form of deducibility problems that arises in this context is defined as follows: let Y be a set of names sampled in Z q , д some group generator, E the equational theory capturing field and groups operations, some set X ⊂ Y , f 1 , ...f k , h ∈ K[Y ] be a set of polynomials over the names, and Γ be a coherent set of axioms. The deducibility problem is then: The algorithm that supports the proof of the proposition proceeds by reducing an input deducibility problem to an equivalent membership problem of the saturation of some Z q [X ]-module in Z q [Y ], and by using an extension for modules [START_REF] Eisenbud | Commutative Algebra: with a view toward algebraic geometry[END_REF] of Buchberger's algorithm [START_REF] Buchberger | A Theoretical Basis for the Reduction of Polynomials to Canonical Forms[END_REF] to solve the membership problem.

Γ |= X , д f 1 , ..., д f k ⊢ E д h
The reduction to the membership problem proceeds as follows: first, we reduce deducibility to solving a system of polynomial equations. We then use the notion of saturation for submodules and prove that solving the system of polynomial equations corresponding to the deducibility problem is equivalent to checking whether the polynomial h is a member of the saturation of some submodule M. The latter problem can be checked using Gröbner basis computations.

Fields and non-commutative rings

Another problem of interest is when we consider deducibility inside the field rather than the group. The deducibility problem can then be defined as follows: let Y be a set of names sampled in Z q , E the equational theory capturing field operations, f 1 , ...f k , h ∈ K[Y ] be a set of polynomials over the names, and Γ be a coherent set of axioms. The deducibility problem is then:

f 1 , ..., f k ⊢ E h
We emphasize that this problem is in fact not an instance of the problem for Diffie-Hellman exponentiation. In the previous problem, if we look at field elements, the adversary could compute any polynomial in K[X ] but he may now compute any polynomial in K[f 1 , ..., f k ], the subalgebra generated by the known polynomials.

Decidability is obtained thanks to [START_REF] Shannon | Using GröBner Bases to Determine Algebra Membership, Split Surjective Algebra Homomorphisms Determine Birational Equivalence[END_REF], where they solve the subalgebra membership problem using methods based on classical Gröbner basis. Proposition 4.2. Deducibility for fields is decidable.

If we wish to characterize the full adversary knowledge as done for Diffie-Hellman exponentiation using Gröbner basis, we would have to resort to so-called SAGBI [START_REF] Robbiano | Subalgebra bases[END_REF] (Subalgebra Analog to Gröbner Basis for Ideals) techniques, which form the counterpart of Gröbner basis computations. However, some finitely generated subalgebras are known to have infinite SAGBI bases [START_REF] Robbiano | Subalgebra bases[END_REF], thus it can only provide semi-decision for the membership problem.

For the case of non-commutative rings, we are not aware of any counterpart to [START_REF] Shannon | Using GröBner Bases to Determine Algebra Membership, Split Surjective Algebra Homomorphisms Determine Birational Equivalence[END_REF], we resort to the non-commutative SAGBI [START_REF] Nordbeck | Canonical Subalgebraic Bases in Non-commutative Polynomial Rings[END_REF] theory. Proposition 4.3. Deducibility for non-commutative rings is semidecidable.

It is an open problem whether one can give a decision procedure for non-commutative rings. We note that the problem of module membership over a non-commutative algebra is undecidable [START_REF] Mora | An introduction to commutative and noncommutative Gröbner bases[END_REF], as there is a reduction from the word problem over a finitely presented group. On the other hand, the problem is known to be decidable for some classes of subalgebras, notably in the the homogeneous case where all monomials are of the same degree.

Matrices

The case of matrices introduces a final difficulty: expressions may involve structural operations. To address the issue, we show that every deducibility problem in the theory of matrices is provably equivalent to a deducibility problem that does not involve structural operations, nor transposition-said otherwise, a deducibility problem in the theory of non-commutative rings. Proposition 4.4. Deducibility for matrices is semi-decidable.

The algorithm that supports the proof of semi-decidability for matrices operates in two steps:

(1) it reduces the deducibility problem for matrices to an equivalent deducibility problem for non-commutative rings; (2) it applies the semi-decision procedure for non-commutative rings.

The reduction to non-commutative rings is based on a generalization of the techniques introduced in [START_REF] Barthe | On the Equality of Probabilistic Terms[END_REF] for the theory of bitstringsnote that the techniques were used for a slightly different purpose, i.e. deciding equivalence between probabilistic expressions, rather than for proving deducibility constraints. The general idea for eliminating concatenation and splitting comes from two basic facts:

• M ⊢ M ∥ N ⇔ M ⊢ M ∧ M ⊢ N • M ∪ {M ∥ N } ⊢ T ⇔ M ∪ {M, N } ⊢ T
For transposition, we observe that it commutes with the other operations, so in a proof of deducibility, we can push the transposition applications to the leaves. Everything that can be deduced from a set of matrices M and the transpose operation can also be deduced if instead of the transpose operation we simply provide the transposition of the matrices in M.

IMPLEMENTATIONS AND CASE STUDIES

The implementation of our logic, called AutoLWE, is available at: https://github.com/autolwe/autolwe AutoLWE is implemented as a branch of AutoG&P and thus makes considerable use of its infrastructure.

Moreover, we have used AutoLWE to carry several case studies (see Figure 12): an Identity-Based Encryption scheme and an Hierarchical Identity-Based Encryption scheme by Agrawal, Boneh and Boyen [START_REF] Agrawal | Efficient Lattice (H)IBE in the Standard Model[END_REF], a Chosen-Ciphertext Encryption scheme from Micciancio and Peikert [START_REF] Micciancio | Trapdoors for Lattices: Simpler, Tighter, Faster, Smaller[END_REF], and an Inner Product Encryption scheme and proof from Agrawal, Freeman, and Vaikuntanathan [START_REF] Agrawal | Functional Encryption for Inner Product Predicates from Learning with Errors[END_REF]. These examples are treated in Sections 5.2, 5.4, 5.3 and 5.5 respectively.

Globally, our tool performs well, on the following accounts: formal proofs remains close to the pen and paper proofs; verification time is fast (less than 3 seconds), and in particular the complexity of the (semi-)decision procedures is not an issue; formalization time is moderate (requiring at most several hours of programmer effort per proof). One of the main hurdles is the Leftover Hash Lemma, which must be applied in varying levels of sophistication. The Leftover Hash Lemma (and more generally all oracle-relative assumptions) increase the difficulty of guessing (chained) applications of assumptions, and consequently limits automation. [START_REF] Agrawal | Functional Encryption for Inner Product Predicates from Learning with Errors[END_REF] AFV-IPE IND-wAH-CPA 106

Case study Proof

Figure 12: Overview of case studies. All proofs took less than three seconds to complete.

Implementation

Security games are written in a syntax closely resembling that shown in Figure 1. See Figure 5 for an example concrete proof in our system. Each line of the proof corresponds to a proof rule in our logic, as seen in Figure 8. All tactic applications are fully automated, except for the application of oracle-relative assumptions. The user must provide some hints to AutoLWE about how the security game needs to be factored in order to apply an oracle-relative assumption.

The system in [START_REF] Barthe | Automated Proofs of Pairing-Based Cryptography[END_REF] additionally supports a proof search tactic which automatically finds a series of tactics to apply to finish the goal; we do not have a version of that in our setting.

Oracle-relative

Assumptions. AutoG&P allows one to add user defined axioms, both to express decisional assertions (two distributions are computationally close) and computational assertions (a certain event has small chance of happening). In AutoG&P, these user-defined axioms are stated in terms of symbolic adversaries, which are related to the main security game by rules such as [Abstract] in Section 3.4. However, the symbolic adversaries present in axioms may not have oracles attached to them. While these restricted adversaries can be used to define the LWE assumption, they are not expressive enough to state the oracle-relative axioms we use throughout our proofs. In AutoLWE, we remove this restriction. An example axiom we now support which we did not before is that in Figure 11.

Recall that in order to apply a user defined axiom using [Abstract], we must factor the security game into one which is in terms of the axiom's game. This is done essentially by separating the security game into sections, where each section either reflects the setup code for the axiom, or an instantiation of one of the adversaries in the axiom. We still do this factoring in the case of oracle-relative axioms, but we must also factor oracles in the security game in terms of oracles in the axiom. Once this second step of factoring is done, oracles in the axiom can be compared syntactically to factored oracles in the security game.

5.1.2 Theory of Lists and Matrices. Note that in our case studies, we manipulate both matrices and lists of matrices (often simultaneously). Thus, both our normal form algorithm and our deducibility reduction from Section 4.3 must be lifted to apply to lists of matrices as well. This is what allows our system to reason about the more complicated HIBE scheme in a manner similar to the IBE scheme, which does not use lists.

In order to do this, we do not implement our main algorithms on expressions of matrices directly, but instead over a general signature of matrices, encoded as a certain type of an ML module. We then instantiate this signature both with matrices and lists of matrices. By doing so, we receive an implementation for our new algorithms which operate uniformly across these two types of expressions.

Deduction algorithms.

Many implementations of Gröbner basis computations can be found online, but all of them are only usable for polynomial ideals. In order to handle module and noncommutative subalgebra, we thus implemented generic versions of the Buchberger algorithm for K[X ]-module and the SAGBI algorithm and plugged them into AutoLWE. The algorithms performed well: we could prove all the LWE examples, and the pairing-based examples very quickly, using the SAGBI methods. The efficiency of the computations contrasts with the complexity of the algorithms, which is high because the saturation squares up the number of inputs terms and the Gröbner Basis can be at worst a double exponential. However, we are dealing with relatively small instances of our problem that are extracted from concrete primitives.

Identity-Based Encryption

Mathematical background. Let Λ be a discrete subset of Z m . For any vector c ∈ R m , and any positive parameter σ ∈ R, let ρ σ,c (x ) = exp(-π ||x -c || 2 /σ 2 ) be the Gaussian function on R m with center c and parameter σ . Next, we let ρ σ,c (Λ) = x ∈Λ ρ σ,c (x ) be the discrete integral of ρ σ,x over Λ, and let χ Λ,σ,c (y) := (Λ) . Let S m denote the set of vectors in R m whose length is 1. The norm of a matrix R ∈ R m×m is defined to be sup x ∈S m ||Rx ||. We say a square matrix is full rank if all rows and columns are linearly independent.

ρ σ ,c (y ) ρ σ ,c
Identity-based encryption is a generalization of public key encryption. In IBE, the secret key and ciphertext are associated with different identity strings, and decryption succeeds if and only if the two identity strings are equivalent. The security model, IND-sID-CPA, requires adversary to declare challenge identity upfront before seeing the public parameters, and allows adversary to ask for secret key for any identity except for the challenge identity, and CPA security holds for ciphertext associated with the challenge identity.

The IBE scheme our system supports is constructed by Agrawal et al. [START_REF] Agrawal | Efficient Lattice (H)IBE in the Standard Model[END_REF]. The scheme operates as follows:

• Matrix A is generated by algorithm TrapGen, which outputs a random A ∈ Z n×m q and a small norm matrix T ∈ Z m×m q such that A • T A = 0. Matrices A 1 , B are sampled randomly from Z n×m q , and u is sampled randomly from Z n q . Set pp = (A, A 1 , B, u) and msk = T A .

• To encrypt a message µ ∈ {0, 1} with identity id ∈ Z n q , one generates a uniform s ∈ Z n q , error vector e 0 ← χ m and error integer e 1 ← χ from discrete Gaussian, a random R ∈ {0, 1} m×m , and computes ciphertext ct = s T [A||A 1 + M (id)B||u] + (e T ||e T R||e ′ ) + (0||0||⌈q/2⌉µ).

• The secret key for identity id ∈ Z n q is generated by procedure r ← SampleLeft(A, A 1 + M (id)B, T A , u), where we have r is statistically close to χ 2m , and [A||A 1 + M (id)B] r = u. The idea of the proof is first to rewrite A 1 as AR -M (id * )B, where id * is the adversary's committed identity. If we do so, we then obtain that the challenge ciphertext is of the form

s T [A||AR||u] + (e T ||e T R||e ′ ) + (0||0||⌈q/2⌉µ)
where A comes from TrapGen. We then apply a computational lemma about SampleLeft, in order to rewrite the KeyGen oracle to be in terms of another probabilistic algorithm, SampleRight. This is a statement about equivalence of distributions from which the adversary may sample, so must be handled using an oracle-relative assumption. This is done as described in Section 3.6.3. The computational lemma states that, for appropriately sampled matrices,

SampleLeft(A, AR + B,T A , u) ≈ SampleRight(A, B, R,T B , u),
where A is sampled from TrapGen in the first and uniform in the second, and B is sampled uniformly in the first and from TrapGen in the second. By applying this transformation to our KeyGen oracle, we transform our matrix A from one sampled from TrapGen to uniform. Now that A is uniform, we finish the proof by noticing that our challenge ciphertext is equal to b||bR||b + ⌈q/2⌉µ, where (b, b) forms an LWE distribution of dimension n × m + 1. Thus we may randomize b to uniform, and apply the rnd tactic to erase µ from the ciphertext.

The main point of interest in this proof is the initial rewrite A 1 → AR -M (id * )B. Given that A 1 is uniform, we may first apply optimistic sampling to rewrite A 1 to A 2 -M (id * )B, where A 2 is uniformly sampled. Thus, we now only need to perform the rewrite A 2 → AR. This rewrite is not at all trivial, because A at this point in the proof comes from TrapGen. However, as noted in Section 3.6.2, it is sound to apply the LHL in this case, because TrapGen generates matrices which are close to uniform in distribution. Thus, we can use the LHL as encoded in Figure 10.

CCA1-PKE

The CCA1-PKE scheme we study is proposed by Micciancio and Peikert [START_REF] Micciancio | Trapdoors for Lattices: Simpler, Tighter, Faster, Smaller[END_REF]. In comparison with the CPA-PKE scheme [START_REF] Gentry | Trapdoors for hard lattices and new cryptographic constructions[END_REF] described in Section 2, the security model of CCA1-PKE is stronger: the adversary can query a decryption oracle for any ciphertext he desires before receiving the challenge ciphertext. The scheme operates as follows:

• Matrix A ∈ Z n×m q is sampled randomly and R ← {-1, 1} m×m . Set pk = (A, AR) and sk = R.

• Let M : Z n q → Z n×m q be an embedding from Z n q to matrices, such that for distinct u and v, M (u) -M (v) is full rank. To encrypt a message µ ∈ {0, 1}, one generates a uniform s ∈ Z n q , a uniform u ∈ Z n q , a uniform matrix R ′ ∈ {-1, 1} m×m and an error vector e ∈ Z m q sampled from a discrete Gaussian, and computes the ciphertext

c 0 = u, c 1 = s T A u + (e T ||e T * R ′ ) + (0||Encode(µ)), where A u := [A|| -AR + M (u)G],
G is a publicly known gadget matrix, and Encode : {0, 1} → Z m q sends µ to µ ⌈q/2⌉ (1, . . . , 1). • To decrypt a ciphertext (u := c 0 , c 1 ) with sk = R and u 0, one computes A u and calls a procedure Invert(A u , R, c 1 ), which will output s and e such that c 1 = s T A u + e, where e has small norm. By doing a particular rounding procedure using c 1 , s, e, and R, the message bit µ can be derived.

The main subtlety of the proof is that the secret key R is used in the decryption oracle. Because of this, we must apply the Leftover Hash Lemma relative to this oracle, by using oracle-relative axioms. As we will see, not all uses of the LHL are valid in this new setting; care must be taken to ensure that the axioms derived from the LHL are still cryptographically sound.

The high-level outline of the proof is as follows: first, we note that instead of using a fresh R ′ to encrypt, we can actually use the secret key R. This is justified by the following corollary of the Leftover Hash Lemma: the distribution (A, AR, e, eR ′ ) is statistically close to the distribution (A, AR, e, eR) where A, R, R ′ , and e are sampled as in the scheme. This corollary additionally holds true relative to the decryption oracle, which makes use of R.

Once we use R to encrypt instead of R ′ , we again use the Leftover Hash Lemma to transform AR into -AR + M (u)G, where u is generated from the challenge encryption. Again, this invocation of the Leftover Hash Lemma is stated relative to the decryption oracle. Crucially, note here that we do not transform AR directly into uniform, as we did before: the reason being is that this transformation would actually be unsound, because it would decouple the public key from R as it appears in the decryption oracle. Thus, we must do the transformation AR → -AR + M (u)G in one step, which is cryptographically sound relative to the decryption oracle. (Currently, we must write this specialized transformation as a unique variant of the Leftover Hash Lemma, as discussed in Section 3.6.2; future work will involve unifying these separate variants.)

At this point, we may apply the LWE assumption along with a more routine invocation of the LHL in order to erase the message content from the challenge ciphertext, which finishes the proof.

Hierarchical Identity-Based Encryption

Hierarchical IBE is an extension of IBE. In HIBE, the secret key for ID string id can delegate secret keys for ID strings id ′ , where id is a prefix for id. Moreover, decryption succeeds if the ID string for the secret key is a prefix of (or equal to) the ID string for the ciphertext. The security model can be adapted according to the delegation functionality.

The HIBE construction our system supports is described in [START_REF] Agrawal | Efficient Lattice (H)IBE in the Standard Model[END_REF]. The ID space for HIBE is id i ∈ (Z n q ) d . The secret key for ID string id = (id 1 , . . . , id ℓ ), where id i ∈ Z n q , is a small-norm matrix T, such that F id T = 0, and

F id = [A 0 ||A 1 + M (id 1 )B|| • • • ||A ℓ + M (id ℓ )B].
We note that T can be computed as long as we know the secret key for id ′ , where id ′ is a prefix of id. Ciphertext for ID string id can be generated similarly with respect to matrix F id .

The security proof of HIBE is similar to the counterpart of IBE. The challenge ID string id

* = (id * 1 , . . . , id * ℓ ) is embedded in pp as ∀i ∈ [ℓ], A i = AR i -M (id * i )B, ∀ℓ < j ≤ d, A j = AR j
For admissible query id = (id 1 , . . . , id k ), where id is not a prefix of id * , we have

B k = (M (id 1 ) -M (id * 1 ))B|| • • • ||(M (id k ) -M (id * k )
)B 0 Then we can generate secret key for id using information B k and

R k = (R 1 || • • • ||R k ).
In previous cases, we manipulate and apply rewriting rules to matrices. However, in order to reason about the security in a similar manner to pen-and-paper proof, we introduce the list notation, and adapt our implementation to operate uniformly across these two types of expressions.

Inner Product Encryption

The IPE scheme our scheme supports is described in [START_REF] Agrawal | Functional Encryption for Inner Product Predicates from Learning with Errors[END_REF]. We briefly recall their construction as

• Matrix A is generated by algorithm TrapGen. Matrices {matB i } i ∈[d ]
are sampled randomly from Z n×m q , and random vector u is from Z n q . The public parameters pp = (A, {B i } i ∈[d ] , u), and msk = T A .

• Secret key sk v = r for vector v ∈ Z d q is computed by algorithm r ← SampleLeft(A, i ∈[d ] B i G -1 (v i G), T A , u), where for oper- ation G -1 (•) : Z n×m q → Z m×m q , for any A ∈ Z n×m q , it holds that G • G -1 (A) = A and G -1 (A) has small norm.
• To encrypt a message µ ∈ {0, 1} for attribute w, one generates a uniform s ∈ Z n q , error vector e 0 ← χ m and error integer e 1 ← χ from discrete Gaussian, random matrices

{R i } i ∈[d ] ∈ {0, 1} m×m , and computes ciphertext (c 0 , {c i } i ∈[d ] , c) as c 0 = s T A + e T 0 , c i = s T (B i + w i G) + e T 0 R, c = s T u + e + ⌈q/

2⌉µ

The main challenge in the proof is to answer secret key queries for any vector v as long as ⟨v, w 0 ⟩, ⟨v, w 1 ⟩ are both not 0, where (w 0 , w 1 ) is declared by adversary upfront. The attribute w b (b is a random bit) is first embedded in pp, i.e.

B i = AR i -w bi G, ∀i ∈ [d],
where R i is a small matrix. By unfolding the matrix for query v, we have

       A|| i ∈[d ] B i G -1 (v i G)        =        A||A i ∈[d ] R i G -1 (v i G) + ⟨w b , v⟩G       
If ⟨w b , v⟩ 0, the algorithm SampleRight can be used to generate secret key for v.

The sequence of hybrids generated in symbolic proof is a bit different from the pen-and-paper proof. In particular, instead of transforming from embedding of challenge attribute w 0 directly to embedding of w 1 , we use the original scheme as a middle game, i.e. from embedding of w 0 to original scheme, then to embedding of w 1 . The reason for using the original scheme again in the proof is that when using LHL to argue the indistinguishability between (A, {B i = AR i -w 0i G} i ) and (A, {B i = AR i -w 1i G} i ), the real public parameters (A, {B i } i ) actually serves as a middleman. Therefore, to ensure the consistency with respect to public parameters and secret key queries, the real scheme is used to make the transformation valid.

RELATED WORK

For space reasons, we primarily focus on related works whose main purpose is to automate security proofs in the computational model.

Corin and den Hartog [START_REF] Corin | A Probabilistic Hoare-style Logic for Game-Based Cryptographic Proofs[END_REF] show chosen plaintext security of ElGamal using a variant of a general purpose probabilistic Hoare logic. In a related spirit, Courant, Daubignard, Ene, Lafourcade and Lakhnech [START_REF] Courant | Towards automated proofs for asymmetric encryption schemes in the random oracle model[END_REF] propose a variant of Hoare logic that is specialized for proving chosen plaintext security of padding-based encryption, i.e. public-key encryption schemes based on one-way trapdoor permutations (such as RSA) and random oracles. Later, Gagné, Lafourcade, Lakhnech and Safavi-Naini [START_REF] Gagné | Automated Security Proofs for Almost-Universal Hash for MAC Verification[END_REF][START_REF] Gagné | Automated Security Proof for Symmetric Encryption Modes[END_REF] adapt these methods to symmetric encryption modes and message authentication codes.

Malozemoff, Katz and Green [START_REF] Malozemoff | Automated Analysis and Synthesis of Block-Cipher Modes of Operation[END_REF] and Hoang, Katz and Malozemoff [START_REF] Viet | Automated Analysis and Synthesis of Authenticated Encryption Schemes[END_REF] pursue an alternative approach for proving security of modes of operations and authenticated encryption schemes. Their approach relies on a simple but effective type system that tracks whether values are uniform and fresh, or adversarially controlled. By harnessing their type system into a synthesis framework, they are able to generate thousands of constructions with their security proofs, including constructions whose efficiency compete with state-of-the-art algorithms that were discovered using conventional methods. Using SMT-based methods, Tiwari, Gascón and Dutertre [START_REF] Tiwari | Program Synthesis Using Dual Interpretation[END_REF] introduce an alternative approach to synthesize bitvector programs, padding-based encryption schemes and modes of operation.

Our work is most closely related to CIL [START_REF] Barthe | Computational indistinguishability logic[END_REF], ZooCrypt [START_REF] Barthe | Fully automated analysis of padding-based encryption in the computational model[END_REF] and AutoG&P [START_REF] Barthe | Automated Proofs of Pairing-Based Cryptography[END_REF]. Computational Indistinguishability Logic (CIL) [START_REF] Barthe | Computational indistinguishability logic[END_REF] is a formal logic for reasoning about security experiments with oracle and adversary calls. CIL is general, in that it does not prescribe a syntax for games, and side-conditions are mathematical statements. CIL does not make any provision for mechanization, although, as any mathematical development, CIL can be formalized in a proof assistant, see [START_REF] Corbineau | Certified Security Proofs of Cryptographic Protocols in the Computational Model: An Application to Intrusion Resilience[END_REF]. ZooCrypt [START_REF] Barthe | Fully automated analysis of padding-based encryption in the computational model[END_REF] is a platform for synthesizing padding-based encryption schemes; it has been used successfully to analyze more than a million schemes, leading to the discovery of new and interesting schemes. ZooCrypt harnesses two specialized computational logics for proving chosen-plaintext and chosen-ciphertext security, and effective procedures for finding attacks. The computational logics use deducibility to trigger proof steps that apply reduction to one-wayness assumptions, and to compute the probability of bad events using a notion of symbolic entropy. However, ZooCrypt is highly specialized.

AutoG&P [START_REF] Barthe | Automated Proofs of Pairing-Based Cryptography[END_REF] introduce a computational logic and provide an implementation of their logic, called AutoG&P, for proving security of pairing-based cryptographic constructions. Their logic uses deducibility for ensuring that proof rules are correctly enforced. Their implementation achieves a high level of automation, thanks to a heuristics for checking deducibility, and a proof search procedure, which decides which proof rule to apply and automatically selects applications of computational assumptions. We build heavily on this work; in particular, AutoLWE is implemented as an independent branch of AutoG&P. The main differences are:

• AutoLWE supports oracle-relative assumptions and general forms of the Leftover Hash Lemma, and (semi-)decision procedures for deducibility problems, for the theories of Diffie-Hellman exponentiation, fields, non-commutative rings and matrices. In contrast, AutoG&P only support more limited assumptions and implements heuristics for the theory of Diffie-Hellman exponentiation; • AutoG&P supports automated generation of EasyCrypt proofs, which is not supported by AutoLWE. Rather than supporting generation of proofs a posteriori, a more flexible alternative would be to integrate the features of AutoG&P and AutoLWE in Easy-Crypt.

Theodorakis and Mitchell [START_REF] Theodorakis | Semantic Security Invariance under Variant Computational Assumptions[END_REF] develop a category-theoretical framework for game-based security proofs, and leverage their framework for transferring such proofs from the group-based or pairingbased to the lattice-based setting. Their results give an elegant prooftheoretical perspective on the relationship between cryptographic proofs. However, they are not supported by an implementation. In contrast, we implement our computational logic. Furthermore, proofs in AutoLWE have a first-class status, in the form of proof scripts. An interesting direction for future work is to implement automated compilers that transform proofs from the group-and pairing-based settings to the lattice-based settings. Such proof compilers would offer a practical realization of [START_REF] Theodorakis | Semantic Security Invariance under Variant Computational Assumptions[END_REF] and could also implement patches when they fail on a specific step.

CONCLUSION

We have introduced a symbolic framework for proving the security of cryptographic constructions based on the (decisional) Learning with Errors assumption. A natural step for future work is to broaden the scope of our methods to deal with other hardness assumptions used in lattice-based cryptography, including the Ring Learning with Errors assumption, the Short Integer Solution assumption. A further natural step would then be to analyze lattice-based key exchange protocols [START_REF] Bos | Frodo: Take off the Ring! Practical, Quantum-Secure Key Exchange from LWE[END_REF][START_REF] Peikert | Lattice Cryptography for the Internet[END_REF]. To this end, it would be interesting to embed the techniques developed in this paper (and in [START_REF] Barthe | Automated Proofs of Pairing-Based Cryptography[END_REF]) into the EasyCrypt proof assistant [START_REF] Barthe | EasyCrypt: A Tutorial[END_REF][START_REF] Barthe | Computer-Aided Security Proofs for the Working Cryptographer[END_REF], and to further improve automation of EasyCrypt for typical transformations used for proving security of protocols.

A PROOFS OF SECTION 4.1

In group theory, a multilinear map is a function which goes from a set of groups into a target group, and is linear with respect to all its arguments. They have been used in the past years to develop new schemes, such as Boneh-Boyen Identity Based Encryption [START_REF] Boneh | Efficient Selective-ID Secure Identity-Based Encryption Without Random Oracles[END_REF] or Waters' Dual System Encryption [START_REF] Waters | Dual System Encryption: Realizing Fully Secure IBE and HIBE under Simple Assumptions[END_REF].

Given a multilinear map ê, д 1 , .., д n , д t a set of groups generators, let X be a set of public names sampled in Z q , Y be a set of private names sampled in Z q , f 1 , ...f k , h ∈ K[X , Y ] be a set of polynomials over both public and secret names and Γ be a coherent set of axioms.

Our deducibility problem is to decide if Γ |= X , д

f 1 i 1 , ..., д f k i k ⊢ E д h t
Without loss of generality, we consider here the case of a bilinear map, to simplify the writing, but the proofs scale up to multilinear maps.

A.1 Saturation into the target group

First, we reduce our problem to the case of a single group. This result comes from the Proposition 1 of [START_REF] Kremer | Reducing Equational Theories for the Decision of Static Equivalence[END_REF]. Their constructive proof can trivially be used to obtain the following proposition:

Proposition A.1. For any sets X and Y , polynomials f 1 , ...f n , h ∈ K[X , Y ] and groups elements д

f 1 i 1 , ..., д f n i n , we denote (д e i t ) = { ê (д i j , д i k )|1 ≤ j ≤ k ≤ n, д i j ∈ G 1 , д i k ∈ G 2 } ∪{ ê (д i j , 1)|1 ≤ j ≤ n, д i j ∈ G 1 , } ∪{ ê (1, д i j )|1 ≤ j ≤ n, д i j ∈ G 2 , } Then Γ |= X , д f 1 i 1 , ..., д f n i n ⊢ E д h t ⇔ Γ |= X , д e 1 t , ..., д e N t ⊢ E-ê д h t .
We obtain a problem where we only have elements in the target group, we can therefore reduce the general problem to the single group case. ∃(e i , д i ) ∈ K[X ], (∀i, Γ |= д i 0)

A.2 Reduction to polynomials

∧ i e i × f i д i = h
Proof. If Γ = ∅, the adversary can construct elements of the form (д w i t ) e i , where e i ∈ K[X ], i.e e i is a polynomial constructed over variables fully known by the adversary, and then multiply this kind of term, yielding a sum in the exponent. If Γ ∅, he may also divide by some д д i t , with д i ∈ K[X ]. We capture here the three capabilities of the adversary, which when looking in the exponent immediately translate into the formula on the right side. □

To handle this new problem, we notice that we can actually compute the set {д|Γ |= д 0}. Indeed, for each axiom f 0, we can extract a finite set of non zero irreducible polynomials by factorizing them (for example using Lenstra algorithm [START_REF] Lenstra | Factoring multivariate polynomials over finite fields[END_REF]). Any non annulling polynomial will be a product of all these irreducible polynomials. We can then obtain a finite set Gs = (д i ) such that G = {д|Γ |= д 0} = { д ∈Gs д k д |∀д, k д ∈ N}. With these notations, we can simplify proposition 1, because we know the form of the д i . Moreover, as we do not want to deal with fractions, we multiply by the common denominator of all the w i д i .

Lemma A. We do not prove this lemma, we will rather reformulate it using more refined mathematical structures and then prove it. Let us call M = { i e i × w i |e i ∈ K[X ]} the free K[X ]-module generated by the (w i ). We recall that a S-module is a set stable by multiplication by S and addition, and that ⟨(w i )⟩ S is the S-module generated by (w i ). We also recall the definition of the saturation : Definition A.4. Given a S-module T, f ∈ S and S ⊂ S ′ , the saturation of T by f in S' is T : S ′ ( f ) ∞ = {д ∈ S ′ |∃n ∈ N, f n д ∈ T }.

The previous lemma can be reformulated using saturation; if M is the module generated by w 1 , ..., w N : Lemma A.5. Γ |= X , д w 1 t , ...,

д w N t ⊢ E д h t ⇔ h ∈ M : K[X,Y ] (д 1 ...д n ) ∞
Proof. We recall that:

M : K[X,Y ] (д 1 ...д n ) ∞ = {x ∈ K[X , Y ]|∃k ∈ N, (д 1 ...д n ) k × x ∈ M } ⇒
We have i e i ×w i = h д ∈Gs д k д . With K = max (k д ), we multiply both sides by д д K -k д to get h д ∈Gs д K = i д д K -k д e i × w i ∈ M. Which proves that h ∈ M : K[X,Y ] (д 1 ...д n ) ∞ . ⇐ If h ∈ M : K[X,Y ] (д 1 ...д n ) ∞ , we instantly have (e i ) ∈ K[X ], k ∈ N such that h д ∈Gs д k д = i e i f i . □

We then simplify the saturation, by transforming it into the membership of the intersection of modules. Lemma A.6. For any sets X and Y , f 1 , ...

f n , h ∈ K[X , Y ], д ∈ K[X ],let M = { i e i × f i |e i ∈ K[X ]} . Then, with t a fresh variable M : K[X,Y ] д ∞ = ⟨( f i ) ∪ ((дt -1)Y j ) j ∈ {deд Y (f i ) } ⟩ K[X,t ] ∩ K[X , Y ].
Proof. ⊂. Let there be v ∈ M : K[X,Y ] д ∞ . Then, we have k such that д k × v ∈ M. The following equalities shows that v is in the right side set v = д k t k v -(1 + дt + ... + д k-1 t k -1 )(дt -1)v. Indeed, д k t k v ∈ MK[X , t], so we have (e i ) ∈ K[X , t] such that д k t k v = i e i f i . Moreover, д k × ∈ M and д ∈ K[X ] implies that deд Y (v) ⊂ {deд Y ( f i )}. So we do have (e ′ i ) ∈ K[X , t] and (j i ) ⊂ {deд Y ( f i )} such that

(1 + дt + ... + д k -1 t k-1 )(дt -1)v = e ′ i (дt -1)Y j i Finally, v ∈ ⟨( f i ) ∪ ((дt -1)Y j ) j ∈ {deд Y (f i ) } ⟩ K[X,t ] ∩ K[X , Y ]. ⊃. Let there be v ∈ ⟨( f i ) ∪ ((дt -1)Y j ) j ∈ {deд Y (f i ) } ⟩ K[X,t ] ∩ K[X , Y
]. Then we have (e i ), (e ′ i ) ∈ K[X , t] and

(j i ) ⊂ {deд Y ( f i )} such that : v = i e i f i + i e ′ i (дt -1)Y j i
We have that v ∈ K[X , Y ], so v is invariant by t. So, if we subsitute t with 1 д , we have that v = i e i (X , 1 д ) f i . Let us consider д k the common denominator of all those fractions and call e ′′ i = д k e i ∈ K[X ]. We finally have

д k × v = i e ′′ i f i ∈ M, which means that v ∈ M : K[X,Y ] д ∞ . □
The Buchberger algorithm allows us to compute a Gröbner basis of any free K[X ]-module [START_REF] Eisenbud | Commutative Algebra: with a view toward algebraic geometry[END_REF] and then decide the membership problem for a module. We thus solve our membership problem using this method. Theorem A.7. For any sets X and Y , polynomials f 1 , ...f n , h ∈ K[X , Y ], group elements д i 1 , ..., д i n and a set of axioms Γ we can decide if Γ |= X , д

f 1 i 1 , ..., д f n i n ⊢ E д h t Proof.
To decide if h is deducible, we first reduce to a membership problem with lemma A.5 that can be solved using lemma A.6 by computing the Gröbner basis of ⟨( f i )∪((дt-1)Y j ) j ∈ {deд Y (f i ) } ⟩ K[X,t ] , keeping only the elements of the base that are independent of t and then checking if the reduced form of h is 0. □ As a side note, being able to decide the deducibility in this setting allows us to decide another classical formal method problem, the static equivalence. Indeed the computation of the Gröbner basis allows us to find generators of the corresponding syzygies (Theorem 15.10 of [START_REF] Eisenbud | Commutative Algebra: with a view toward algebraic geometry[END_REF]), which actually captures all the possible distinguishers of a frame.

B PROOFS FOR SECTION 4.3

We provide a more detailed proof of Proposition 4.4. To reason about matrices deducibility, written M ⊢ M for a set of matrices M and a matrix M, we use the natural formal proof system K which matches the operations on expressions (see Figure 13), that we extend with the equality rule

[Eq] M ⊢ M 1 M ⊢ M 1 = M 2 M ⊢ M 2
. For ease of writing, we denote B ⊤ ). Given a set of matrices M, we rewrite the matrices so that the concatenations operators are at the top. We can see the matrices as block matrices with submatrices without any concat, and then, we can create a set S(M) containing all the submatrices. This preserves deducibility thanks to the Eq rule for the rewriting, and to the split rules for the submatrices. □ Definition B.2. We call N the proof system based on K without splits, and write the deducibility with M ⊢ N M. Proof. We prove it by induction on the size of the proof, and by disjunction on the last rule applied.

Base case: |π | = 2, then the proof is a concat on axioms and we can then obtain the sub matrix directly, with a proof of size one.

Induction case:

• The last rule is Then, we directly obtain by induction on ( R S ) smaller proofs for R and S.

Figure 1 :

 1 Figure 1: IND-CPA security of dual-Regev PKE.

Figure 2 :

 2 Figure 2: Dual-Regev PKE: Game 2

Figure 3 :

 3 Figure 3: Dual-Regev PKE: Game 3

Figure 4 :

 4 Figure 4: Dual-Regev PKE: Game 4

Figure 5 :

 5 Figure 5: AutoLWE proof for Dual Regev Encryption.

Figure 8 :

 8 Figure 8: Selected proof rules

Figure 9 :

 9 Figure 9: The LWE assumption, encoded in AutoLWE.

Figure 10 :

 10 Figure 10: The LHL assumption combined with TrapGen, encoded in AutoLWE.

Figure 11 :

 11 Figure 11: Example axiom capturing computational closeness of distributions.

Proposition 4 . 1 .

 41 Deducibility for Diffie-Hellman exponentiation is decidable.

Lemma A. 2 .

 2 For any sets X and Y , polynomials w 1 , ...w N , h ∈ K[X , Y ] we have Γ |= X , д w 1 t , ..., д w N t ⊢ E д h t if and only if:

  ( A B ) := (A ⊤ ||B ⊤ ) ⊤ . Splits elimination. Proposition B.1. Given a set of matrices M and a matrix M, we can obtain S(M) a set of matrices without any concats, such that M ⊢ M ⇔ S(M) ⊢ H . Proof. We notice that the concat operations commute with all the other operators: (A||B) + (C ||D) = (A + C ||B + D), (A||B) -(C ||D) = (A -C ||B -D), A × (B||C) = (AB||AC) , (A||B) × C D = AC + BD, (A||B) ⊤ = ( A ⊤

Lemma B. 3 .

 3 If M ⊢ (R||S ) with a proof π (resp. M ⊢ ( R S ) ) then M ⊢ R and M ⊢ S with smaller proofs (resp. M ⊢ R, M ⊢ S ) .

  e ′ if there exists a context C such that Γ |= e ⊢ E e ′ . More generally, a (general) context C is an expression that only contains distinguished variables • 1 , . . . , • n . We write e 1 , . . . , e n ⊢ C E e ′ , where e 1 , . . . , e n , e ′ are expressions and C is a context, if ⊢ E C[e 1 , . . . , e n ] = e ′ . We write e 1 , . . . , e n ⊢ E e ′ if there exists a context C such that e 1 , . . . , e n ⊢ C E e ′ and Γ |= e 1 , . . . , e n ⊢ E e ′ if there exists a context C such that Γ |= e 1 , . . . , e n ⊢ E e ′ . Intuitively, a context is a recipe that shows how some expression may be computed given other expressions. If we consider matrices, we may have

•. We write e ⊢ C E e ′ , where e, e ′ are expressions and C is a context, if ⊢ E C[e] = e ′ . We write e ⊢ E e ′ if there exists a context C such that e ⊢ C E e ′ . Similarly, we write Γ |= e ⊢ C E e ′ if Γ ⊢ E C[e] = e ′ and Γ |= e ⊢ E E e ′ . Similarly, we write Γ |= e 1 , . . . , e n ⊢ C E e ′ if Γ |= C[e 1 , . . . , e n ] =

  3. For any sets X and Y , polynomials w 1 , ...w N , h ∈ K[X , Y ] we have Γ |= X , д w 1 t , ..., д w N

	д k д
	д ∈Gs

t ⊢ E д h t if and only if:

∃(e i ) ∈ K[X ], (k д ) ∈ N, i e i × w i = h

Acknowledgements. This work is partially supported by ONR Grant N000141512750 (Barthe), by IBM under Agreement 4915013672 (Fan), and by NSF Grant 1704788 (Gancher).

• The last rule is

Proof. We prove it by induction on the size of the proof, and by disjunction on the last rule applied.

Base case: |π | = 1, then the only problem might be if the rule used was a split, but as we have matrices without concatenations, this is not possible.

Induction case:

we conclude by applying the induction hypothesis to the premise of the rule.

• The last rule is

M . Then, we have a proof of (M |N ) of size π -1, and with lemma B.3 we have a smaller proof of M, on which we can then apply our induction hypothesis to obtain a proof of M without split.

• splitR is similar.

Proof. The left implication is trivial. For the right one, we once more do a proof by induction on the size of the proof.

Base case: |π | = 1, the last rule is a [||], and we do have a proof of M and N .

Induction case:

• The last rule is

Then, by induction on the proof of N, we obtain proofs of size smaller than |π | -1 of N l and N r without concats, and we just have to add a [×] to those proofs, yielding proofs of MN l and MN r without concats.

• If the last rule is [Tr], [+], [-], [sL],

[sR], we proceed as in the previous case • The last rule is [||]. Then the induction rule instantly yields the expected proofs. Then, we have a proof of (M |N ) of size π -1, and with lemma B.3 we have a smaller proof of M, on which we can then apply our induction hypothesis to obtain a proof of M without split.

Proof. The left implication is trivial, we prove the right one. As was done in Lemma B.1, we can see M has a bloc matrix, i.e with all the concat at the top.

We are given a proof of M ⊢ N M, which must contain all its concatenations at the bottom of the proof tree. If we look at all the highest concat rule in the proof such that no concat is made before, we have some proof of M ⊢ N (M i |M j ), and thanks to lemma B.6, we have M ⊢ T M i ∧ (A i ) ⊢ T M j . Applying this to all the highest concat rules in the proof yields the result. □

Removal of the transposition.

Definition B.8. We call V the proof system based on N without concat, and write the deducibility M ⊢ V M.

The transposition commutes with the other operations, given a matrix M we define the normal form N (M ) where the transposition is pushed to the variables. We extend the notation for normal form to sets of matrices.

Proof. ⇐ This is trivial, as the normal form can be deduced using the rule [Eq]. ⇒ Given the proof of M, we can commute the trans rule with all the others, and obtain a proof tree where all the transposition are just after a [∈] rule. Then, any [∈] followed by [trans] can be replaced by a [∈] and a [eq] when given the input M ∪ (N (M t ))) instead of M. We can thus construct a valid proof of M ∪ (N (M