摘要
采用应用pi演算来建模自动解决争端的公平电子商务协议,基于一致性给出了公平性的形式描述方法,利用应用pi演算的自动化分析工具——ProVerif分析了该协议,结果表明,利用一致性描述协议公平性是可行的,同时指出了基于ProVerif验证电子商务协议的优缺点:适用于分析"A事件发生以前,B事件是否曾经发生",但不适用于分析"A事件发生之后,B事件将来是否会必然(或可能)发生"。
It was very important to analyze e-commerce protocols by formal methods. A technique for modeling the fair-change e-commerce protocol （FEEP） with automated dispute resolution and for verifying its property was proposed. First, FEEP was modeled in applied pi-calculus and a novel formalization of the fairness was provided in term of a correspondence property. Then, ProVerif, proposed by Juels, Catalano and Jakobsson, was adopted to analyze FEEP automatically. The results show that：it is feasible to formalize the fairness based on a correspondence property; ProVerif can be used to verify the property that before event A happened, event B had happened, but it is not applicable to analyze the property that after event A happened, event B would happen.
出处
《通信学报》
EI
CSCD
北大核心
2009年第3期125-129,共5页
Journal on Communications
基金
国家重点基础研究发展计划(“973”计划)基金资助项目(2007CB311100)
国家高技术研究发展计划(“863”计划)基金资助项目(2007AA01Z446)
国家自然科学基金资助项目(60703021,60873217)~~
