Eighth Workshop on
Formal and Computational Cryptography
FCC 2010

Harvard University, June 27th--28th, 2012


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