Formal and computational cryptographic proofs

Workshop theme

Proofs arise in many forms in cryptography and security;

As mathematical proofs of security in a complexity theoretic model of a protocol or scheme; such proofs are typical of the area known as "reductionist proofs of security".
As mathematical proofs of security in a logical, or symbolic, model of a protocol or scheme; such proofs are typified by work in the "formal methods"/"symbolic" tradition, a.k.a. the Dolev-Yao model.
As objects in their own right which are used in a protocol; for example as in zero-knowledge interactive proofs or probabilistically checkable proofs.

The workshop is timely given recent work in establishing that some Dolev-Yao style proofs can have the same computational guarantees as provided by reductionist proofs of security. Such meta-proofs, show that Dolev-Yao proofs are computationally sound. In addition recent years have shown the development of automated theorem provers, traditionally the reserve of formal methods style proofs, into the arena of provable security. In addition, we have seen the actual deployment of protocols based on zero-knowledge proofs via protocols such as U-Prove (from Microsoft) and Idemix (from IBM). Finally, the last ten years have seen the application of ideas from complexity theory, such as the PCP theorem, to cryptographic protocols, and it is to be hoped that such protocols may soon become practical.

The aim of the workshop on "Formal and Computational Cryptographic Proofs" is to bring together people working on all such topics, with a view for cross disciplinary work, to obtain new insights on old problems, and to capitalise on the recent advances alluded to above.

The application is closed

Timetable

Tuesday 10th April 2012
09:00 to 09:55	Registration	No Room Required
09:55 to 10:00	Welcome from Christie Marr (INI Deputy Director) & Annoucements	Room 1
10:00 to 11:00	Andy Gordon Microsoft (UK) Verifying Crypto Protocols Written in C	Room 1
11:00 to 11:30	Morning Coffee	No Room Required
11:30 to 12:30	Vinod Vaikuntanathan University of Toronto Multi-key Homomorphic Encryption and Applications	Room 1
12:30 to 13:30	Lunch at Wolfson Court	No Room Required
13:30 to 14:30	Bogdan Warinschi University of Bristol Compositionality of game-based secure key-exchange	Room 1
14:30 to 15:30	Silvio Micali Massachusetts Institute of Technology Rational Proofs	Room 1
15:30 to 16:00	Afternoon Tea	No Room Required
16:00 to 17:00	Ueli Maurer ETH Zürich Constructive cryptography	Room 1
17:00 to 18:00	Welcome Drinks Reception	No Room Required

Wednesday 11th April 2012
09:00 to 10:00	Phillip Rogaway University of California, Davis Foundations of Garbled Circuits	Room 1
10:00 to 11:00	Marc Fischlin Technische Universität Darmstadt Meta-Reductions	Room 1
11:00 to 11:30	Morning Coffee	No Room Required
11:30 to 12:30	Jens Groth University College London Pairing-based succinct non-interactive zero-knowledge arguments	Room 1
12:30 to 13:30	Lunch at Wolfson Court	No Room Required
13:30 to 14:30	Bruno Blanchet CNRS - Ecole Normale Superieure Paris From crypto verif specifications to computationally secure implementations of protocols	Room 1
14:30 to 15:30	Craig Gentry IBM Thomas J. Watson Research Center New York Quadratic Span Programs for Succinct NIZKs without PCPs	Room 1
15:30 to 16:00	Afternoon Tea	No Room Required
16:00 to 17:00	How to Compute in the Presence of Leakage	Room 1

Thursday 12th April 2012
09:00 to 10:00	Giuseppe Persiano Università degli Studi di Salerno Definitions of Predicate Encryption	Room 1
10:00 to 11:00	Eike Kiltz Ruhr-Universität Bochum How provably secure are cryptographic primitives used in practice	Room 1
11:00 to 11:30	Morning Coffee	No Room Required
11:30 to 12:30	David Pointcheval ENS - Paris Efficient Smooth Projective Hash Functions and Applications	Room 1
12:30 to 13:30	Lunch at Wolfson Court	No Room Required
13:30 to 14:30	Amit Sahai University of California, Los Angeles Leakage-Resilient Zero-Knowledge Proofs and their Applications	Room 1
14:30 to 15:30	Where Delegation Meets Einstein	Room 1
15:30 to 16:00	Afternoon Tea	No Room Required
16:00 to 17:00	Stefano Tessaro University of California, Santa Barbara Semantic security for the wiretap channel	Room 1
17:00 to 18:00	Shafi Goldwasser Massachusetts Institute of Technology Rothschild Lecture: Pseudo Deterministic Algorithms and Applications to Cryptography	Room 1
19:30 to 22:00	Conference Dinner at Gonville and Caius College	No Room Required

Friday 13th April 2012
09:00 to 10:00	Moni Naor Weizmann Institute of Science The Privacy of the Analyst and The Power of the State	Room 1
10:00 to 11:00	Krzysztof Pietrzak Institute of Science and Technology (IST Austria) How to fake auxiliary input	Room 1
11:00 to 11:30	Morning Coffee	No Room Required
11:30 to 12:30	Boaz Barak Harvard University Zero Knowledge Proofs and Nuclear Disarmament	Room 1
12:30 to 13:30	Lunch at Wolfson Court	No Room Required
13:30 to 14:30	Cédric Fournet Microsoft (UK) Cryptographically verified implementation of TLS 1.2	Room 1
14:30 to 15:30	Yevgeniy Dodis New York University Overcoming Weak Expectations	Room 1
15:30 to 16:00	Afternoon Tea	No Room Required
16:00 to 17:00	Gilles Barthe Madrid Institute of Advanced Studies (IMDEA); Max Planck Institute for Astronomy, Heidelberg Computer-aided security proofs	Room 1

Formal and computational cryptographic proofs

Speakers

Boaz Barak Harvard University
Gilles Barthe Madrid Institute of Advanced Studies (IMDEA); Max Planck Institute for Astronomy, Heidelberg
Bruno Blanchet CNRS - Ecole Normale Superieure Paris
Yevgeniy Dodis New York University
Marc Fischlin Technische Universität Darmstadt
Cédric Fournet Microsoft (UK)
Craig Gentry IBM Thomas J. Watson Research Center New York
Shafi Goldwasser Massachusetts Institute of Technology
Andy Gordon Microsoft (UK)
Jens Groth University College London
Eike Kiltz Ruhr-Universität Bochum
Ueli Maurer ETH Zürich
Silvio Micali Massachusetts Institute of Technology
Moni Naor Weizmann Institute of Science
Giuseppe Persiano Università degli Studi di Salerno
Krzysztof Pietrzak Institute of Science and Technology (IST Austria)
David Pointcheval ENS - Paris
Phillip Rogaway University of California, Davis
Amit Sahai University of California, Los Angeles
Stefano Tessaro University of California, Santa Barbara
Vinod Vaikuntanathan University of Toronto
Bogdan Warinschi University of Bristol

Show All

Formal and computational cryptographic proofs

Workshop theme

The application is closed

Timetable

Speakers

Supported By

Register for updates