Formally validated specification of a micro-payment protocol
Résumé
In this paper, we develop a formal specification for a micro-payment protocol, first on paper, then within the Coq proof assistant. Our approach in defining a notion of execution traces for protocol runs is inspired by previous works, notably by L. Paulson (in the Isabelle/HOL System). However, we show that the protocol we study entails some modifications to Pailson's frameword, related to the modeling of the agents' internal state. We moreover take profit from Coq's expressive meta-language to mechanically derive proofs bout the formalisation itself, by introducing a notion a well-formedness for protocol rules
Cet article présente la spécification formelle d'un protocole de micro-paiement d'abord par une définition sur papier, puis par une formalisation dans l'assistant à la preuve Coq. Nous nous inspirons d'une méthode employée principalement par L. Paulson afin d'introduire une notion de trace pour les exécutions du protocole que nous étudions.Néanmoins, le traitement du protocole en question rend nécessaires quelques modifications à l'approche de Paulson, en rapport avec la modélisation de l'état interne des agents. Nous exploitons le cadre formel fourni par Coq pour valider la spécification qui 'est faire en prouvant des propriétés de la spécification proposée, propriétés qui s’expriment çà travers une notion de bonne formation des règles définissant les étapes du protocole
Origine : Fichiers produits par l'(les) auteur(s)