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