International Association
for Cryptologic Research

We present CrypTFlow, a first of its kind system that converts TensorFlow inference code into Secure Multi-party Computation (MPC) protocols at the push of a button. To do this, we build three components. Our first component, Athos, is an end-to-end compiler from TensorFlow to a variety of semi-honest MPC protocols. The second component, Porthos, is an improved semi-honest 3-party protocol that provides significant speedups for Tensorflow like applications. Finally, to provide malicious secure MPC protocols, our third component, Aramis, is a novel technique that uses hardware with integrity guarantees to convert any semi-honest MPC protocol into an MPC protocol that provides malicious security. The security of the protocols output by Aramis relies on hardware for integrity and MPC for confidentiality. Moreover, our system, through the use of a new float-to-fixed compiler, matches the inference accuracy over the plaintext floating-point counterparts of these networks.

We experimentally demonstrate the power of our system by showing the secure inference of real-world neural networks such as ResNet50, DenseNet121, and SqueezeNet over the ImageNet dataset with running times of about 30 seconds for semi-honest security and under two minutes for malicious security. Prior work in the area of secure inference (SecureML, MiniONN, HyCC, ABY$^3$, CHET, EzPC, Gazelle, and SecureNN) has been limited to semi-honest security of toy networks with 3--4 layers over tiny datasets such as MNIST or CIFAR which have 10 classes. In contrast, our largest network has 200 layers, 65 million parameters and over 1000 ImageNet classes. Even on MNIST/CIFAR, CrypTFlow outperforms prior work.

In the article we propose a new compression method (to $2\log_2(p) + 3$ bits) for the $\mathbb{F}_{\!p^2}$-points of an elliptic curve $E_b\!: y^2 = x^3 + b$ (for $b \in \mathbb{F}_{\!p^2}^*$) of $j$-invariant $0$. It is based on $\mathbb{F}_{\!p}$-rationality of some generalized Kummer surface $GK_b$. This is the geometric quotient of the Weil restriction $R_b := \mathrm{R}_{\: \mathbb{F}_{\!p^2}/\mathbb{F}_{\!p}}(E_b)$ under the order $3$ automorphism restricted from $E_b$. More precisely, we apply the theory of conic bundles (i.e., conics over the function field $\mathbb{F}_{\!p}(t)$) to obtain explicit and quite simple formulas of a birational $\mathbb{F}_{\!p}$-isomorphism between $GK_b$ and $\mathbb{A}^{\!2}$. Our point compression method consists in computation of these formulas. To recover (in the decompression stage) the original point from $E_b(\mathbb{F}_{\!p^2}) = R_b(\mathbb{F}_{\!p})$ we find an inverse image of the natural map $R_b \to GK_b$ of degree $3$, i.e., we extract a cubic $\mathbb{F}_{\!p}$-root. For $p \not\equiv 1 \: (\mathrm{mod} \ 27)$ this is just a single exponentiation in $\mathbb{F}_{\!p}$, hence the new method seems to be much faster than the classical one with $x$ coordinate, which requires two exponentiations in $\mathbb{F}_{\!p}$. In particular, it is perfectly applicable to pairing-friendly elliptic curves from one IETF-draft and to those used in the cryptocurrencies Ethereum and Zcash.

We present a methodology to construct preprocessing zkSNARKs where the structured reference string (SRS) is universal and updatable. This exploits a novel use of *holography* [Babai et al., STOC 1991], where fast verification is achieved provided the statement being checked is given in encoded form.

We use our methodology to obtain a preprocessing zkSNARK where the SRS has linear size and arguments have constant size. Our construction improves on Sonic [Maller et al., CCS 2019], the prior state of the art in this setting, in all efficiency parameters: proving is an order of magnitude faster and verification is thrice as fast, even with smaller SRS size and argument size. Our construction is most efficient when instantiated in the algebraic group model (also used by Sonic), but we also demonstrate how to realize it under concrete knowledge assumptions. We implement and evaluate our construction.

The core of our preprocessing zkSNARK is an efficient *algebraic holographic proof* (AHP) for rank-1 constraint satisfiability (R1CS) that achieves linear proof length and constant query complexity.

The task of function inversion is central to cryptanalysis: breaking block ciphers, forging signatures, and cracking password hashes are all special cases of the function-inversion problem. In 1980, Hellman showed that it is possible to invert a random function $f\colon [N] \to [N]$ in time $T = \widetilde{O}(N^{2/3})$ given only $S = \widetilde{O}(N^{2/3})$ bits of precomputed advice about $f$. Hellman’s algorithm is the basis for the popular “Rainbow Tables” technique (Oechslin, 2003), which achieves the same asymptotic cost and is widely used in practical cryptanalysis.

Is Hellman’s method the best possible algorithm for inverting functions with preprocessed advice? The best known lower bound, due to Yao (1990), shows that $ST = \widetilde{\Omega}(N)$, which still admits the possibility of an $S = T = \widetilde{O}(N^{1/2})$ attack. There remains a long-standing and vexing gap between Hellman’s $N^{2/3}$ upper bound and Yao’s $N^{1/2}$ lower bound. Understanding the feasibility of an $S = T = N^{1/2}$ algorithm is cryptanalytically relevant since such an algorithm could perform a key-recovery attack on AES-128 in time $2^{64}$ using a precomputed table of size $2^{64}$.

For the past 29 years, there has been no progress either in improving Hellman’s algorithm or in strengthening Yao’s lower bound. In this work, we connect function inversion to problems in other areas of theory to (1) explain why progress may be difficult and (2) explore possible ways forward.

Our results are as follows:

- We show that *any* improvement on Yao’s lower bound on function-inversion algorithms will imply new lower bounds on depth-two circuits with arbitrary gates. Further, we show that proving strong lower bounds on *non-adaptive* function-inversion algorithms would imply breakthrough circuit lower bounds on linear-size log-depth circuits.

- We take first steps towards the study of the *injective* function-inversion problem, which has manifold cryptographic applications. In particular, we show that improved algorithms for breaking PRGs with preprocessing would give improved algorithms for inverting injective functions with preprocessing.

- Finally, we show that function inversion is closely related to well-studied problems in communication complexity and data structures. Through these connections we immediately obtain the best known algorithms for problems in these domains.

In predicate encryption for a function $f$, an authority can create ciphertexts and secret keys which are associated with `attributes'. A user with decryption key $K_y$ corresponding to attribute $y$ can decrypt a ciphertext $CT_x$ corresponding to a message $m$ and attribute $x$ if and only if $f(x,y)=0$. Furthermore, the attribute $x$ remains hidden to the user if $f(x,y) \neq 0$.

We construct predicate encryption from assumptions on bilinear maps for a large class of new functions, including sparse set disjointness, Hamming distance at most $k$, inner product mod 2, and any function with an efficient Arthur-Merlin communication protocol. Our construction uses a new probabilistic representation of Boolean functions we call `one-sided probabilistic rank,' and combines it with known constructions of inner product encryption in a novel way.

In a recent work, Garg, Hajiabadi, Mahmoody, and Rahimi (TCC 18) introduced a new encryption framework, which they referred to as Registration-Based Encryption (RBE). The central motivation behind RBE was to provide a novel methodology for solving the well-known key-escrow problem in Identity-Based Encryption (IBE) systems. Informally, in an RBE system there is no private-key generator unlike IBE systems, but instead it is replaced with a public key accumulator. Every user in an RBE system samples its own public-secret key pair, and sends the public key to the accumulator for registration. The key accumulator has no secret state, and is only responsible for compressing all the registered user identity-key pairs into a short public commitment. Here the encryptor only requires the compressed parameters along with the target identity, whereas a decryptor requires supplementary key material along with the secret key associated with the registered public key.

The initial construction by Garg et al. (TCC 18) based on standard assumptions only provided weak efficiency properties. In a follow-up work by Garg, Hajiabadi, Mahmoody, Rahimi, and Sekar (PKC 19), they gave an efficient RBE construction from standard assumptions. However, both these works considered the key accumulator to be honest which might be too strong an assumption in real-world scenarios. In this work, we initiate a formal study of RBE systems with malicious key accumulators. To that end, we introduce a strengthening of the RBE framework which we call Verifiable RBE (VRBE). A VRBE system additionally gives the users an extra capability to obtain short proofs from the key accumulator proving correct (and unique) registration for every registered user as well as proving non-registration for any yet unregistered identity.

We construct VRBE systems which provide succinct proofs of registration and non-registration from standard assumptions (such as CDH, Factoring, LWE). Our proof systems also naturally allow a much more efficient audit process which can be perfomed by any non-participating third party as well. A by-product of our approach is that we provide a more efficient RBE construction than that provided in the prior work of Garg et al. (PKC 19). And, lastly we initiate a study on extension of VRBE to a wider range of access and trust structures.

Bluetooth is a widely deployed standard for wireless communications between mobile devices. It uses authenticated Elliptic Curve Diffie-Hellman for its key exchange. In this paper we show that the authentication provided by the Bluetooth pairing protocols is insufficient and does not provide the promised MitM protection. We present a new attack that modifies the y-coordinates of the public keys (while preserving the x-coordinates). The attack compromises the encryption keys of all of the current Bluetooth authenticated pairing protocols, provided both paired devices are vulnerable. Specifically, it successfully compromises the encryption keys of 50% of the Bluetooth pairing attempts, while in the other 50% the pairing of the victims is terminated. The affected vendors have been informed and patched their products accordingly, and the Bluetooth specification had been modified to address the new attack. We named our new attack the “Fixed Coordinate Invalid Curve Attack”. Unlike the well known “Invalid Curve Attack” of Biehl et. al. which recovers the private key by sending multiple specially crafted points to the victim, our attack is a MitM attack which modifies the public keys in a way that lets the attacker deduce the shared secret.

We present a machine-checked proof of security for the domain management protocol of Amazon Web Services' KMS (Key Management Service) a critical security service used throughout AWS and by AWS customers. Domain management is at the core of AWS KMS; it governs the top-level keys that anchor the security of encryption services at AWS. We show that the protocol securely implements an ideal distributed encryption mechanism under standard cryptographic assumptions. The proof is machine-checked in the EasyCrypt proof assistant and is the largest EasyCrypt development to date.

Vehicular Ad-hoc Networks (VANETs) are a cardinal part of intelligent transportation system (ITS) which render various services in terms of traffic and transport management. The VANET is used to manage growing traffic and manage data about traffic conditions, weather, road conditions, speed of the vehicle, etc. Even though, VANETs are self-sufficient and effective networks but they still suffer from various security and privacy issues. VANETs need to ensure that an adversary should not be able to breach user associated data and delete or modify the exchanged messages for its gains, as these messages comprise of sensitive data. In this paper, we have proposed an authentication and key-agreement protocol based on cryptographic hash functions which makes it lightweight in nature and also suitable for VANET environment. Moreover, to enhance the security and reliability of the entire system, the proposed key-agreement protocol makes use of random session modulus to compute a dynamic session key i.e. for every session, vehicles generate their session specific secret modulus which are then converged to form a common group session key. The formal verification of the proposed work is done using Real - or - Random oracle model, AVISPA and BAN Logic while informal security analysis shows that the proposed protocol can withstand various attacks. The simulation results and analysis prove that the proposed work is efficient and has a real-time application in VANET environment.

Existing logic obfuscation approaches aim to protect hardware design IPs from SAT attack by increasing query count and output corruptibility of a locked netlist. In this paper, we demonstrate the ineffectiveness of such techniques to obfuscate hardware accelerator platforms. Subsequently, we propose a Hardware/software co-design based Accelerator Obfuscation (HSCAO) scheme to provably safeguard the IP of such designs against SAT as well as removal/bypass type of attacks while still maintaining high output corruptability for applications. The attack resiliency of HSCAO scheme is manifested by using a sequence of keys to obfuscate instruction encoding for an application. Experimental evaluations utilizing an accelerator simulator demonstrate the effectiveness of our proposed countermeasure.

With the burgeoning Vehicle-to-Everything (V2X) communication, security and privacy concerns are paramount. Such concerns are usually mitigated by combining cryptographic mechanisms with suitable key management architecture. However, cryptographic operations may be quite resource-intensive, placing a considerable burden on the vehicle’s V2X computing unit. To assuage this issue, it is reasonable to use hardware acceleration for common cryptographic primitives, such as block ciphers, digital signature schemes, and key exchange protocols. In this scenario, custom extension instructions can be a plausible option, since they achieve fine-tune hardware acceleration with a low to moderate logic overhead, while also reducing code size. In this article, we apply this method along with dual-data memory banks for the hardware acceleration of the PRESENT block cipher, as well as for the $F_{2^{255}-19}$ finite field arithmetic employed in cryptographic primitives based on Curve25519 (e.g., EdDSA and X25519). As a result, when compared with a state-of-the-art software-optimized implementation, the performance of PRESENT is improved by a factor of 17 to 34 and code size is reduced by 70%, with only a 4.37% increase in FPGA logic overhead. In addition, we improve the performance of operations over Curve25519 by a factor of ~2.5 when compared to an Assembly implementation on a comparable processor, with moderate logic overhead (namely, 9.1%). Finally, we achieve significant performance gains in the V2X provisioning process by leveraging our hardware-accelerated cryptographic primitives

Event date: 15 April to 17 April 2020
Submission deadline: 26 November 2019
Notification: 20 January 2020

We present a searchable encryption scheme for dynamic document collections in a multi-user scenario. Our scheme features fine-grained access control to search results, as well as access control to operations such as adding documents to the document collection, or changing individual documents. The scheme features verifiability of search results. Our scheme also satisfies the forward privacy notion crucial for the security of dynamic searchable encryption schemes.

Card-based cryptography provides simple and practicable protocols for performing secure multi-party computation (MPC) with just a deck of cards. For the sake of simplicity, this is often done using cards with only two symbols, e.g., clubs and hearts. Within this paper, we target the setting where all cards carry distinct symbols, catering for use-cases with commonly available standard decks and a weaker indistinguishability assumption. As of yet, the literature provides for only three protocols and no proofs for non-trivial lower bounds on the number of cards. As such complex proofs (handling very large combinatorial state spaces) tend to be involved and error-prone, we propose using formal verification for finding protocols and proving lower bounds. In this paper, we employ the technique of software bounded model checking (SBMC), which reduces the problem to a bounded state space, which is automatically searched exhaustively using a SAT solver as a backend.

Our contribution is twofold: (a) We identify two protocols for converting between different bit encodings with overlapping bases, and then show them to be card-minimal. This completes the picture of tight lower bounds on the number of cards with respect to runtime behavior and shuffle properties of conversion protocols. For computing AND, we show that there is no protocol with finite runtime using four cards with distinguishable symbols and fixed output encoding, and give a four-card protocol with an expected finite runtime using only random cuts. (b) We provide a general translation of proofs for lower bounds to a bounded model checking framework for automatically finding card- and length-minimal protocols and to give additional confidence in lower bounds. We apply this to validate our method and, as an example, confirm our new AND protocol to have a shortest run for protocols using this number of cards.

ISO/IEC standardizes several chosen ciphertext-secure key encapsulation mechanism (KEM) schemes in ISO/IEC 18033-2. However, all ISO/IEC KEM schemes are not quantum resilient. In this paper, we introduce new isogeny-based KEM schemes (i.e., CSIDH-ECIES-KEM and CSIDH-PSEC-KEM) by modifying Diffie-Hellman-based KEM schemes in ISO/IEC standards. The main advantage of our schemes are compactness. The key size and the ciphertext overhead of our schemes are about five times smaller than these of SIKE-KEM which is submitted to NIST's post-quantum cryptosystems standardization.

The LLL algorithm takes as input a basis of a Euclidean lattice, and, within a polynomial number of operations, it outputs another basis of the same lattice but consisting of rather short vectors. We provide a generalization to R-modules contained in K^n for arbitrary number fields K and dimension n, with R denoting the ring of integers of K. Concretely, we introduce an algorithm that efficiently finds short vectors in rank-n modules when given access to an oracle that finds short vectors in rank-2 modules, and an algorithm that efficiently finds short vectors in rank-2 modules given access to a Closest Vector Problem oracle for a lattice that depends only on K. The second algorithm relies on quantum computations and its analysis is heuristic.

In this work we advance the study of leakage-resilient Authenticated Encryption with Associated Data (AEAD) and lay the theoretical groundwork for building such schemes from sponges. Building on the work of Barwell et al. (ASIACRYPT 2017), we reduce the problem of constructing leakage-resilient AEAD schemes to that of building fixed-input-length function families that retain pseudorandomness and unpredictability in the presence of leakage. Notably, neither property is implied by the other in the leakage-resilient setting. We then show that such a function family can be combined with standard primitives, namely a pseudorandom generator and a collision-resistant hash, to yield a nonce-based AEAD scheme. In addition, our construction is quite efficient in that it requires only two calls to this leakage-resilient function per encryption or decryption call. This construction can be instantiated entirely from the T-sponge to yield a concrete AEAD scheme which we call SLAE. We prove this sponge-based instantiation secure in the non-adaptive leakage setting. SLAE bears many similarities and is indeed inspired by ISAP, which was proposed by Dobraunig et al. at FSE 2017. However, while retaining most of the practical advantages of ISAP, SLAE additionally benefits from a formal security treatment.

The customary formulation of authenticated encryption (AE) requires the decrypting party to supply the correct nonce with each ciphertext it decrypts. To enable this, the nonce is often sent in the clear alongside the ciphertext. But doing this can forfeit anonymity and degrade usability. Anonymity can also be lost by transmitting associated data (AD) or a session-ID (used to identify the operative key). To address these issues, we introduce anonymous AE, wherein ciphertexts must conceal their origin even when they are understood to encompass everything needed to decrypt (apart from the receiver's secret state). We formalize a type of anonymous AE we call anAE, anonymous nonce-based AE, which generalizes and strengthens conventional nonce-based AE, nAE. We provide an efficient construction for anAE, NonceWrap, from an nAE scheme and a blockcipher. We prove NonceWrap secure. While anAE does not address privacy loss through traffic-flow analysis, it does ensure that ciphertexts, now more expansively construed, do not by themselves compromise privacy.

We study the possibility of achieving full security, with guaranteed output delivery, for secure multiparty computation of functionalities where only one party receives output, to which we refer as solitary functionalities. In the standard setting where all parties receive an output, full security typically requires an honest majority; otherwise even just achieving fairness is impossible. However, for solitary functionalities, fairness is clearly not an issue. This raises the following question: Is full security with no honest majority possible for all solitary functionalities? We give a negative answer to this question, by showing the existence of solitary functionalities that cannot be computed with full security. While such a result cannot be proved using fairness based arguments, our proof builds on the classical proof technique of Cleve (STOC 1986) for ruling out fair coin-tossing and extends it in a nontrivial way. On the positive side, we show that full security against any number of malicious parties is achievable for many natural and useful solitary functionalities, including ones for which the multi-output version cannot be realized with full security.

Event date: 17 June to 19 June 2020
Submission deadline: 16 December 2019
Notification: 5 March 2020