Seminars (SASW02)

I will present a new notion of fully homomorphic encryption (FHE) called multi-key FHE that permits computation on data encrypted under multiple unrelated keys, a new construction of multi-key FHE based on the NTRU encryption scheme, and a new application of multi-key FHE to the problem of constructing minimally interactive cloud-assisted secure multi-party computation protocols. Joint Work with Adriana Lopez-Alt (NYU) and Eran Tromer (Tel-Aviv U).

We unify the treatment of asymmetry of information in theoretical computer science and economics. We put forward a new type of proof system, where an unbounded Prover and a polynomial time Verifier interact, on inputs a string x and a function f, so that the Verifier may learn f(x). In our setting there no longer are “good” or “malicious” Provers, but only RATIONAL ones. In essence, (1) the Verifier gives the Prover a reward in [0,1] determined by the transcript of their interaction; (2) the Prover wishes to maximize his expected reward; and (3) the reward is maximized only if the verifier correctly learns f(x). Rational proofs are as powerful as interactive ones, but can be amazingly more efficient in the amount of communication involved: that is, the number of bits exchanged and the number of rounds of interaction. Joint work with Pablo Azar.

Garbled circuits, a classical idea rooted in the work of A. Yao, have generally been understood as a cryptographic *technique*, not a cryptographic *goal*. Here we treat garbled circuits as a proper cryptographic primitive, giving a syntax for a "garbling scheme" and formalizing several security notions for such schemes. The most basic of our notions, "privacy", suffices for the classical goals of two-party secure function evaluation (SFE) and private function evaluation (PFE). We provide a simple and efficient garbling scheme achieving privacy, this built from a block cipher, and we analyze its concrete security. We next consider the "authenticity" and "obliviousness" of a garbling scheme, extending the blockcipher-based protocol to achieve these ends, too. Our treatment of garbling schemes solidifies notions that have been swirling around the literature for years, and promises a more modular approach to designing and using garbling schemes in the future.

A non-interactive zero-knowledge argument enables a prover to convince a verifier that a statement is true without revealing any other private information. We consider succinct arguments that are smaller than the size of the statement. Succinct arguments are known in the random oracle model. The goal of this talk is to present alternative pairing-based methods that can be used instead of the random oracle model relying on different and perhaps more plausible cryptographic assumptions.

We introduce a new characterization of the NP complexity class, called "Quadratic Span Programs" (QSPs), which is a natural extension of "span programs" by Karchmer and Wigderson. Our main motivation is the construction of succinct arguments of NP-statements that are quickly constructible and verifiable. QSPs seem well-suited for this task, perhaps even better than Probabilistically Checkable Proofs (PCPs). In 2010, Groth constructed a NIZK argument in the common reference string (CRS) model for Circuit-SAT consisting of only 42 elements in a bilinear group. Interestingly, his argument does not (explicitly) use PCPs. But his scheme has some disadvantages -- namely, the CRS size and prover computation are both quadratic in the circuit size. In 2011, Lipmaa reduced the CRS size to quasi-linear, but with prover computation still quadratic. Using QSPs we construct a NIZK argument in the CRS model for Circuit-SAT consisting of just 7 group elements. The CRS size is linear in the circuit size, and prover computation is quasi-linear, making our scheme seemingly quite practical. (The prover only needs to do a linear number of group operations; the quasi-linear computation is a multipoint evaluation.) Our results are complementary to those of Valiant (TCC 2008) and Bitansky et al. (2012), who use ``bootstrapping" (recursive composition) of arguments to reduce CRS size and prover and verifier computation. QSPs also provide a crisp mathematical abstraction of some of the techniques underlying Groth's and Lipmaa's constructions. Joint work with Rosario Gennaro, Bryan Parno, and Mariana Raykova.

We discuss the recent simulation-based definitions of security for functional and predicate encryption and give some further results.

In 2008, Groth and Sahai proposed a powerful suite of techniques for constructing non-interactive zero-knowledge proofs in bilinear groups. Their proof systems have found numerous applications, including group signature schemes, anonymous voting, and anonymous credentials. In this talk, we demonstrate that the notion of smooth projective hash functions is an efficient alternative for interactive protocols. We show that this approach provides suitable proofs for designing schemes that rely on standard security assumptions in the standard model with a common-reference string and are more efficient than those obtained using the Groth-Sahai methodology when interactions are already required by the primitive itself. As an illustration of our design principle, we describe efficient blind signature schemes, as well as an oblivious signature-based envelope scheme, but also the new notion of Language-based Authenticated Key Exchange, that includes Password-based Authenticated Key Exchange, Secret Handshakes and Credential Authenticated Key Exchange. This is a joint work with Olivier Blazy, Céline Chevalier and Damien Vergnaud.

We show a curious connection between the problem of *computation delegation* and the model of *no-signalling multi-prover interactive proofs*, a model that was studied in the context of multi-prover interactive proofs with provers that share quantum entanglement, and is motivated by the physical law that information cannot travel instantly (and is, like matter, limited by the speed of light).

We consider the method suggested by Aiello et. al. for converting a 1-round multi-prover interactive proof (MIP) into a 1-round delegation scheme, by using a computational private information retrieval (PIR) scheme. On one direction, we show that if the underlying MIP protocol is sound against statistically no-signalling cheating provers then the resulting delegation protocol is secure (under the assumption that the underlying PIR is secure for attackers of sub-exponential size). On the other direction, we show that if the resulting delegation protocol is secure for every PIR scheme, and the proof of security is a black-box reduction that reduces the security of the protocol to the security of any ``standard'' cryptographic assumption, and such that the number of calls made by the reduction to the cheating prover is independent of the security parameter, then the underlying MIP protocol is sound against statistically no-signalling cheating provers.

This is joint work with Ran Raz and Ron Rothblum.

We describe a new type of probabilistic search algorithm: a randomized algorithm which is guaranteed to run in expected polynomial time, and with high probability produce correct and unique solution. These algorithms are pseudo-deterministic: they can not be distinguished from deterministic algorithms in polynomial time by a probabilistic polynomial time observer with black box access. We will exhibit a necessary and sufficient condition for the existence of a pseudo-deterministic algorithm for an NP relation R. Several examples of such algorithms, for problems in number theory, algebra and graph theory which improve on deterministic solutions, will also be discussed. We note that the characterization scales up. The notion of pseudo-deterministic computations is interesting beyond just sequential polynomial time algorithms, in other domains where the use of randomization is essential. For example, one can define and obtain pseudo-deterministic fault tolerance distributed algorithms and pseudo deterministic sub-linear algorithms for tasks which are impossible to solve without randomization. We will discuss several such domains.

We show that for any joint distribution $(X,A)$ and any family $F$ of distinguishers, e.g. polynomial size circuits, there exists an efficient (deterministic) simulator $h$ such that $F$ cannot distinguish $(X,A)$ from $(X,h(X))$, i.e. for all $f$ in $F$ we have $\bigl| E[f(X,A)]-E(f(X,h(X))] \bigr| <eps$. Efficient means exponential in the length of $A$ and polynomial in $1/eps$. Several known results, including a strong version of the dense model theorem, follow as simple corollaries. The main motivation for this work is to simplify leakage-resilience proofs which currently use the dense model theorem.

Joint work with Karthik Bhargavan, Markulf Kohlweiss, Alfredo Pironti, and Pierre-Yves Strub.

We develop a reference implementation of the TLS 1.2 Internet Standard. Our code fully supports binary wire formats, multiple ciphersuites, sessions and connections with re-handshakes and resumptions, alerts, message fragmentation, ... as prescribed by the standard; it interoperates with other implementations, notably existing web browsers and servers. At the same time, our code is carefully structured to enable its automated, modular verification, from its main API down to computational security assumptions on its underlying cryptographic algorithms.

In the talk, I will review our modular cryptographic verification method, which is based on F7, a refinement type checker coupled with an SMT-solver, with a theory formalized in Coq. Using F7, we verify constructions and protocols coded in F# by typing them against new cryptographic interfaces that capture their authenticity and secrecy properties. We relate their ideal functionalities and concrete implementations, using game-based program transformations behind typed interfaces, so that we can easily compose them.

I will also outline our TLS implementations, coded in F# and specified in F7. I will present its main typed interfaces, which can be read as specifications of "giant" ideal functionalities for its main components, such as authenticated encryption for the record layer and key establishment for the handshake. I will finally describe our main security results, as well as some new attacks we found in the process.