Skip to Main content Skip to Navigation
Conference papers

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.
Complete list of metadata
Contributor : Dominique Méry Connect in order to contact the contributor
Submitted on : Wednesday, November 11, 2009 - 11:31:41 AM
Last modification on : Friday, February 4, 2022 - 3:14:50 AM


  • HAL Id : inria-00431253, version 1



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. ⟨inria-00431253⟩



Record views