一种电子商务协议形式化分析方法

被引：24

作者：

卿斯汉

机构：

[1] 中国科学院软件研究所信息安全技术工程研究中心北京北京中科安胜信息技术有限公司

来源：

软件学报 | 2005年 / 10期

基金：

北京市自然科学基金;

关键词：

形式化分析; 电子商务协议; 可追究性; 公平性; 可信第三方;

D O I：

暂无

中图分类号：

TP393.04 [];

学科分类号：

081201 ; 1201 ;

摘要：

提出了一种新颖的形式化方法,可以用于分析电子商务协议的安全性质,例如可追究性和公平性.与以前的工作相比较,主要贡献在于:(1)对协议主体的拥有集合给出了形式化定义,且主体的初始拥有集合只依赖于环境;(2)将协议的初始状态假设集合分为3类:基本假设集合、可信假设集合和协议理解假设集合,避免了因非形式化的初始假设而产生的分析错误;(3)对可信假设作细粒度的形式化规范,揭示协议的内涵;(4)建立公理系统,使新方法更为严格与合理.

引用

页码：1757 / 1765

页数：9

共 9 条

[1] 公平交换协议的一个形式化模型 [J].

卿斯汉 ;

李改成 .

中国科学E辑:信息科学, 2005, (02) :161-172

[2] 电子商务协议中的可信第三方角色 [J].

卿斯汉 .

软件学报, 2003, (11) :1936-1943

[3] 安全协议的设计与逻辑分析 [J].

卿斯汉 .

软件学报, 2003, (07) :1300-1309

[4] 一种分析电子商务协议的新工具 [J].

周典萃 ;

卿斯汉 ;

周展飞 .

软件学报, 2001, (09) :1318-1328

[5] Kailar逻辑的缺陷 [J].

周典萃 ;

卿斯汉 ;

周展飞 .

软件学报, 1999, (12) :1238-1245

[6]

密码学与计算机网络安全[M]. - 清华大学出版社 , 卿斯汉著, 2001

[7]

安全协议[M]. - 清华大学出版社 , 卿斯汉编著, 2005

[8]

Practical protocols for certified electronic mail[J] . Robert H. Deng,Li Gong,Aurel A. Lazar,Weiguo Wang.Journal of Network and Systems Management . 1996 (3)

[9] A LOGIC OF AUTHENTICATION [J].

BURROWS, M ;

ABADI, M ;

NEEDHAM, R .

ACM TRANSACTIONS ON COMPUTER SYSTEMS, 1990, 8 (01) :18-36

← 1 →