Using the B Method to Model Protocols
Jean-Louis Lanet · 2007
In this paper we suggest to use the B formal method to model a protocol dedicated to smart cards. We use a pragmatic approach to prove the dynamic properties of the protocol by using historical variables to express the past. We check manually that those variables have been correctly updated in the different operations. With this approach we can avoid the use of a model checker to verify the dynamic properties. We show the advantages of this method to express general properties and service properties. We focused on the formalisation of the rules given in the standard and on the refinement process. We introduce new events and invariants at each level. Using this method enabled us to bring to the fore some ambiguities and errors of the protocol. 1.