使用通信顺序进程CSP和博弈理论提出了基于动态博弈的电子支付系统模型,提出了一种电子支付协议的新属性自利性;基于纳什均衡理论给出了自利性的形式化定义,可以用于对电子支付系统安全属性的形式化分析。与以前的工作相比,其主要贡献为:基于CSP事件对参与者的交叠并发和同步行为建模,基于博弈策略理论对协议主体的多种不诚实行为和三种质量的通信媒介建模,可以用于分析协议主体与通信媒介之间的合作和竞争行为;对进程失效和通信失效建模,其中通信失效模型考虑了消息延迟导致的失效,因此可以分析更多失效情况下协议的性质;自利性解决了如何描述协议公平性和计算代价的折中性问题,可以表示以协议主体为中心的性质如匿名性等;证明了在给定条件下协议的公平性蕴涵自利性,反之不成立。
This paper built a dynamic game-based model of electronic ecommerce systems, and presented self-interested property in electronic payment protocol' s. In the model, it gave a formal description of self-interested property, which was used to analyze formally security property of electronic payment protocols. Compared with the previous work, the main contributions are the following. Firstly, modeling channels in different qualities and participants of dishonest behaviors helped to analyze co- operative and adversarial behaviors. Secondly, modeling process failure and channel failure helped to analyze a protocol's se- curity properties in failed environment. Thirdly, self-interested property was applicant to all kinds of electronic payment protocols, and it represented a trade-off between complexity and what they achieve, and that it was applicable in any transaction where participants had different interests to protect such as protecting one' s privacy and accepting items sent by the other party. Fourthly, it has been proved that fairness implies self-interested under some conditions and the inverse is not true.