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
Complete list of metadatas

https://hal-lara.archives-ouvertes.fr/hal-02101908
Contributor : Colette Orange <>
Submitted on : Wednesday, April 17, 2019 - 9:09:33 AM
Last modification on : Thursday, November 21, 2019 - 2:34:03 AM

File

RR2001-31.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02101908, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

3

Files downloads

8