Novel Logical Method for Security Analysis of Electronic Payment Protocols
This work addresses security analysis for electronic payment protocols, which is crucial for secure e-commerce, but it is incremental as it builds on an existing logical method.
The paper tackled the lack of timeliness analysis in formal methods for electronic payment protocols by proposing a novel logical approach that extends an existing method with time expressions and inference rules. It applied this to the Netbill protocol, finding a fairness issue due to timeliness, demonstrating the approach's ability to analyze key security properties.
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.