on the link between formal and computational models
Paris, 23-24 June 2005

Call for participation
List of participants and abstracts of the talks
Organizing committee

Scope of the workshop

The workshop will focus on the relations between the symbolic (Dolev-Yao) model and the computational (complexity-theoretic) model, and more broadly on new advances and research directions in protocol verification.


The workshop will take place at École Normale Supérieure, in Paris.
The conference room is the "Salle Jules Ferry", located 29 rue d'Ulm, 75005 Paris. Please notice that this conference room is NOT located at the main building of the École Normale Supérieure de Paris but at a building named "Institut National de Recherche Pedagogique", next building 5 and between building 5 and 6 on the map.

Registration (free)

The participation to the workshop is free but registration is mandatory.

If you are interested in participating, please send an email to
If moreover you are interested in giving a talk, please send to a title and a short abstract (one or two paragraphs) with an indication whether you intend to give a long or a short talk.

Please register by May 31st.

Registrations after May 31st are welcome, but unfortunately we may not be able to include all late registrants in lunches and dinners, and to include talks proposed late (though we will try).


Here is a list of hotels, approximately from the cheapest to the most expensive.
All of them are within walking distance of Ecole Normale Superieure. Hotel Pierre Nicole is a bit further than the others (550 meters), but cheaper.

There are plenty of restaurants near the Ecole Normale Supérieure. Most of them are located in rue Mouffetard and in rue du Pot de Fer: with 42 restaurants just in those two streets, you should not have problems in finding one to your taste.
Here is a list of restaurants we can recommend.

Organizing Committee

  Martin Abadi, University of California at Santa Cruz, USA
  Bruno Blanchet, CNRS, Laboratoire d'Informatique de l'École Normale Supérieure, Paris, France
  Véronique Cortier, CNRS, LORIA, Nancy, France
  Cédric Fournet, Microsoft Research, Cambridge Lab, United Kingdom
  Steve Kremer, INRIA, Laboratoire Spécification et Vérification, Cachan, France
  Yassine Lakhnech, Université Joseph Fourier, VERIMAG Lab., Grenoble, France


Artist2: Network of Excellence on Embedded Systems Design IST-004527
ACI Jeunes Chercheurs JC 9005 (in french): Link between cryptanalysis and logical models for cryptographic protocols
Projet RNTL PROUVÉ : Protocoles cryptographiques : outils de vérification automatiques

Last modified on June 10th, 2005.