SET协议模型的改进与SMV分析

doi:10.3778/j.issn.1002-8331.2010.08.032

计算机工程与应用 ›› 2010, Vol. 46 ›› Issue (8): 113-116.DOI: 10.3778/j.issn.1002-8331.2010.08.032

SET协议模型的改进与SMV分析

鲁四美，张建林

首都师范大学信息工程学院，北京 100048

收稿日期:2008-09-12 修回日期:2008-12-08 出版日期:2010-03-11 发布日期:2010-03-11
通讯作者: 鲁四美

Improvement of SET protocol model and formal analysis via SMV

LU Si-mei，ZHANG Jian-lin

College of Information Engineering，Capital Normal University，Beijing 100048，China

Received:2008-09-12 Revised:2008-12-08 Online:2010-03-11 Published:2010-03-11
Contact: LU Si-mei

摘要/Abstract

摘要： 在以Lu&Smolka对SET协议支付过程的简化模型为研究对象的情况下，进行形式化建模和有限状态机模型。同时应用CTL对相应的安全性质进行形式描述，并在网络环境被入侵者控制的假设下，利用SMV分析了协议的认证性、保密性和完整性，发现攻击并对该攻击所产生的影响进行了讨论。最后修改其协议模型对改进后的协议进行分析和检验，说明了SET协议独具特色的双重签名在整个协议运行中至关重要。

Abstract: The simplified model of payment process of the SET protocol is used to build up its formal model and finite state machine model，as well as CTL formulations of the security properties are presented.Under the assumption of the network environment being controlled by intruder，the symbolic model checking ware（SMV） is applied for analyzing the authentication，confidentiality and integrity，attacks are found.Then，the influence of attacks is discussed.Finally，the protocol model is optimized.The result of analysis and checking indicates the importance of dual signature on SET protocol.

中图分类号:

TP309

鲁四美，张建林. SET协议模型的改进与SMV分析[J]. 计算机工程与应用, 2010, 46(8): 113-116.

LU Si-mei，ZHANG Jian-lin. Improvement of SET protocol model and formal analysis via SMV[J]. Computer Engineering and Applications, 2010, 46(8): 113-116.

[1]	陈宁，胡安峰. 一种结合DWT和DFT的彩色图像盲水印方案[J]. 计算机工程与应用, 2010, 46(9): 88-91.
[2]	徐璐，张红旗，杜学绘，王超. 一种面向应用系统的强制访问控制模型[J]. 计算机工程与应用, 2010, 46(9): 107-110.
[3]	申军伟¹，杨晓元^1，2，梁中银¹，陈海滨¹. 一种新的无证书代理签名方案的分析与改进[J]. 计算机工程与应用, 2010, 46(8): 96-98.
[4]	安小明¹，王小明^1，2，王巧玲¹. 具有时空约束的角色访问控制模型[J]. 计算机工程与应用, 2010, 46(7): 89-92.
[5]	李洁，吴振强，于璐，孙鹏. 增强的无线TNC证实模型及协议设计[J]. 计算机工程与应用, 2010, 46(7): 121-124.
[6]	朱英敏¹，黄生叶¹，冯穗力²，叶梧². IEEE802.16e标准安全机制的改进[J]. 计算机工程与应用, 2010, 46(6): 103-106.
[7]	王世峰¹，张龙军²，杨晓元^1，3. 一种基于零知识证明的互联网密钥交换协议[J]. 计算机工程与应用, 2010, 46(5): 73-75.
[8]	张弢，慕德俊，任帅，姚磊. 一种基于风险矩阵法的信息安全风险评估模型[J]. 计算机工程与应用, 2010, 46(5): 93-95.
[9]	刘连浩，温从剑. AES的差分－代数攻击[J]. 计算机工程与应用, 2010, 46(5): 111-113.
[10]	顾国生，战荫伟，侯文邦. 图像Contourlet域快速置乱算法[J]. 计算机工程与应用, 2010, 46(4): 15-17.
[11]	王涛，王立斌，马昌社. 通用高效RFID授权协议模型设计与实现[J]. 计算机工程与应用, 2010, 46(4): 72-75.
[12]	刘素楠^1，2，方志宏¹，李淑芝³. 采用混沌加密和重复码的复倒谱音频水印算法[J]. 计算机工程与应用, 2010, 46(4): 79-82.
[13]	李跃强. DCT域音频水印透明健壮算法[J]. 计算机工程与应用, 2010, 46(3): 84-86.
[14]	牟亚莉^1，2，曾浩³，姚洪². 基于角色任务的约束委托模型[J]. 计算机工程与应用, 2010, 46(3): 87-89.
[15]	严波涛，潘晓中，张昊，张天祥. 一种对改进图像LSB隐秘方法的重加密检测方案[J]. 计算机工程与应用, 2010, 46(2): 83-85.

SET协议模型的改进与SMV分析

Improvement of SET protocol model and formal analysis via SMV

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics