Abstract
| 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 | |
| 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 |
Fingerprint
Keywords
- Model Checking
- Verification
- CSP
- Micropayment protocols
- Virtual payment systems
- PAT
Cite this
}
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
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 -