Zero Knowledge (ZK) as a technique has been invented 35 years ago, and since then it gained many theoretical implications to cryptographic research and enabled various cryptographic primitives, and the centrality of the notion is very well established in cryptography. Further, in the last few years concrete applications of ZK have been developed primarily as part of the cryptocurrency wave but also elsewhere. Efficient methods have been found and implemented etc. to solve actual (i.e., industry) problems in systems.

In this talk I will review some properties of ZK from an industrial perspective, and how it became handy and uniquely positioned for concrete deployed solutions in my own experience, and how the availability of the techniques matched exactly and uniquely what was needed in actual applications under actual trust and threat settings.

Zero-knowledge proofs and in particular succinct non-interactive zero-knowledge proofs (so called zk-SNARKs) are getting increasingly used in real-world applications, with cryptocurrencies being the prime example. Simulation extractability (SE) is a strong security notion of zk-SNARKs which informally ensures non-malleability of proofs, which is considered highly important in practical applications. Another problematic issue for the practical use of zk-SNARKs is the requirement of a fully trusted setup, as especially for large-scale decentralized applications finding a trusted party that runs the setup is practically impossible. Quite recently, the study of approaches to relax or even remove the trust in the setup procedure, and in particular subversion as well as updatable zk-SNARKs (with latter being the most promising approach), has been initiated and received considerable attention since then. Unfortunately, so far SE-SNARKs with aforementioned properties are only constructed in an ad-hoc manner and no generic techniques are available.

In this SoK paper we present the state-of-the-art in generic techniques to obtain SE subversion and updatable SNARKs. In particular, we present a revisited version of the lifting technique due to Kosba et al. (called C∅C∅). This revisited version called OC∅C∅ explores the design space of many recently proposed SNARK- and STARK-friendly symmetric-key primitives. While C∅C∅ and OC∅C∅ are compatible with subversion SNARKs, they are not compatible with updatable SNARKs. Then, we present another lifting transformation called Lamassu, which is build upon key-homomorphic signatures as well as so called updatable signatures. Lamassu preserves the subversion and in particular updatable properties of the underlying zk-SNARK. Finally, we present an comprehensive comparison of these lifting transformations with ad-hoc techniques as well as a discussion of many aspects regarding the instantiation of the techniques.

Existing models for non-interactive MPC necessarily require leakage of the residual function – the output of the function on the honest parties’ inputs together with all possible settings of the adversarial inputs. We present a new MPC model which enables to circumvent this lower bound.

To achieve this, we utilize a blockchain in a novel way, incorporating smart contracts and (arbitrary) miners as participants. Security is maintained under a monetary assumption on the computational resources of the adversary in relation to those of the honest parties. This yields non-interactive MPC protocols with very strong security guarantees in the short term. Over time, as the adversary can invest more and more computational resources, the security guarantee decays. Thus, our model, which we call Gage MPC, is very suitable for secure computation with limited-time secrecy, such as auctions over the blockchain.

A key ingredient in our protocols is a new primitive we call “Gage Time Capsules” (GaTC) which utilize zero-knowledge proofs.

Joint work: Ghada Almashaqbeh, Fabrice Benhamouda. Seungwook Han, Daniel Jaroslawicz , Tal Malkin, Alex Nicita. Abhishek Shah, Eran Tromer

$\Sigma$-protocols provide a method to obtain efficient zero knowledge. In this work we first use CryptHOL~\cite{DBLP:journals/afp/Lochbihler17}, a framework embedded inside Isabelle/HOL, to provide a fully formalised theory of $\Sigma$-protocols. Our formalisation proves secure multiple case studies namely; the Schnorr, Chaum-Pedersen and Okamoto $\Sigma$-protocols as well as a construction that allows for compound (AND and OR) $\Sigma$-protocols.

This work also reports on our fully formalised theory of commitment schemes. A highlight of the work is a formalisation of the construction of commitment schemes from $\Sigma$-protocols \cite{sigma_protocols}. We formalise this proof at an abstract level using the modularity available in Isabelle/HOL and CryptHOL. This way, the proofs of the instantiations come for free.

Formal verification of proofs of security is important to increase the rigour of provable security. In particular they allow the proofs to be scrutinised in a level of detail beyond that which is available in paper proofs. For example, in this work, we are able to highlight which of the numerous definitions of $\Sigma$-protocols in the literature is the correct one.

We believe this work lays strong foundations for providing a fully formalised theory of Zero-Knowledge using CryptHOL. It is however, unclear what form this formalisation should take to be of most use for Cryptographers? Is a formalised definitional theory sufficient, or are there certain results that the community would benefit from being formalised?

All definitions and statements presented in this work have been formalised in CryptHOL and are available online.

One of the main applications of zero-knowledge proofs is the design and construction of cryptographic protocols, typically by proving knowledge of values that are inputs and/or output of selected cryptographic primings. For instance, a group signature scheme can be realised as a proof of knowledge of an encrypted value that is signed by the group manager. Now, to obtain efficient protocols, it is essentials that the zero-knowledge proofs and the cryptographic primitives interact well.

In this talk we will give a brief overview different construction frameworks of compatible primitives and zero-knowledge proofs and then discuss open problems and challenges that arise when folding these protocol construction frameworks are folded into security modelling frameworks such as UC.

In this work, we design and implement the first protocol for RSA modulus construction that can support thousands of parties and offers security against an arbitrary number of corrupted parties. In a nutshell, we design the ``best'' protocol for this scale that is secure against passive corruption, then amplify it to obtain active security using efficient non-interactive zero-knowledge arguments. Our protocol satisfies a stronger security guarantee where a deviating party can be identified when the protocol aborts (referred to as security with identifiable-abort) and allows for "public verifiability".

We instantiate our ZK proof system by composing two different types of ZK proof systems: (1) the Ligero sub-linear zero-knowledge proof system (Ames et al., CCS 2017), and (2) Sigma-protocol for proving the knowledge of a discrete logarithm in unknown order groups (Shoup, Eurocrypt 2000).

We implemented both the passive and the active variants of our protocol and ran experiments using 2--4000 parties. For generating a 2048-bit modulus among 1,000 parties, our passive protocol executed in under 4 minutes and the active variant ran in 22 minutes. In all our experiments, we ran each party on a t3.small AWS EC2 instance (2 vCPUs, 2GB RAM, up to 2Mbps) and the coordinator on a r5dn.24xlarge instance (96 vCPUs, 768GB RAM, up to 100Gbps).

We highlight that this is the first implementation that:(1) Scales an MPC protocol to more than 1000 parties, (2) Demonstrates viability of the classic GMW compiler from passive to active, and (3) Implements a zero-knowledge prover of a large NP statement in a memory/cpu constrained environment.

This is a joint work with Megan Chen, Yuval Ishai, Yuriy Kashnikov, Daniele Micciancio, Tarik Riviere, abhi shelat, Muthu Venkitasubramaniam and Ruihan Wang.

This talk focuses on hardware acceleration of modular multiplication and its application to the blockchain ecosystem. While there have been many exciting new developments in computer science and cryptography over the past decade, less effort has been spent on how to make these new techniques computationally practical. By increasing the performance of modular multiplication, novel cryptographic techniques like VDFs, SNARKs, and Accumulators can become feasible, enabling blockchain protocols to reduce their compute, storage, and networking requirements. This talk will discuss techniques for optimization across CPU, GPU, FPGA, and ASIC architectures, as well as both algorithmic and numerical representation techniques that enable improved performance. We will provide concrete data from recent optimization work on different architectures for RSA-based cryptography, and discuss the viability of this approach to improve blockchain security and scalability. The talk will conclude with a discussion of developments that have <1% the latency of a CPU system, and over 1000 times the throughput of a CPU core.