Skip to Main content Skip to Navigation
New interface
Reports (Research report)

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 :
Reports (Research report)
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 : Wednesday, October 26, 2022 - 8:15:50 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⟩



Record views


Files downloads