  Electronic payment protocols play a vital role in electronic commerce
security, which is essential for secure operation of electronic commerce
activities. Formal method is an effective way to verify the security of
protocols. But current formal method lacks the description and analysis of
timeliness in electronic payment protocols. In order to improve analysis
ability, a novel approach to analyze security properties such as
accountability, fairness and timeliness in electronic payment protocols is
proposed in this paper. This approach extends an existing logical method by
adding a concise time expression and analysis method. It enables to describe
the event time, and extends the time characteristics of logical inference
rules. We analyzed the Netbill protocol with the new approach and found that
the fairness of the protocol is not satisfied, due to timeliness problem. The
result illustrates the new approach is able to analyze the key properties of
electronic payment protocols. Furthermore, the new approach can be introduced
to analyze other time properties of cryptographic protocols.
