Cryptographic Protocols Analysis in Event B

Nazim Benaissa 1 Dominique Méry 1
1 MOSEL - Proof-oriented development of computer-based systems
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We consider the proof-based development of cryptographic protocols satisfying security properties. For instance, the model of Dolev- Yao provides a way to integrate a description of possible attacks, when designing a protocol. We use existing protocols and want to provide a systematic way to prove but also to design cryptographic protocols; moreover, we would like to provide proof-based guidelines or patterns for integrating cryptographic elements in an existing protocol. The goal of the paper is to present a first attempt to mix design patterns (as in software engineering) and formal methods (as a verification tool). We illustrate the technique on the well known Needham-Schroeder public key protocol and Blake-Wilson-Menezes key transport protocol. The un- derlying modelling language is Event B and is supported by the RODIN platform, which is used to validate models.
Type de document :
Communication dans un congrès
Seventh International Andrei Ershov Memorial Conference «PERSPECTIVES OF SYSTEM INFORMATICS» - PSI 2009, Jun 2009, Novosibisrk, Russia. Springer-Verlag, 2009, Lectures Notes in Computer Science
Liste complète des métadonnées

https://hal.inria.fr/inria-00431264
Contributeur : Dominique Méry <>
Soumis le : mercredi 11 novembre 2009 - 14:18:12
Dernière modification le : jeudi 11 janvier 2018 - 06:19:52

Identifiants

  • HAL Id : inria-00431264, version 1

Collections

Citation

Nazim Benaissa, Dominique Méry. Cryptographic Protocols Analysis in Event B. Seventh International Andrei Ershov Memorial Conference «PERSPECTIVES OF SYSTEM INFORMATICS» - PSI 2009, Jun 2009, Novosibisrk, Russia. Springer-Verlag, 2009, Lectures Notes in Computer Science. 〈inria-00431264〉

Partager

Métriques

Consultations de la notice

134