Model Checking a Server-Side Micro Payment Protocol

Kaylash Chaudhary, Ansgar Fehnker

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

1 Citation (Scopus)


Many virtual payment systems are available on the world wide web for micropayment, and as they deal with money, correctness is important. One such payment system is Netpay. This paper examines the server-side version of the Netpay protocol and provides its formalization as a CSP model. The PAT model checker is used to prove three properties essential for correctness: impossibility of double spending, validity of an ecoin during the execution and the absence of deadlock. We prove that the protocol is executing according to its description based on the assumption that the customers and vendors are cooperative. This is a very strong assumption for system built to prevent abuse, but further analysis suggests that without it the protocol does no longer guarantee all correctness properties.
Original languageEnglish
Title of host publicationFormal Methods for Industrial Critical Systems
Subtitle of host publication20th International Workshop, FMICS 2015, Oslo, Norway, June 22-23, 2015 Proceedings
EditorsManuel Núñez, Matthias Güdemann
Place of PublicationBerlin
Number of pages15
ISBN (Electronic)978-3-319-19458-5
ISBN (Print)978-3-319-19457-8
Publication statusPublished - 2015
Externally publishedYes
Event20th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2015 - Oslo, Norway
Duration: 22 Jun 201523 Jun 2015
Conference number: 20

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Workshop20th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2015
Abbreviated titleFMICS


  • Model Checking
  • Verification
  • CSP
  • Micropayment protocols
  • Virtual payment systems
  • PAT


Dive into the research topics of 'Model Checking a Server-Side Micro Payment Protocol'. Together they form a unique fingerprint.

Cite this