An Incremental Proof-Based Process of the NetBill Electronic Commerce Protocol

This paper presents an incremental formal modeling of the NetBill protocol using Event-B method. The NetBill protocol is an electronic commerce protocol designed for micropayment systems for selling and delivery of information and goods through the internet. We model the protocol step by step using refinement, which is the key mechanism of the Event-B method. Event-B modeling starts with an abstraction of a system and adds details during refinement levels in order to gain a final model close to the implementation. Moreover mathematical proofs are incorporated into Event-B to verify the correctness of refinement steps. The outcome of this incremental approach was that we achieved a very high degree of automatic proof. In the developed Event-B model of the NetBill protocol described in this paper, all proofs are generated and discharged by the Rodin tool.