Symbolic Proofs for Lattice-Based Cryptography
Symbolic Proofs for Lattice-Based Cryptography
复制标题
DOI：
10.1145/3243734.3243825
复制
发表时间：
2018-10
期刊：
影响因子：
--
通讯作者：
G. Barthe;Xiong Fan;Joshua Gancher;B. Grégoire;Charlie Jacomme;E. Shi
中科院分区：
文献类型：
--
作者：
G. Barthe;Xiong Fan;Joshua Gancher;B. Grégoire;Charlie Jacomme;E. Shi
符号方法已被广泛用于证明Dolev-Yao模型中密码协议的安全性，最近用于证明计算模型中密码原语和构造的安全性。然而，现有的方法来证明安全的密码结构的计算模型往往需要大量的专业知识和互动，或相当有限的范围和表现力。本文介绍了一种基于错误学习假设（Regev，STOC 2005）的密码构造安全性证明的符号方法。这种构造是基于格的密码学的实例，并且由于它们在后量子密码学中的潜在作用而非常重要。继（Barthe，Grégoire和施密特，CCS 2015），我们的方法结合了计算逻辑和演绎问题-一个代表对手知识的标准工具，Dolev-Yao模型。计算逻辑用于捕获（基于不可验证性的）安全概念并驱动安全证明，而演绎问题用作侧条件以控制逻辑规则的正确应用。然后，我们使用AutoLWE（逻辑的一种实现）来提供几种象征性构造的非常短甚至自动的证明，包括CPA-PKE（Gentry et al.，STOC 2008）、（分层）基于身份的加密（Agrawal等人，Eurocrypt 2010）、内部产品加密（Agrawal等人，Asiacrypt 2011）、CCA-PKE（Micciancio等人，Eurocrypt 2012）。AutoLWE之外的主要技术新奇是一组用于演绎问题的（半）决策程序，使用（非）交换设置中的子代数的Gröbner基计算的扩展（而不是交换设置中的理想）。我们的程序涵盖了理论的矩阵，这是必要的基于格的假设，以及理论的非交换环，字段，和Diffie-Hellman指数，在其标准，双线性和多线性形式。此外，AutoLWE支持预言机相关的假设，这些假设专门用于应用（高级形式的）剩余哈希引理，这是一种广泛用于基于格的证明的信息理论工具。
Symbolic methods have been used extensively for proving security of cryptographic protocols in the Dolev-Yao 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 lattice-based cryptography and are extremely important due to their potential role in post-quantum cryptography. Following (Barthe, Grégoire and Schmidt, CCS 2015), our approach combines a computational logic and deducibility problems---a standard tool for representing the adversary's knowledge, the Dolev-Yao model. The computational logic is used to capture (indistinguishability-based) security notions and drive the security proofs whereas deducibility problems are used as side-conditions 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) Identity-Based Encryption (Agrawal et al. Eurocrypt 2010), Inner Product Encryption (Agrawal et al. Asiacrypt 2011), CCA-PKE (Micciancio et al., Eurocrypt 2012). The main technical novelty beyond AutoLWE is a set of (semi-)decision procedures for deducibility problems, using extensions of Gröbner 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 lattice-based assumption, as well as the theory of non-commutative rings, fields, and Diffie-Hellman exponentiation, in its standard, bilinear and multilinear forms. Additionally, AutoLWE supports oracle-relative assumptions, which are used specifically to apply (advanced forms of) the Leftover Hash Lemma, an information-theoretical tool widely used in lattice-based proofs.