The past, present and future of protocol checking with CSP and FDR

Abstract : The prehistory of AVoCS (that is, the series of workshops that gave birth to it) consisted of once or twice annual workshops sponsored by DERA (originally by Peter Ryan) from about 1995, usually held in Oxford or Royal Holloway. The focus of many of these meetings was the development of the CSP model of cryptographic protocols, following Gavin Lowe's discovery that they could be modelled successfully on FDR in 1994. That work led directly or indirectly to most of the formal work done on security protocols since, but naturally many of those whose work was triggered by these discoveries have translated or re-created the ideas in their own notations. In this talk I will show the particular advantages of using a process algebra, and CSP in particular, for modelling cryptoprotocols, and also some of the problems we have had. I will concentrate on the problem of proving protocols in general, rather than specific small implementations. These methods are based on data independence and in particular the insight of Ranko Lazic that it is possible to get strong results about systems that may include conditional checks for equalities, but not inequalities. In particular, reporting recent joint work with Eldar Kleiner and Tilo Buschmann, I will show how previous work on this topic can be simplified (and automated in Casper) in such a way that it produces remarkably quick proofs or refutations. This work has led to some interesting insights into the relationship between model checking and other methods of protocol analysis based on strand spaces and Horn clauses.
Type de document :
Communication dans un congrès
Stephan Merz and Tobias Nipkow. Automatic Verification of Critical Systems, Sep 2006, Nancy/France, pp.5, 2006, Automatic Verification of Critical Systems (AVoCS 2006)
Liste complète des métadonnées

https://hal.inria.fr/inria-00091659
Contributeur : Stephan Merz <>
Soumis le : mercredi 6 septembre 2006 - 19:02:55
Dernière modification le : mercredi 6 septembre 2006 - 20:48:28
Document(s) archivé(s) le : jeudi 20 septembre 2012 - 10:20:58

Fichier

Identifiants

  • HAL Id : inria-00091659, version 1

Collections

Citation

Bill Roscoe. The past, present and future of protocol checking with CSP and FDR. Stephan Merz and Tobias Nipkow. Automatic Verification of Critical Systems, Sep 2006, Nancy/France, pp.5, 2006, Automatic Verification of Critical Systems (AVoCS 2006). 〈inria-00091659〉

Partager

Métriques

Consultations de la notice

98

Téléchargements de fichiers

85