We consider the refinement-based process for the development of security protocols. Our approach is based on the Event B refinement, which makes proofs easier and which makes the design process faithfull to the structure of the protocol as the designer thinks of it. We introduce the notion of mechanism related to a given security property; a mechanism can be combined with another mechanism through the double refinement process ensuring the preservation of previous security properties of mechanisms. Mechanisms and combination of mechanisms are based on Event B models related to the security property of the current mechanism. Analysing cryptographic protocols requires precise modelling of the attacker's knowledge and the attacker's behaviour conforms to the Dolev-Yao model. © 2010 Springer-Verlag.
CITATION STYLE
Benaissa, N., & Méry, D. (2010). Proof-based design of security protocols. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6072 LNCS, pp. 25–36). https://doi.org/10.1007/978-3-642-13182-0_3
Mendeley helps you to discover research relevant for your work.