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),more »
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 more »
 Award ID(s):
 1815546
 Publication Date:
 NSFPAR ID:
 10208485
 Journal Name:
 Lecture notes in computer science
 Volume:
 10991
 Page Range or eLocationID:
 693721
 ISSN:
 03029743
 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 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 etmore »

Pass, Rafael ; Pietrzak, Krzysztof (Ed.)In the backdoored randomoracle (BRO) model, besides access to a random function H , adversaries are provided with a backdoor oracle that can compute arbitrary leakage functions f of the function table of H . Thus, an adversary would be able to invert points, find collisions, test for membership in certain sets, and more. This model was introduced in the work of Bauer, Farshim, and Mazaheri (Crypto 2018) and extends the auxiliaryinput idealized models of Unruh (Crypto 2007), Dodis, Guo, and Katz (Eurocrypt 2017), Coretti et al. (Eurocrypt 2018), and Coretti, Dodis, and Guo (Crypto 2018). It was shown that certain security properties, such as onewayness, pseudorandomness, and collision resistance can be reestablished by combining two independent BROs, even if the adversary has access to both backdoor oracles. In this work we further develop the technique of combining two or more independent BROs to render their backdoors useless in a more general sense. More precisely, we study the question of building an indifferentiable and backdoorfree random function by combining multiple BROs. Achieving full indifferentiability in this model seems very challenging at the moment. We however make progress by showing that the xor combiner goes well beyond security against preprocessing attacksmore »

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.

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 analogousmore »