Modèle formel pour l’analyse de propriétés du protocole

Ce chapitre propose une alternative basée sur la modélisation formelle pour concevoir et évaluer le protocole en ne focalisant plus sur sa performance, mais plutôt sur ses propriétés intrinsèques, notamment afin de montrer les garanties qu'il apporte sous des hypothèses identifiées. Le protocole de l'étude de cas est analysé avec la méthode Event-B, ainsi que chaque étape de sa vérification.