Skip to Main content Skip to Navigation

Formally validated specification of a micro-payment protocol

Abstract : 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
Document type :
Complete list of metadata
Contributor : Colette Orange Connect in order to contact the contributor
Submitted on : Wednesday, April 17, 2019 - 9:09:33 AM
Last modification on : Saturday, September 11, 2021 - 3:19:17 AM


Files produced by the author(s)


  • HAL Id : hal-02101908, version 1



Pierre Dargenton, Daniel Hirschkoff, Pierre Lescanne, E. Pommateau. Formally validated specification of a micro-payment protocol. [Research Report] LIP RR-2001-31, Laboratoire de l'informatique du parallélisme. 2001, 2+15p. ⟨hal-02101908⟩



Les métriques sont temporairement indisponibles