基于ProVerif的电子商务协议分析  

Analysis for e-commerce protocols based on ProVerif

作　　者：郭云川[1,2] 丁丽[3] 周渊[3] 郭莉[1] 

机构地区：[1]中国科学院计算技术研究所,北京100019 [2]中国科学院研究生院,北京100049 [3]国家计算机网络应急技术处理协调中心,北京100029

出　　处：《通信学报》2009年第3期125-129,共5页Journal on Communications

基　　金：国家重点基础研究发展计划(“973”计划)基金资助项目(2007CB311100);国家高技术研究发展计划(“863”计划)基金资助项目(2007AA01Z446);国家自然科学基金资助项目(60703021,60873217)~~

摘　　要：采用应用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.

关 键 词：电子商务协议 公平性 ProVerif 

分 类 号：TP393.04[自动化与计算机技术—计算机应用技术]