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

郭云川; 丁丽; 周渊; 郭莉

您当前的位置：

首页 >

文章列表页 >

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

短文 | 更新时间：2024-10-14

- 基于ProVerif的电子商务协议分析
- Analysis for e-commerce protocols based on ProVerif
- 通信学报 2009年30卷第3期页码：125-129
- 作者机构：
  
  1. 中国科学院计算技术研究所
  2. 中国科学院研究生院
  3. 国家计算机网络应急技术处理协调中心
- 作者简介：
- 基金信息：
  
  国家重点基础研究发展计划(“973”计划)基金资助项目(2007CB311100);国家高技术研究发展计划(“863”计划)基金资助项目(2007AA01Z446);国家自然科学基金资助项目(60703021,60873217)~~
- DOI：
  中图分类号： TP393.04
- 纸质出版日期：2009
- 稿件说明：
移动端阅览
郭云川, 丁丽, 周渊, 等. 基于ProVerif的电子商务协议分析[J]. 通信学报, 2009,30(3):125-129.

GUO Yun-chuan1, DING Li3, ZHOU Yuan3, et al. Analysis for e-commerce protocols based on ProVerif[J]. 2009, 30(3): 125-129.
郭云川, 丁丽, 周渊, 等. 基于ProVerif的电子商务协议分析[J]. 通信学报, 2009,30(3):125-129. DOI：

GUO Yun-chuan1, DING Li3, ZHOU Yuan3, et al. Analysis for e-commerce protocols based on ProVerif[J]. 2009, 30(3): 125-129. DOI：

摘要

采用应用pi演算来建模自动解决争端的公平电子商务协议

基于一致性给出了公平性的形式描述方法

利用应用pi演算的自动化分析工具——ProVerif分析了该协议

结果表明

利用一致性描述协议公平性是可行的

同时指出了基于ProVerif验证电子商务协议的优缺点:适用于分析"A事件发生以前

B事件是否曾经发生"

但不适用于分析"A事件发生之后

B事件将来是否会必然(或可能)发生"。

Abstract

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 picalculus 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.

关键词

Keywords

references

浏览量

311

下载量

CSCD

文章被引用时，请邮件提醒。

提交

工具集

关联资源

基于角色的区块链拍卖合约抽象建模及其时间安全性与公平性验证

信任环境下考虑系统公平性的边缘计算卸载策略和资源分配

反向散射辅助的无线供能通信网络中用户能效公平性研究

基于链路容量的多路径拥塞控制算法

基于网络效用最大化理论的分布式车联网拥塞控制策略