Skip to content

Workshop Programme

for period 10 - 13 April 2012

Formal and Computational Cryptographic Proofs

10 - 13 April 2012

Timetable

Tuesday 10 April
09:00-09:55 Registration
09:55-10:00 Welcome from Christie Marr (INI Deputy Director) & Annoucements
10:00-11:00 Gordon, A (Microsoft Research)
  Verifying Crypto Protocols Written in C Sem 1
 

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 verification-condition 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 two-message protocol.

 
11:00-11:30 Morning Coffee
11:30-12:30 Vaikuntanathan, V (Toronto)
  Multi-key Homomorphic Encryption and Applications Sem 1
 

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).

 
12:30-13:30 Lunch at Wolfson Court
13:30-14:30 Warinschi, B (Bristol)
  Compositionality of game-based secure key-exchange Sem 1
 

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 game-based security security and avoids the idiosyncrasies of simulation-based definitions. As an application, I will discuss how the results can be applied to proving the security of the Transport Layer Security protocol.

 
14:30-15:30 Micali, S (MIT)
  Rational Proofs Sem 1
 

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.

 
15:30-16:00 Afternoon Tea
16:00-17:00 Maurer, U (ETH Zürich)
  Constructive cryptography Sem 1
 

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.

 
17:00-18:00 Welcome Drinks Reception
Wednesday 11 April
09:00-10:00 Rogaway, P (UC, Davis)
  Foundations of Garbled Circuits Sem 1
 

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.

 
10:00-11:00 Fischlin, M (TU, Darmstadt)
  Meta-Reductions Sem 1
 

Meta-Reductions are a technique to show impossiblity results in reductionist cryptography. Roughly, such a meta-reduction 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 meta-reduction 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, meta-reductions usually work for all reductions R which treat the adversary as a black-box, but often do not impose any restriction on the primitives in question, i.e., the primitive may not be treated as a black-box, and the technique may thus apply to common primitives like RSA or DL. In return, all known meta-reductions work for specific primitives only. In this talk we survey the recent result on meta-reductions and shed light on the applicability of this technique.

 
11:00-11:30 Morning Coffee
11:30-12:30 Groth, J (UCL)
  Pairing-based succinct non-interactive zero-knowledge arguments Sem 1
 

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.

 
12:30-13:30 Lunch at Wolfson Court
13:30-14:30 Blanchet, B (ENS)
  From crypto verif specifications to computationally secure implementations of protocols Sem 1
 

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.

 
14:30-15:30 Gentry, C (IBM Research)
  Quadratic Span Programs for Succinct NIZKs without PCPs Sem 1
 

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.

 
15:30-16:00 Afternoon Tea
16:00-17:00 Rothblum, G (Microsoft Research)
  How to Compute in the Presence of Leakage Sem 1
 

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 side-channel attacks, as well as for running non-cryptographic 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 length-bounded 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.

 
Thursday 12 April
09:00-10:00 Persiano, P (Salerno)
  Definitions of Predicate Encryption Sem 1
 

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

 
10:00-11:00 Kiltz, E (Ruhr-Universität Bochum)
  How provably secure are cryptographic primitives used in practice Sem 1
 

We will discuss how 'provably secure' are several cryptographic primitives of practical relevance. Examples include OAEP encryption and Full Domain Hash Signatures.

 
11:00-11:30 Morning Coffee
11:30-12:30 Pointcheval, D (ENS - Paris)
  Efficient Smooth Projective Hash Functions and Applications Sem 1
 

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.

 
12:30-13:30 Lunch at Wolfson Court
13:30-14:30 Sahai, A (UCLA)
  Leakage-Resilient Zero-Knowledge Proofs and their Applications Sem 1
 

We initiate a study of zero knowledge proof systems in the presence of side-channel 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 leakage-resilient zero knowledge (LR-ZK) 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 LR-ZK 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 leakage-resilient primitives such as encryption, or leakage-resilient devices, or leakage prior to the protocol execution). Next, we give an LR-NIZK argument system based on standard assumptions. We will also discuss several applications of our new notion. Joint work with Sanjam Garg and Abhishek Jain.

 
14:30-15:30 Tauman Kalai, Y
  Where Delegation Meets Einstein Sem 1
 

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.

 
15:30-16:00 Afternoon Tea
16:00-17:00 Tessaro, S (Massachusetts Institute of Technology)
  Semantic security for the wiretap channel Sem 1
 

The wiretap channel is a setting where one aims to provide information-theoretic 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).

 
17:00-18:00 Goldwasser, S (MIT)
  Rothschild Lecture: Pseudo Deterministic Algorithms and Applications to Cryptography Sem 1
 

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.

 
19:30-22:00 Conference Dinner at Gonville and Caius College
Friday 13 April
09:00-10:00 Naor, M (Weizmann Institute of Science)
  The Privacy of the Analyst and The Power of the State Sem 1
 

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 non-trivial 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.

 
10:00-11:00 Pietrzak, C (IST Austria)
  How to fake auxiliary input Sem 1
 

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.

 
11:00-11:30 Morning Coffee
11:30-12:30 Barak, B (Microsoft Research New England)
  Zero Knowledge Proofs and Nuclear Disarmament Sem 1
 

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 about-to-be-dismantled 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.

 
12:30-13:30 Lunch at Wolfson Court
13:30-14:30 Fournet, C (Microsoft Research)
  Cryptographically verified implementation of TLS 1.2 Sem 1
 

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.

 
14:30-15:30 Dodis, Y (New York)
  Overcoming Weak Expectations Sem 1
 

Recently, there has been renewed interest in basing cryptographic primitives on weak secrets, where the only information about the secret is some non-trivial 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 non-malleable extractors, leakage-resilient symmetric encryption, seed-dependent condensers and improved entropy loss for the leftover hash lemma.

 
15:30-16:00 Afternoon Tea
16:00-17:00 Barthe, G (Madrid Institute of Advanced Studies (IMDEA))
  Computer-aided security proofs Sem 1
 

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, zero-knowledge protocols and hash functions. I will present recent developments in the tool and survey new applications.

 

Back to top ∧