10 - 13 April 2012
Organisers: Nigel Smart (Bristol) and Shafi Goldwasser (MIT)
in association with the Newton Institute programme Semantics and Syntax: A Legacy of Alan Turing
(9 January - 6 July 2012)
Proofs arise in many forms in cryptography and security;
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.
Speakers will include: