Author: Xiong Fan

Publisher:

Published: 2019

Total Pages: 199

ISBN-13:

Since the early works of Ajtai (STOC'96) and Regev (STOC'05), lattice-based cryptography has proven to be a powerful building block in cryptography. My research focuses on further exploring the expressive power of lattice-based cryptography, as well as formal verification of lattice-based cryptographic schemes. Deniable encryption (Canetti et al. CRYPTO '97) is an intriguing primitive that provides a security guarantee against not only eavesdropping attacks as required by semantic security, but also stronger coercion attacks performed after the fact. The concept of deniability has later demonstrated useful and powerful in many other contexts, such as leakage resilience, adaptive security of protocols, security against selective opening attacks and coercion resistance in voting systems. Despite its conceptual usefulness, our understanding of how to construct deniable primitives under standard assumptions is restricted. We construct a flexibly bi-deniable Attribute-Based Encryption (ABE) scheme for all polynomial-size Branching Programs from Learning With Errors assumption (Regev STOC'05). Attribute based encryption (ABE) is an advanced encryption system with a built-in mechanism to generate keys associated with functions which in turn provide restricted access to encrypted data. Most of the known candidates of attribute based encryption model the functions as circuits. This results in significant efficiency bottlenecks, especially in the setting where the function associated with the ABE key admits a RAM program whose runtime is sublinear in the length of the attribute. We study the notion of attribute based encryption for random access machines (RAMs), introduced in the work of Goldwasser, Kalai, Popa, Vaikuntanathan and Zeldovich (Crypto 2013) and present a construction satisfying sublinear decryption complexity assuming Learning With Errors. We then introduce 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. Our approach combines a computational logic, deducibility problems, a standard tool for representing the adversary's knowledge and 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. 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 lattice-based assumption, as well as the theory of non-commutative rings, fields, and Diffie-Hellman exponentiation, in its standard, bilinear and multilinear forms.