报告题目：Symbolic Proofs for Lattice-Based Cryptography

报告人：范雄博士

报告时间：2018年11月26日下午14点

报告地点：四川大学望江校区信息管理中心305会议室

报告内容：

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.

报告人简介：

Xiong Fan is a graduate student at Cornell University under the supervision of Prof. Elaine Shi. His main research interest is cryptography and programming languages, with current focus on lattice-based cryptography.  In particular, he focuses on how to develop and optimize advanced cryptographic schemes based on lattices that are secure against attacks by a quantum computer, and use computer-aided proof techniques to formally reason about the security of lattice-based cryptographic constructions.  He spent the summer of 2017 interning in the Cryptography Research Group at IBM T. J. Watson Research Center, the summer of 2016 working with Dr. Vladimir Kolesnikov at Bell Labs, and the summer of 2015 with Dr. Juan Garay and Dr. Payman Mohassel at Yahoo Labs.

欢迎感兴趣的老师和学生参加！

网络空间安全研究院

2018年11月21日