Eighth Workshop on
Formal and Computational Cryptography
FCC 2010

Program

June 27th

14:00-16:00 Session I: Computational soundness -- logics and protocols

• Computationally Sound Verification of the NSL Protocol via Computationally Complete Symbolic Attacker (Abstract)
  Pedro Adao, Gergei Bana and Hideki Sakurada
• A decision procedure for Bana and Comon-Lundh's logical framework for computational security proof of protocols (Abstract)
  Hubert Comon-Lundh, Veronique Cortier and Guillaume Scerri
• Towards Composable Computational Soundness for Signatures and Zero-Knowledge Proofs (Abstract)
  Michael Backes, Fabian Bendun and Esfandiar Mohammadi
• Computational Soundness of Symbolic Zero-knowledge Proofs: Weaker Assumptions and Mechanized Verification (Abstract)
  Michael Backes, Fabian Bendun and Dominique Unruh

16:00-16:30 Coffee

16:30-18:00 Session II: Tools for computational security

• Verified Security of Hashed Authenticated Key-Exchange Protocols (Abstract)
  Gilles Barthe, Juan Manuel Crespo, Cristian Ene, Cesar Kunz, and Yassine Lakhnech
• Computational Analysis of the UMTS and LTE Authentication and Key Agreement Protocols (Abstract)
  Joe-Kai Tsay and Stig F. Mjolsnes
• Computer-aided privacy proofs (Abstract)
  Gilles Barthe, Benjamin Gregoire, Cesar Kunz and Santiago Zanella Beguelin

June 28th

09:30-10:30 Session III: Formal and computational cryptography -- cross pollination

• Computational Semantics for Epistemic Logic (Abstract)
  Rohit Chadha, Yusuke Kawamoto and Steve Kremer
• Symbolic Probabilistic Analysis of Off-line Guessing (Abstract)
  Bruno Conchinha, David Basin and Carlos Caleiro

10:30-11:00 Coffee

11:00-12:30 Soundness and APIs -- Joint session with ASA

• Invited talk: From APIs to Computational Cryptography: A Verified Implementation of TLS
  Cedric Fournet
• Proving Computational Security with a General-Purpose C Verifier (Abstract)
  Francois Dupressoir, Cedric Fournet and Andrew D. Gordon