Proof-Based Design of Security Protocols
Abstract
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 con- forms to the Dolev-Yao model.
Ce document présente une méthodologie de développement incrémental de protocoles cryptographiques guidé par la preuve de pas de raffinement. Le cadre de développement est la méthode Event B et nous analysons les mécanismes de composition de protocoles à l'aide de la technique de raffinement. En particulier, nous utilisons une formalisation du modèle de Dolev et Yao pour modéliser les protocoles.