Crypto Forma Event -- Jan 29th / 30th -- Tentative Schedule

We are very excited to be hosting the CryptoForma event, bringing together UK researchers on cryptography and formal methods for two days. We attach the tentative schedule to give everyone an idea of the sessions and their content. If you are not able to present at the allocated time, please get in touch with us as soon as possible.

The event will include a rump session devoted to short (5 min) talks on current work. You can reserve a slot on the day. Regular talks are allocated 30 minutes, but we encourage short presentations and a high level of interaction with participants.

Travel and local accommodation information is available at:
http://research.microsoft.com/aboutmsr/visitmsr/cambridge/default.aspx

Thursday 29 January 2009

09:00 -- 10:00

Morning Coffee and Registration

10:00 -- 12:00

• Introductions & welcome note
• Dan Grundy (Kent)
  "Calculational proofs for one-way functions"
• Misha Aizatulin (OU)
  "Balanced Contract Signing"
• James Heather (Surrey)
  "Re-encryption in a symmetric setting"
• Eerke Boiten (Kent)
  "The bottom-up formal methods perspective"

Lunch

14:00 -- 15:00

• MSR Talk: Ross Smith (MS)
  "Dude, where’s my boss? Using Serious Games to improve software development productivity"

15:00 -- 16:00

• Mark Ryan (Birmingham)
  "TPM Protocols and their Verification"
• Jan Juerjens (MSRC/OU)
  "Modularity and refinement in the verification of crypto-protocols"

Afternoon coffee

16:30 -- 17:30 Rump Session
Short (5 min) presentations of work-in-progress.

19:30 -- Reception followed by dinner at King's College

Friday 30 January 2009

09:00 -- 10:30

• Aybek Mukhamedov (Birmingham)
  "Formal analysis of the Trusted Platform Module"
• Alfredo Pironti (Torino)
  "Towards provably correct black-box monitoring of security protocols"
• Cédric Fournet (MSRC)
  "A Cryptographic Compiler for Information-Flow Security"

Morning coffee

11:00 -- 12:00

• Kenny Paterson (RHUL)
  "Limitations of provable security with respect to crypto specifications and implementations"
• Karthik Bhargavan (MSRC)
  "Computational Verification of TLS Implementations"

Lunch

14:00 -- 15:30

• Liqun Chen (HP)
  "Parsing ambiguities in authentication and key establishment protocols"
• Tom Chothia (Birmingham)
  "Measuring Information Leakage Using Network Information Theory"
• Bogdan Warinschi (Bristol)
  "A compositional soundness result"