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 »
Shorter and Faster PostQuantum DesignatedVerifier zkSNARKs from Lattices
Zeroknowledge succinct arguments of knowledge (zkSNARKs) enable efficient privacypreserving proofs of membership for general NP languages. Our focus in this work is on postquantum zkSNARKs, with a focus on minimizing proof size. Currently, there is a 1000x gap in the proof size between the best prequantum constructions and the best postquantum ones. Here, we develop and implement new latticebased zkSNARKs in the designatedverifier preprocessing model. With our construction, after an initial preprocessing step, a proof for an NP relation of size 2^20 is just over 16 KB. Our proofs are 10.3x shorter than previous postquantum zkSNARKs for general NP languages.
Compared to previous latticebased zkSNARKs (also in the designatedverifier preprocessing model), we obtain a 42x reduction in proof size and a 60x reduction in the prover's running time, all while achieving a much higher level of soundness. Compared to the shortest prequantum zkSNARKs by Groth (Eurocrypt 2016), the proof size in our latticebased construction is 131x longer, but both the prover and the verifier are faster (by 1.2x and 2.8x, respectively). Our construction follows the general blueprint of Bitansky et al. (TCC 2013) and Boneh et al. (Eurocrypt 2017) of combining a linear probabilistically checkable proof (linear PCP) together with more »
 Publication Date:
 NSFPAR ID:
 10310224
 Journal Name:
 ACM Conference on Computer and Communications Security (CCS)
 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 »

We provide a modified version of the Ligero sublinear zero knowledge proof system for arithmetic circuits provided by Ames et. al. (CCS ‘17). Our modification "BooLigero" tailors Ligero for use in Boolean circuits to achieve a significant improvement in proof size. Although the original Ligero system could be used for Boolean circuits, Ligero generally requires allocating an entire field element to represent a single bit on a wire in a Boolean circuit. In contrast, our system performs operations over words of bits, allowing a proof size savings of between O(log(F)^1/4) and O(log(F)^1/2) compared to Ligero, where F is the field that leads to the optimal proof size in original Ligero. We achieve improvements in proof size of approximately 1.11.6x for SHA2 and 1.72.8x for SHA3. In addition to checking constraints of standard Boolean operations such as AND, XOR, and NOT over words, BooLigero also supports several other constraints such as multiplication in GF(2^w), bit masking, bit rearrangement within and across words, and bitwise outer product. Like Ligero, construction requires no trusted setup and no computational assumptions, which is ideal for blockchain applications. It is plausibly postquantum secure in the standard model. Furthermore, it is publiccoin, perfect honestverifier zero knowledge, andmore »

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 »

Tessaro, Stefano (Ed.)A Proof of Sequential Work (PoSW) allows a prover to convince a resourcebounded verifier that the prover invested a substantial amount of sequential time to perform some underlying computation. PoSWs have many applications including timestamping, blockchain design, and universally verifiable CPU benchmarks. Mahmoody, Moran, and Vadhan (ITCS 2013) gave the first construction of a PoSW in the random oracle model though the construction relied on expensive depthrobust graphs. In a recent breakthrough, Cohen and Pietrzak (EUROCRYPT 2018) gave an efficient PoSW construction that does not require expensive depthrobust graphs. In the classical parallel random oracle model, it is straightforward to argue that any successful PoSW attacker must produce a long ℋsequence and that any malicious party running in sequential time T1 will fail to produce an ℋsequence of length T except with negligible probability. In this paper, we prove that any quantum attacker running in sequential time T1 will fail to produce an ℋsequence except with negligible probability  even if the attacker submits a large batch of quantum queries in each round. The proof is substantially more challenging and highlights the power of Zhandry’s recent compressed oracle technique (CRYPTO 2019). We further extend this result to establish postquantum securitymore »