Model Checking a Server-Side Micro Payment Protocol

Kaylash Chaudhary; Ansgar  Fehnker

doi:10.1007/978-3-319-19458-5_7

Model Checking a Server-Side Micro Payment Protocol

Kaylash Chaudhary, Ansgar Fehnker

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-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 language	English
Title of host publication	Formal Methods for Industrial Critical Systems
Subtitle of host publication	20th International Workshop, FMICS 2015, Oslo, Norway, June 22-23, 2015 Proceedings
Editors	Manuel Núñez, Matthias Güdemann
Place of Publication	Berlin
Publisher	Springer
Pages	96-110
Number of pages	15
ISBN (Electronic)	978-3-319-19458-5
ISBN (Print)	978-3-319-19457-8
DOIs	https://doi.org/10.1007/978-3-319-19458-5_7
Publication status	Published - 2015
Externally published	Yes
Event	20th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2015 - Oslo, Norway Duration: 22 Jun 2015 → 23 Jun 2015 Conference number: 20

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	9128
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Workshop

Workshop	20th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2015
Abbreviated title	FMICS
Country	Norway
City	Oslo
Period	22/06/15 → 23/06/15

Keywords

Model Checking
Verification
CSP
Micropayment protocols
Virtual payment systems
PAT

Access to Document

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

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

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). Springer. https://doi.org/10.1007/978-3-319-19458-5_7

@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",

note = "20th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2015, FMICS ; Conference date: 22-06-2015 Through 23-06-2015",

}

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 proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Model Checking a Server-Side Micro Payment Protocol

AU - Chaudhary, Kaylash

AU - Fehnker, Ansgar

N1 - Conference code: 20

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

T2 - 20th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2015

Y2 - 22 June 2015 through 23 June 2015

ER -