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)

Abstract

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
PublisherSpringer
Pages96-110
Number of pages15
ISBN (Electronic)978-3-319-19458-5
ISBN (Print)978-3-319-19457-8
DOIs
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
PublisherSpringer
Volume9128
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Workshop

Workshop20th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2015
Abbreviated titleFMICS
CountryNorway
CityOslo
Period22/06/1523/06/15

Fingerprint

Model checking
Servers
Network protocols
World Wide Web
Computer systems

Keywords

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

Cite this

Chaudhary, K., & Fehnker, A. (2015). Model Checking a Server-Side Micro Payment Protocol. In M. Núñez, & M. Güdemann (Eds.), Formal Methods for Industrial Critical Systems: 20th International Workshop, FMICS 2015, Oslo, Norway, June 22-23, 2015 Proceedings (pp. 96-110). (Lecture Notes in Computer Science; Vol. 9128). Berlin: Springer. https://doi.org/10.1007/978-3-319-19458-5_7
Chaudhary, Kaylash ; Fehnker, Ansgar . / Model Checking a Server-Side Micro Payment Protocol. Formal Methods for Industrial Critical Systems: 20th International Workshop, FMICS 2015, Oslo, Norway, June 22-23, 2015 Proceedings. editor / Manuel Núñez ; Matthias Güdemann. Berlin : Springer, 2015. pp. 96-110 (Lecture Notes in Computer Science).
@inproceedings{9523acd8378b47ae90889f3a8789e77d,
title = "Model Checking a Server-Side Micro Payment Protocol",
abstract = "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.",
keywords = "Model Checking, Verification, CSP, Micropayment protocols, Virtual payment systems, PAT",
author = "Kaylash Chaudhary and Ansgar Fehnker",
year = "2015",
doi = "10.1007/978-3-319-19458-5_7",
language = "English",
isbn = "978-3-319-19457-8",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "96--110",
editor = "Manuel N{\'u}{\~n}ez and Matthias G{\"u}demann",
booktitle = "Formal Methods for Industrial Critical Systems",

}

Chaudhary, K & Fehnker, A 2015, Model Checking a Server-Side Micro Payment Protocol. in M Núñez & M Güdemann (eds), Formal Methods for Industrial Critical Systems: 20th International Workshop, FMICS 2015, Oslo, Norway, June 22-23, 2015 Proceedings. Lecture Notes in Computer Science, vol. 9128, Springer, Berlin, pp. 96-110, 20th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2015, Oslo, Norway, 22/06/15. https://doi.org/10.1007/978-3-319-19458-5_7

Model Checking a Server-Side Micro Payment Protocol. / Chaudhary, Kaylash; Fehnker, Ansgar .

Formal Methods for Industrial Critical Systems: 20th International Workshop, FMICS 2015, Oslo, Norway, June 22-23, 2015 Proceedings. ed. / Manuel Núñez; Matthias Güdemann. Berlin : Springer, 2015. p. 96-110 (Lecture Notes in Computer Science; Vol. 9128).

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

TY - GEN

T1 - Model Checking a Server-Side Micro Payment Protocol

AU - Chaudhary, Kaylash

AU - Fehnker, Ansgar

PY - 2015

Y1 - 2015

N2 - 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.

AB - 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.

KW - Model Checking

KW - Verification

KW - CSP

KW - Micropayment protocols

KW - Virtual payment systems

KW - PAT

U2 - 10.1007/978-3-319-19458-5_7

DO - 10.1007/978-3-319-19458-5_7

M3 - Conference contribution

SN - 978-3-319-19457-8

T3 - Lecture Notes in Computer Science

SP - 96

EP - 110

BT - Formal Methods for Industrial Critical Systems

A2 - Núñez, Manuel

A2 - Güdemann, Matthias

PB - Springer

CY - Berlin

ER -

Chaudhary K, Fehnker A. Model Checking a Server-Side Micro Payment Protocol. In Núñez M, Güdemann M, editors, Formal Methods for Industrial Critical Systems: 20th International Workshop, FMICS 2015, Oslo, Norway, June 22-23, 2015 Proceedings. Berlin: Springer. 2015. p. 96-110. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-319-19458-5_7