Proof-Based Design of Security Protocols

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.