Symbolic methods have been used extensively for proving security of cryptographic protocols in the DolevYao model, and more recently for proving security of cryptographic primitives and constructions in the computational model. However, existing methods for proving security of cryptographic constructions in the computational model often require significant expertise and interaction, or are fairly limited in scope and expressivity.
This paper introduces a symbolic approach for proving security of cryptographic constructions based on the Learning With Errors assumption (Regev, STOC 2005). Such constructions are instances of latticebased cryptography and are extremely important due to their potential role in postquantum cryptography. Following (Barthe, Gre ́goire and Schmidt, CCS 2015), our approach combines a computational logic and deducibility problems—a standard tool for representing the adversary’s knowledge, the DolevYao model. The computational logic is used to capture (indistinguishabilitybased) security notions and drive the security proofs whereas deducibility problems are used as sideconditions to control that rules of the logic are applied correctly. We then use AutoLWE, an implementation of the logic, to deliver very short or even automatic proofs of several emblematic constructions, including CPA PKE (Gentry et al., STOC 2008), (Hierarchical) IdentityBased Encryption (Agrawal et al. Eurocrypt 2010), Inner Product Encryption (Agrawal et al. Asiacrypt 2011), CCAPKE (Micciancio et al., Eurocrypt 2012). The main technical novelty beyond AutoLWE is a set of (semi)decision procedures for deducibility problems, using extensions of Grobner basis computations for subalgebras in the (non)commutative setting (instead of ideals in the commutative setting). Our procedures cover the theory of matrices, which is required for latticebased assumption, as well as the theory of noncommutative rings, fields, and DiffieHellman exponentiation, in its standard, bilinear and multilinear forms. Additionally, AutoLWE supports oraclerelative assumptions, which are used specifically to apply (advanced forms of) the Leftover Hash Lemma, an informationtheoretical tool widely used in latticebased proofs.
more »
« less
NonUniform Bounds in the RandomPermutation, IdealCipher, and GenericGroup Models
The randompermutation model (RPM) and the idealcipher model (ICM) are idealized models that offer a simple and intuitive way to assess the conjectured standardmodel security of many important symmetrickey and hashfunction constructions. Similarly, the genericgroup model (GGM) captures generic algorithms against assumptions in cyclic groups by modeling encodings of group elements as random injections and allows to derive simple bounds on the advantage of such algorithms.
Unfortunately, both wellknown attacks, e.g., based on rainbow tables (Hellman, IEEE Transactions on Information Theory ’80), and more recent ones, e.g., against the discretelogarithm problem (CorriganGibbs and Kogan, EUROCRYPT ’18), suggest that the concrete security bounds one obtains from such idealized proofs are often completely inaccurate if one considers nonuniform or preprocessing attacks in the standard model. To remedy this situation, this work
defines the auxiliaryinput (AI) RPM/ICM/GGM, which capture both nonuniform and preprocessing attacks by allowing an attacker to leak an arbitrary (boundedoutput) function of the oracle’s function table;
derives the first nonuniform bounds for a number of important practical applications in the AIRPM/ICM, including constructions based on the MerkleDamgård and sponge paradigms, which underly the SHA hashing standards, and for AIRPM/ICM applications with computational security; and
using simpler proofs, recovers the AIGGM security bounds obtained by CorriganGibbs and Kogan against preprocessing attackers, for a number of assumptions related to cyclic groups, such as discrete logarithms and DiffieHellman problems, and provides new bounds for two assumptions.
An important step in obtaining these results is to port the tools used in recent work by Coretti et al. (EUROCRYPT ’18) from the ROM to the RPM/ICM/GGM, resulting in very powerful and easytouse tools for proving security bounds against nonuniform and preprocessing attacks.
more »
« less
 Award ID(s):
 1815546
 NSFPAR ID:
 10208485
 Date Published:
 Journal Name:
 Lecture notes in computer science
 Volume:
 10991
 ISSN:
 03029743
 Page Range / eLocation ID:
 693721
 Format(s):
 Medium: X
 Sponsoring Org:
 National Science Foundation
More Like this


Symbolic methods have been used extensively for proving security of cryptographic protocols in the DolevYao model, and more recently for proving security of cryptographic primitives and constructions in the computational model. However, existing methods for proving security of cryptographic constructions in the computational model often require significant expertise and interaction, or are fairly limitedin scope and expressivity. This paper introduces a symbolic approach for proving security of cryptographic constructions based on the Learning With Errors assumption (Regev, STOC 2005). Such constructions are instances of latticebased cryptography and are extremely important due to their potential role in postquantum cryptography. Following (Barthe, Gregoire and Schmidt, CCS 2015), our approach combines a computational logic and deducibility problems—a standard tool for representing the adversary’s knowledge, the DolevYao model. The computational logic is used to capture (indistinguishabilitybased) security notions and drive the security proofs whereas deducibility problems are used as sideconditions to control that rules of the logic are applied correctly. We then use AutoLWE, an implementation of the logic, to deliver very short or even automatic proofs of several emblematic constructions, including CPAPKE (Gentry et al., STOC 2008), (Hierarchical) IdentityBased Encryption (Agrawal et al. Eurocrypt 2010), Inner Product Encryption (Agrawal et al. Asiacrypt 2011), CCAPKE (Micciancio et al., Eurocrypt 2012). The main technical novelty beyond AutoLWE is a set of (semi)decision procedures for deducibility problems, using extensions of Grobner basis computations for subalgebras in the noncommutative setting (instead of ideals in the commutative setting). Our procedures cover the theory of matrices, which is required for latticebased assumption, as well as the theory of noncommutative rings, fields, and DiffieHellman exponentiation, in its standard, bilinear and multilinear forms. Additionally, AutoLWE supports oraclerelative assumptions, which are used specifically to apply (advanced forms of) the Leftover Hash Lemma, an informationtheoretical tool widely used in latticebased proofs.more » « less

We present a highassurance and highspeed implementation of the SHA3 hash function. Our implementation is written in the Jasmin programming language, and is formally verified for functional correctness, provable security and timing attack resistance in the EasyCrypt proof assistant. Our implementation is the first to achieve simultaneously the four desirable properties (efficiency, correctness, provable security, and sidechannel protection) for a nontrivial cryptographic primitive. Concretely, our mechanized proofs show that: 1) the SHA3 hash function is indifferentiable from a random oracle, and thus is resistant against collision, first and second preimage attacks; 2) the SHA3 hash function is correctly implemented by a vectorized x86 implementation. Furthermore, the implementation is provably protected against timing attacks in an idealized model of timing leaks. The proofs include new EasyCrypt libraries of independent interest for programmable random oracles and modular indifferentiability proofs.more » « less

null (Ed.)We study several strengthening of classical circular security assumptions which were recently introduced in four new latticebased constructions of indistinguishability obfuscation: BrakerskiDottlingGargMalavolta (Eurocrypt 2020), GayPass (STOC 2021), BrakerskiDottlingGargMalavolta (Eprint 2020) and WeeWichs (Eprint 2020). We provide explicit counterexamples to the 2circular shielded randomness leakage assumption w.r.t. the GentrySahaiWaters fully homomorphic encryption scheme proposed by GayPass, and the homomorphic pseudorandom LWE samples conjecture proposed by WeeWichs. Our work suggests a separation between classical circular security of the kind underlying unlevelled fullyhomomorphic encryption from the strengthened versions underlying recent iO constructions, showing that they are not (yet) on the same footing. Our counterexamples exploit the flexibility to choose specific implementations of circuits, which is explicitly allowed in the GayPass assumption and unspecified in the WeeWichs assumption. Their indistinguishabilty obfuscation schemes are still unbroken. Our work shows that the assumptions, at least, need refinement. In particular, generic leakageresilient circular security assumptions are delicate, and their security is sensitive to the specific structure of the leakages involved.more » « less

The Schnorr signature scheme is an efficient digital signature scheme with short signature lengths, i.e., $4k$bit signatures for $k$ bits of security. A Schnorr signature $\sigma$ over a group of size $p\approx 2^{2k}$ consists of a tuple $(s,e)$, where $e \in \{0,1\}^{2k}$ is a hash output and $s\in \mathbb{Z}_p$ must be computed using the secret key. While the hash output $e$ requires $2k$ bits to encode, Schnorr proposed that it might be possible to truncate the hash value without adversely impacting security. In this paper, we prove that \emph{short} Schnorr signatures of length $3k$ bits provide $k$ bits of multiuser security in the (Shoup's) generic group model and the programmable random oracle model. We further analyze the multiuser security of keyprefixed short Schnorr signatures against preprocessing attacks, showing that it is possible to obtain secure signatures of length $3k + \log S + \log N$ bits. Here, $N$ denotes the number of users and $S$ denotes the size of the hint generated by our preprocessing attacker, e.g., if $S=2^{k/2}$, then we would obtain secure $3.75k$bit signatures for groups of up to $N \leq 2^{k/4}$ users. Our techniques easily generalize to several other FiatShamirbased signature schemes, allowing us to establish analogous results for ChaumPedersen signatures and KatzWang signatures. As a building block, we also analyze the $1$outof$N$ discretelog problem in the generic group model, with and without preprocessing.more » « less