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.