We develop and implement AlgoROM, a tool to systematically analyze the security of a wide class of symmetric primitives in idealized models of computation. The schemes that we consider are those that can be expressed over an alphabet consisting of XOR and function symbols for hash functions, permutations, or block ciphers. We implement our framework in OCaml and apply it to a number of prominent constructions, which include the Luby-Rackoff (LR), key-alternating Feistel (KAF), and iterated Even-Mansour (EM) ciphers, as well as substitution-permutation networks (SPN). The security models we consider are (S)PRP, and strengthenings thereof under related-key (RK), key-dependent message (KD), and more generally key-correlated (KC) attacks. Using AlgoROM, we are able to reconfirm a number of classical and previously established security theorems, and in one case we identify a gap in a proof from the literature (Connolly et al., ToSC'19). However, most results that we prove with AlgoROM are new. In particular, we obtain new positive results for LR, KAF, EM, and SPN in the above models. Our results better reflect the configurations actually implemented in practice, as they use a single idealized primitive. In contrast to many existing tools, our automated proofs do not operate in symbolic models, but rather in the standard probabilistic model for cryptography.

We propose automated methods for synthesising attacks against indifferentiability, a powerful simulation-based notion of security commonly used to reason about symmetric-key constructions. Our methods are inspired from symbolic cryptography which is popular to reason about, e.g., cryptographic protocols. For that, we introduce a core programming language for algebraic distinguishers and study the class of universal distinguishers, who win the indifferentiability game against every simulator; then, we show that the universality of algebraic distinguishers can be reduced to solving systems of algebraic, deducibility and static-equivalence constraints.

Abstract Attribute-based encryption (ABE) is a form of public-key encryption that allows fine-grained access control on encrypted data. Blind key-generation (BKG) attribute-based encryption (Rial,Designs, Codes and Cryptography 2016) is a variant in which the master authority issues secret keys without learning any information about the attributes associated to them. This extra functionality makes it an appealing building block for several applications. In this work, we extend the generic framework of ABE based on pair encodings (Attrapadung,Eurocrypt 2014) to support blind key-generation. In particular, we define two new notions of pair encodings that we coinBKG-compatibleandalgebraicpair encoding. We show that every encoding satisfies the former without loss of generality, whereas the latter is satisfied by all existing pair encodings from the literature. We then show how to enhance any ABE based on a BKG-compatible pair encoding to achieve honest-but-curious blind key-generation. In the case of algebraic encodings, our protocol admits a very efficient version, secure against malicious parties. The main advantage of our work is generality. Our protocol is designed over the recent and most advanced modular frameworks of ABE that can handle a rich variety of predicates.

Abstract In a Functional Encryption scheme (FE), a trusted authority enables designated parties to compute specific functions over encrypted data. As such, FE promises to break the tension between industrial interest in the potential of data mining and user concerns around the use of private data. FE allows the authority to decide who can compute and what can be computed, but it does not allow the authority to control which ciphertexts can be mined. This issue was recently addressed by Naveed et al., that introduced so-called Controlled Functional encryption (or C-FE), a cryptographic framework that extends FE and allows the authority to exert fine-grained control on the ciphertexts being mined. In this work we extend C-FE in several directions. First, we distribute the role of (and the trust in) the authority across several parties by defining multi-authority C-FE (or mCFE). Next, we provide an efficient instantiation that enables computation of quadratic functions on inputs provided by multiple data-owners, whereas previous work only provides an instantiation for linear functions over data supplied by a single data-owner and resorts to garbled circuits for more complex functions. Our scheme leverages CCA2 encryption and linearly-homomorphic encryption. We also implement a prototype and use it to showcase the potential of our instantiation.

The problem of fair exchange consists of interchanging goods between two parties that do not trust each other. Despite known impossibility results, recent works leverage the block-chain and zero-knowledge proofs to implement zero-knowledge contingent payment (zkCP) systems that make fair exchange of digital goods possible. Implementing these systems in a secure and efficient way is a big challenge, as evidenced by several unsuccessful attempts from the literature. Campanelli et al. (ACM CCS 2017) discovered a vulnerability on an existing zkCP proposal based on SNARKs (succinct non-interactive arguments of knowledge) and suggested several repairs. Fuchsbauer (ACM CCS 2019) found a flaw in the mentioned countermeasures. In particular, he showed that witness-indistinguishability (WI) is not sufficient for the zkCP schemes proposed by Campanelli et al. to be secure. In this work, we observe that a slightly stronger notion of WI, that we coin trapdoor subversion WI (tS-WI), rules out Fuchsbauer's attack. We formally define security properties for CP systems and show that, under tS-WI, Campanelli et al.'s proposal indeed satisfies these properties. Additionally, we explore alternative approaches to implement ZK (other than SNARKs) and develop a prototype, using it to demonstrate their potential. Our new ideas result in a protocol to sell ECDSA signatures with contingent payment that can be executed in less than $150$ milliseconds over a LAN network.

Attribute-based encryption (ABE) is a cryptographic primitive which supports fine-grained access control on encrypted data, making it an appealing building block for many applications. In this paper, we propose, implement, and evaluate fully automated methods for proving security of ABE in the Generic Bilinear Group Model (Boneh, Boyen, and Goh, 2005, Boyen, 2008), an idealized model which admits simpler and more efficient constructions, and can also be used to find attacks. Our method is applicable to Rational-Fraction Induced ABE, a large class of ABE that contains most of the schemes from the literature, and relies on a Master Theorem, which reduces security in the GGM to a (new) notion of symbolic security, which is amenable to automated verification using constraint-based techniques. We relate our notion of symbolic security for Rational-Fraction Induced ABE to prior notions for Pair Encodings. Finally, we present several applications, including automated proofs for new schemes.