  Use of formal techniques for verifying the security features of electronic
commerce protocols would facilitate, the enhancement of reliability of such
protocols, thereby increasing their usability. This paper projects the
application of logic programming techniques for formal verification of a well
referred security and transactions protocol, the NetBill. The paper uses ALSP
(Action Language for Security Protocols) as an efficient formal specification
language and SMODELS a model generator to formally analyze and plan attacks on
the protocol.
