Formal and Computational Cryptographic Proofs
Tuesday 10th April 2012 to Friday 13th April 2012
09:00 to 09:55  Registration  
09:55 to 10:00  Welcome from Christie Marr (INI Deputy Director) & Annoucements  INI 1  
10:00 to 11:00 
Verifying Crypto Protocols Written in C
The security of much critical infrastructure depends in part on cryptographic software coded in C, and yet vulnerabilities continue to be discovered in such software. We describe recent progress on checking the security of C code implementing cryptographic software. In particular, we describe projects that combine verificationcondition generation and symbolic execution techniques for C, with methods for stating and verifying security properties of abstract models of cryptographic protocols. We illustrate these techniques on C code for a simple twomessage protocol.

INI 1  
11:00 to 11:30  Morning Coffee  
11:30 to 12:30 
Multikey Homomorphic Encryption and Applications
I will present a new notion of fully homomorphic encryption (FHE) called multikey FHE that permits computation on data encrypted under multiple unrelated keys, a new construction of multikey FHE based on the NTRU encryption scheme, and a new application of multikey FHE to the problem of constructing minimally interactive cloudassisted secure multiparty computation protocols. Joint Work with Adriana LopezAlt (NYU) and Eran Tromer (TelAviv U).

INI 1  
12:30 to 13:30  Lunch at Wolfson Court  
13:30 to 14:30 
Compositionality of gamebased secure keyexchange
In this talk I will present two approaches towards modular security proofs for the composition of key exchange protocols with arbitrary other cryptographic tasks. While the two approaches differ in their scope and applicability they both rely on gamebased security security and avoids the idiosyncrasies of simulationbased definitions. As an application, I will discuss how the results can be applied to proving the security of the Transport Layer Security protocol.

INI 1  
14:30 to 15:30 
Rational Proofs
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.

INI 1  
15:30 to 16:00  Afternoon Tea  
16:00 to 17:00 
Constructive cryptography
I will present constructive cryptography, a new paradigm for defining and proving security of cryptographic protocols. Constructive cryptography differs from previous approaches both in terms of the types of statements made as well as in terms of the abstraction level at which they are proved.

INI 1  
17:00 to 18:00  Welcome Drinks Reception 
09:00 to 10:00 
P Rogaway ([UC, Davis]) Foundations of Garbled Circuits
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 twoparty 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 blockcipherbased 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.

INI 1  
10:00 to 11:00 
M Fischlin ([TU, Darmstadt]) MetaReductions
MetaReductions are a technique to show impossiblity results in reductionist cryptography. Roughly, such a metareduction M shows that there cannot exist a reduction R which turns a successful adversary against one cryptographic primitive into a successful adversary against another, hard primitive. This is shown by turning the reduction R through the metareduction M (a 'reduction against the reduction') into an algorithm solving the underlying primitive directly, without relying on the assumption of a successful adversary. Hence, either the reduction R cannot exist (if the primitive is really hard), or it is trivial (if the primitive is already easy). Unlike other separation techniques, metareductions usually work for all reductions R which treat the adversary as a blackbox, but often do not impose any restriction on the primitives in question, i.e., the primitive may not be treated as a blackbox, and the technique may thus apply to common primitives like RSA or DL. In return, all known metareductions work for specific primitives only. In this talk we survey the recent result on metareductions and shed light on the applicability of this technique.

INI 1  
11:00 to 11:30  Morning Coffee  
11:30 to 12:30 
Pairingbased succinct noninteractive zeroknowledge arguments
A noninteractive zeroknowledge 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 pairingbased methods that can be used instead of the random oracle model relying on different and perhaps more plausible cryptographic assumptions.

INI 1  
12:30 to 13:30  Lunch at Wolfson Court  
13:30 to 14:30 
From crypto verif specifications to computationally secure implementations of protocols
CryptoVerif is a protocol verifier in the computational model, which generates proofs by sequences of games, like those written manually by cryptographers. We have implemented a compiler that automatically translates CryptoVerif specifications into implementations of protocols, in the OCaml language. The goal of this compiler is to generate implementations of security protocols proved secure in the computational model: from the same specification, we can prove it using CryptoVerif and generate the implementation using our compiler. We are currently using this framework in order to generate an implementation of SSH.

INI 1  
14:30 to 15:30 
C Gentry (IBM Research) Quadratic Span Programs for Succinct NIZKs without PCPs
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 NPstatements that are quickly constructible and verifiable. QSPs seem wellsuited 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 CircuitSAT 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 quasilinear, but with prover computation still quadratic.
Using QSPs we construct a NIZK argument in the CRS model for CircuitSAT consisting of just 7 group elements. The CRS size is linear in the circuit size, and prover computation is quasilinear, making our scheme seemingly quite practical. (The prover only needs to do a linear number of group operations; the quasilinear 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.

INI 1  
15:30 to 16:00  Afternoon Tea  
16:00 to 17:00 
How to Compute in the Presence of Leakage
We address the following problem: how to execute any algorithm, for an unbounded number of executions, in the presence of an attacker who gets to observe partial information on the internal state of the computation during executions.
This general problem has beenaddressed in the last few years with varying degrees of success. It is important for running cryptographic algorithms in the presence of sidechannel attacks, as well as for running noncryptographic algorithms, such as a proprietary search algorithm or a game, on a cloud server where parts of the execution's internals might be observed.
In this work, we view algorithms as running on a leaky CPU. In each (sub)computation run on the CPU, we allow the adversary to observe the output of an arbitrary and adaptively chosen lengthbounded function on the CPU's input, output, and randomness.
Our main result is a general compiler for transforming any algorithm into one that is secure in the presence of this family of partial observation attacks (while maintaining the algorithm's functionality). This result is unconditional, it does not rely on any secure hardware components or cryptographic assumptions.

INI 1 
09:00 to 10:00 
Definitions of Predicate Encryption
We discuss the recent simulationbased definitions of security for functional and predicate encryption and give some further results.

INI 1  
10:00 to 11:00 
How provably secure are cryptographic primitives used in practice
We will discuss how 'provably secure' are several cryptographic primitives of practical relevance. Examples include OAEP encryption and Full Domain Hash Signatures.

INI 1  
11:00 to 11:30  Morning Coffee  
11:30 to 12:30 
D Pointcheval (ENS  Paris) Efficient Smooth Projective Hash Functions and Applications
In 2008, Groth and Sahai proposed a powerful suite of techniques for constructing noninteractive zeroknowledge 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 commonreference string and are more efficient than those obtained using the GrothSahai 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 signaturebased envelope scheme, but also the new notion of Languagebased Authenticated Key Exchange, that includes Passwordbased Authenticated Key Exchange, Secret Handshakes and Credential Authenticated Key Exchange.
This is a joint work with Olivier Blazy, Céline Chevalier and Damien Vergnaud.

INI 1  
12:30 to 13:30  Lunch at Wolfson Court  
13:30 to 14:30 
LeakageResilient ZeroKnowledge Proofs and their Applications
We initiate a study of zero knowledge proof systems in the presence of sidechannel attacks. Specifically, we consider a setting where a cheating verifier is allowed to obtain arbitrary bounded leakage on the entire state (including the witness and the random coins) of the prover during the entire protocol execution. We formalize a meaningful definition of leakageresilient zero knowledge (LRZK) proof system, that intuitively guarantees that "the protocol does not yield anything beyond the validity of the statement, and whatever leakage the attacker could have obtained without the protocol ever taking place."
We give a construction of LRZK interactive proof system based on general assumptions. To the best of our knowledge, this is the first instance of a cryptographic protocol where the adversary is allowed to perform leakage attacks during the protocol execution (in contrast, prior work only focused on leakageresilient primitives such as encryption, or leakageresilient devices, or leakage prior to the protocol execution). Next, we give an LRNIZK argument system based on standard assumptions.
We will also discuss several applications of our new notion.
Joint work with Sanjam Garg and Abhishek Jain.

INI 1  
14:30 to 15:30 
Where Delegation Meets Einstein
We show a curious connection between the problem of *computation
delegation* and the model of *nosignalling multiprover interactive proofs*, a model that was studied in the context of multiprover 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 1round multiprover interactive proof (MIP) into a 1round 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 nosignalling cheating provers then the resulting delegation protocol is secure (under the assumption that the underlying PIR is secure for attackers of subexponential 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 blackbox 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 nosignalling cheating provers. This is joint work with Ran Raz and Ron Rothblum. 
INI 1  
15:30 to 16:00  Afternoon Tea  
16:00 to 17:00 
Semantic security for the wiretap channel
The wiretap channel is a setting where one aims to provide informationtheoretic privacy of communicated data based solely on the assumption that the channel from sender to adversary is “noisier” than the channel from sender to receiver. The central quest in this area has been secure schemes of optimal rate but decades of work have provided only non constructive proofs of existence of such schemes for a notion of security that from the cryptographic perspective is weak. We define and prove equivalent two strong security metrics, one based on semantic security and the other on entropy. We then provide a new scheme that achieves these strong security goals in polynomial time with optimal rate, thereby not only solving the central open problem in this area but delivering even more in terms of security.
This is joint work with Mihir Bellare and Alexander Vardy (UCSD).

INI 1  
17:00 to 18:00 
Rothschild Lecture: Pseudo Deterministic Algorithms and Applications to Cryptography
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 pseudodeterministic: 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
pseudodeterministic 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 pseudodeterministic
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 pseudodeterministic
fault tolerance distributed algorithms and pseudo deterministic sublinear
algorithms for tasks which are impossible
to solve without randomization. We will discuss several such domains.

INI 1  
19:30 to 22:00  Conference Dinner at Gonville and Caius College 
09:00 to 10:00 
M Naor (Weizmann Institute of Science) The Privacy of the Analyst and The Power of the State
Differential privacy is a paradigm in privacy that is aimed at mitigating the drawbacks of traditional anonymization techniques, as it provides a rigorous guarantee for the added risk to an individual in participating in a database. Roughly speaking, a mechanism satisfies differential privacy if for any possible output of the mechanism and any possible set of data on individuals, the probability of obtaining this particular output changes only very little with the addition or deletion of the data on an individual.
We initiate the study of privacy for the analyst in differentially private data analysis. That is, not only are we concerned with ensuring differential privacy for the data (i.e. individuals or customers), which are the usual concern of differential privacy, but we also consider (differential) privacy for the set of queries posed by each data analyst. The privacy achieved is with respect to other analysts which are the users of the system. This problem of analysts' queries being leaked arises only in the context of stateful privacy mechanisms, in which the responses to queries depend on other queries posed. A recent wave of results in the area of differential privacy utilized coordinated noise and state in order to allow answering hugely many queries. We argue the problem is real by proving an exponential gap between the number of queries that can be answered (with nontrivial error) by stateless and stateful differentially private mechanisms. We then give a stateful algorithm for differentially private data analysis that also ensures differential privacy for the analyst and can answer exponentially many queries. Joint work with Cynthia Dwork and Salil Vadhan. 
INI 1  
10:00 to 11:00 
How to fake auxiliary input
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 leakageresilience proofs which currently use the dense model theorem.

INI 1  
11:00 to 11:30  Morning Coffee  
11:30 to 12:30 
B Barak ([Microsoft Research New England]) Zero Knowledge Proofs and Nuclear Disarmament
I'll describe a physical implementation of zero knowledge proofs whose goal is to verify that two physical objects are identical, without revealing any information about them. Our motivation is the task of verifying that an abouttobedismantled nuclear warhead is authentic without revealing its classified design. This is one of the technical hurdles that arises in implementing nuclear disarmament. Joint work with Alex Glaser and Robert Goldston from Princeton University and the Princeton Plasma Physics Laboratory.

INI 1  
12:30 to 13:30  Lunch at Wolfson Court  
13:30 to 14:30 
C Fournet (Microsoft Research) Cryptographically verified implementation of TLS 1.2
Joint work with Karthik Bhargavan, Markulf Kohlweiss, Alfredo Pironti, and PierreYves 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 rehandshakes 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 SMTsolver, 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 gamebased 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. 
INI 1  
14:30 to 15:30 
Y Dodis ([New York]) Overcoming Weak Expectations
Recently, there has been renewed interest in basing cryptographic primitives on weak secrets, where the only information about the secret is some nontrivial amount of (min)entropy. From a formal point of view, such results require to upper bound the expectation of some function f(X), where X is a weak source in question. We show an elementary inequality which essentially upper bounds such 'weak expectation' by two terms, the first of which is *independent* of f, while the second only depends on the 'variance' of f under *uniform* distribution. Quite remarkably, as relatively simple corollaries of this elementary inequality, we obtain some 'unexpected' results, in several cases noticeably simplifying/improving prior techniques for the same problem. Examples include nonmalleable extractors, leakageresilient symmetric encryption, seeddependent condensers and improved entropy loss for the leftover hash lemma.

INI 1  
15:30 to 16:00  Afternoon Tea  
16:00 to 17:00 
Computeraided security proofs
CertiCrypt is a toolset that assists the construction and verification of cryptographic proofs; it supports common patterns of reasoning in cryptography, and has been used successfully to prove the security of many examples, including encryption schemes, signature schemes, zeroknowledge protocols and hash functions. I will present recent developments in the tool and survey new applications.

INI 1 