Modeling And Verification For The Micropayment Protocol Netpay
Kaylash Chaudhary, Ansgar Fehnker · Zenodo (CERN European Organization for Nuclear Research) · 2012
There are many virtual payment systems available to conduct micropayments. It is essential that the protocols satisfy the highest standards of correctness. This paper examines the Netpay Protocol [3], provide its formalization as automata model, and prove two important correctness properties, namely absence of deadlock and validity of an ecoin during the execution of the protocol. This paper assumes a cooperative customer and will prove that the protocol is executing according to its description.