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 underlying modelling language is Event B and is supported by the RODIN platform, which is used to validate models. © 2010 Springer Berlin Heidelberg.
CITATION STYLE
Benaissa, N., & Méry, D. (2010). Cryptographic protocols analysis in event B. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5947 LNCS, pp. 282–293). https://doi.org/10.1007/978-3-642-11486-1_24
Mendeley helps you to discover research relevant for your work.