Formal Verification and Simulation of the NetBill Protocol Using SPIN
José García-Fanjul, Javier Tuya, José A. Corrales
In: 4th International Workshop on Automata Theoretic Verification with the SPIN Model Checker, París, pp. 195-210, 1998
(ps.zip)

Abstract

Electronic Commerce and Internet are profoundly changing the way goods are exchanged, but there is still little confidence among users concerning the security of their data. The application of formal techniques to the modelling and design of electronic commerce protocols should help to improve their reliability and so enhance the choices of these new technologies. In this paper, basic concepts of security and payment protocols are described, the NetBill protocol is graphically specified and its behaviour in terms of reliability is formally verified using the SPIN tool.

Index - Testing - Personal Page