Cryptologic protocols analysis using proof-based patterns

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. The main motivation is that cryptographic protocols are very complex systems to prove and to design, since they are based on specific assumptions. For instance, the model of Dolev-Yao pro- vides 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 patterns for integrating cryptographic elements in an existing pro- tocol. The goal of the paper is to present an attempt to mix design patterns (as in software engineering) and formal methods (as a verification tool). We use the notion of proof-based design pattern, allow- ing a correct-by-construction approach to security protocols. Communication channels are supposed to be unsafe. Analysing cryptographic protocols requires precise modelling of the attacker's knowl- edge. In this paper, we present a technique for analysing key establishment protocols. The attacker's behaviour conforms to the Dolev-Yao model. In the Dolev-Yao model, the attacker has full control of the communication channel, and the cryptographic primitives are supposed to be perfect. We illustrate the technique on the well known Needham-Schroeder public key protocol and Blake-Wilson-Menezes key transport protocol. The underlying 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, Novosibirsk, Russia. Springer-Verlag, 2009, Lecture Notes in Computer Science
Liste complète des métadonnées

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

Identifiants

  • HAL Id : inria-00431253, version 1

Collections

Citation

Nazim Benaissa, Dominique Méry. Cryptologic protocols analysis using proof-based patterns. Seventh International Andrei Ershov Memorial Conference "PERSPECTIVES OF SYSTEM INFORMATICS" - PSI 2009, Jun 2009, Novosibirsk, Russia. Springer-Verlag, 2009, Lecture Notes in Computer Science. 〈inria-00431253〉

Partager

Métriques

Consultations de la notice

143