Formal and computational cryptographic proofs
SASW02
10 April 2012 to 13 April 2012
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.
Applications for this workshop are now closed
The Institute kindly requests that any papers published as a result of this programme’s activities are credited as such. Please acknowledge the support of the Institute in your paper using the following text:
The author(s) would like to thank the Isaac Newton Institute for Mathematical Sciences, Cambridge, for support and hospitality during the programme Formal and computational cryptographic proofs, where work on this paper was undertaken. This work was supported by EPSRC grant EP/F005431/1 and EP/I016392/1.
Timetable
| Tuesday 10th April 2012 | |||
|---|---|---|---|
| 09:00 to 09:55 | 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) |
Room 1 | 
|
| 11:00 to 11:30 | No Room Required | ||
| 11:30 to 12:30 |
Vinod Vaikuntanathan University of Toronto |
Room 1 |
|
| 12:30 to 13:30 | No Room Required | ||
| 13:30 to 14:30 |
Bogdan Warinschi University of Bristol |
Room 1 |
|
| 14:30 to 15:30 |
Silvio Micali Massachusetts Institute of Technology |
Room 1 |
|
| 15:30 to 16:00 | No Room Required | ||
| 16:00 to 17:00 |
Ueli Maurer ETH Zürich |
Room 1 |
|
| 17:00 to 18:00 | No Room Required | ||
| Wednesday 11th April 2012 | |||
|---|---|---|---|
| 09:00 to 10:00 |
Phillip Rogaway University of California, Davis |
Room 1 |
|
| 10:00 to 11:00 |
Marc Fischlin Technische Universität Darmstadt |
Room 1 |
|
| 11:00 to 11:30 | No Room Required | ||
| 11:30 to 12:30 |
Jens Groth University College London |
Room 1 |
|
| 12:30 to 13:30 | No Room Required | ||
| 13:30 to 14:30 |
Bruno Blanchet CNRS - Ecole Normale Superieure Paris |
Room 1 |
|
| 14:30 to 15:30 |
Craig Gentry IBM Thomas J. Watson Research Center New York |
Room 1 |
|
| 15:30 to 16:00 | No Room Required | ||
| 16:00 to 17:00 | Room 1 |
|
|
| Thursday 12th April 2012 | |||
|---|---|---|---|
| 09:00 to 10:00 |
Giuseppe Persiano Università degli Studi di Salerno |
Room 1 |
|
| 10:00 to 11:00 |
Eike Kiltz Ruhr-Universität Bochum |
Room 1 |
|
| 11:00 to 11:30 | No Room Required | ||
| 11:30 to 12:30 |
David Pointcheval ENS - Paris |
Room 1 |
|
| 12:30 to 13:30 | No Room Required | ||
| 13:30 to 14:30 |
Amit Sahai University of California, Los Angeles |
Room 1 |
|
| 14:30 to 15:30 | Room 1 |
|
|
| 15:30 to 16:00 | No Room Required | ||
| 16:00 to 17:00 |
Stefano Tessaro University of California, Santa Barbara |
Room 1 |
|
| 17:00 to 18:00 |
Shafi Goldwasser Massachusetts Institute of Technology |
Room 1 | |
| 19:30 to 22:00 | No Room Required | ||
| Friday 13th April 2012 | |||
|---|---|---|---|
| 09:00 to 10:00 |
Moni Naor Weizmann Institute of Science |
Room 1 |
|
| 10:00 to 11:00 |
Krzysztof Pietrzak Institute of Science and Technology (IST Austria) |
Room 1 |
|
| 11:00 to 11:30 | No Room Required | ||
| 11:30 to 12:30 |
Boaz Barak Harvard University |
Room 1 |
|
| 12:30 to 13:30 | No Room Required | ||
| 13:30 to 14:30 |
Cédric Fournet Microsoft (UK) |
Room 1 |
|
| 14:30 to 15:30 |
Yevgeniy Dodis New York University |
Room 1 |
|
| 15:30 to 16:00 | No Room Required | ||
| 16:00 to 17:00 |
Gilles Barthe Madrid Institute of Advanced Studies (IMDEA); Max Planck Institute for Astronomy, Heidelberg |
Room 1 |
|
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
Supported By
