skip to content

Formal and Computational Cryptographic Proofs


we have been made aware of a very convincing phone scam that is focusing on our workshop participants. Participants may be contacted by phone by a firm called Business Travel Management to arrange accommodation for workshops and/or programmes.  This includes a request to enter credit card information.

Please note, INI will never contact you over the phone requesting card details. We take all payments via the University of Cambridge Online store

If you have been contacted by this company please contact us as soon as possible.

10th April 2012 to 13th April 2012

Organisers: Nigel Smart (Bristol) and Shafi Goldwasser (MIT)

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.

Alan Turing Year logo












University of Cambridge Research Councils UK
    Clay Mathematics Institute London Mathematical Society NM Rothschild and Sons