Models and Tools for Security Analysis and Proofs

29th April 2017, University Pierre and Marie Curie (UPMC), Paris, France

The ECRYPT-CSA project is organizing a one-day workshop on Models and Tools for Security Analysis and Proofs. The workshop is co-located with IEEE Euro Security and Privacy and Eurocrypt 2017 .


It has become clear that computer aided tools and their associated abstract models are indispensable to scalable and rigorous analysis of cryptographic systems. The aim of the workshop is two-fold: to survey the state of the art in the area and to chart future research directions. The workshop is addressed to both researchers in the area of formal models and tools but also to cryptographers interested in the limits and support provided by existing tools. There will be plenty of scope for discussion.

Confirmed speakers

Programme (tentative)

8:00-9:00 Breakfast/Registration
9:00-9:45 Gilles Barthe: Programming language methods for cryptography
9:45 - 10:30 Veronique Cortier: Models and Tools for Electronic Voting protocols (Slides)
10:30 - 11:00 Coffee Break
11:00-12:00 Peter Schwabe: Two approaches to verifiying high-speed ECC software
12:00 - 14:00 Lunch
14:00-14:30 Karthik Barghavan: HACL*: Writing and verifying a cryptographic library in F*
14:30-15:00 Jonathan Protzenko: KreMLin, a secure compiler from F* to C
15:00-15:30 Cedric Fournet: Type-based cryptographic verification in F*
15:30-16:00 Coffee break
16:00-16:45 Bruno Blanchet: CryptoVerif:state of the art, perspectives, and relations to other tools (Slides)
16:45 - 17:30 Joshua Guttman: Measuring protocol strength with security goals

Organizers and Contacts

  • Manuel Barbosa (INESC TEC and FCUP, Porto --,
  • Cas Cremers (Oxford University -- ),
  • Bogdan Warinschi (University of Bristol --


Please register using the link avilable from the Eurocrypt'17 site:


The workshop will be held at the University Pierre and Marie Curie (UPMC), Paris, France.