基于小系统理论的简化SET协议

doi:10.3969/j.issn.1006-2475.2014.12.021

计算机与现代化

基于小系统理论的简化SET协议

（1.江西省计算技术研究所，江西南昌 330003;2.江西省软件工程技术研究中心，江西南昌 330003;3.江西警察学院刑事科学系，江西南昌 330100）

收稿日期:2014-09-20 出版日期:2014-12-22 发布日期:2014-12-22
作者简介:罗敏（1963-），女，江西抚州人，江西省计算技术研究所副研究员，研究方向：信息安全技术; 方琳（1986-），女，江西南昌人，江西警察学院助教，硕士研究生，研究方向：软件工程及文件信息检测; 施炜利（1983-），女，浙江缙云人，工程师，本科，研究方向：信息安全技术。
基金资助:
江西省科技计划项目(20123BBE50106)

Simplified SET Protocol Based on Small System Theory

(1. Jiangxi Institute of Computing Technology, Nanchang 330003, China;
2. Software Engineering and Technical Research Center of Jiangxi Province, Nanchang 330003, China;
3. Department of Criminal Science and Technology, Jiangxi Police College, Nanchang 330100, China)

Received:2014-09-20 Online:2014-12-22 Published:2014-12-22

摘要/Abstract

摘要： 基于Lu & Smolka的SET协议支付过程简化模型，在小系统理论的基础上，运用Promela语言对协议进行形式化建模，采用线性时态逻辑LTL公式对协议的认证性进行形式化描述。在网络环境被入侵者控制的假设下，运用SPIN发现攻击；采用atomic和Bit-state hashing等优化策略，降低模型检测的复杂性，提高验证效率；最后针对协议存在的漏洞提出协议改进方案。

关键词: 小系统理论, SET协议, 模型检测, SPIN, 认证性

Abstract: In this paper, we use the Promela language to model formally for the simplified SET payment protocol proposed by Lu & Smolka based on small system theory, and use LTL (linear temporal logic) formulas to describe the authentication property of the protocol. Under the hypothesis of the network environment being controlled by the intruder, we use SPIN to find the attacks, and adopt optimization strategies of atomic and Bit-state hashing technology to reduce the complexity of model checking and improve the efficiency of verification. Finally, we put forward the improvement solution for the existing vulnerabilities of the SET protocol.

Key words: small system theory, SET protocol, model checking, SPIN, authentication

中图分类号:

TP393

罗敏1,2，方琳3，施炜利1,2. 基于小系统理论的简化SET协议[J]. 计算机与现代化, doi: 10.3969/j.issn.1006-2475.2014.12.021.

LUO Min1,2, FANG Lin3, SHI Wei-li1,2. Simplified SET Protocol Based on Small System Theory[J]. Computer and Modernization, doi: 10.3969/j.issn.1006-2475.2014.12.021.

参考文献

[1] 谢晓尧. 电子商务网络协议的形式化分析理论与应用[M]. 北京:科学出版社, 2008.

[2] 肖茵茵,苏开乐. 电子商务支付协议认证性的SVO逻辑验证[J]. 计算机工程与应用, 2014,50(8):6-10.

[3] Lu Shiyong, Smolka S A. Model checking the secure electronic transaction (SET) protocol[C]// Proceedings of the 7th International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems. 1999:358-365.

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

[5] 温炽亮. 小额交易中SET协议的优化及SPIN验证的研究[J]. 计算机与现代化, 2011(7):201-206.

[6] 化希耀,苏博妮,陈立平,等. 模型检测技术研究综述[J]. 塔里木大学学报, 2013,25(4):119-124.

[7] 李翠翠. 基于SPIN模型检测的电子商务协议分析与验证[D]. 上海:华东理工大学, 2012.

[8] 肖美华,薛锦云. 基于SPIN/Promela的并发系统验证[J]. 计算机科学, 2004,31(8):201-203.

[9] Holzmann G J. The SPIN Model Checker: Primer and Reference Manual[M]. Addison-Wesley, 2003.

[10] Bella G, Massacci F, Paulson L. Verifying the SET registration protocols[J]. IEEE Journal on Selected Areas in Communications, 2003,21(1):77-87.

[11] Ruiz M C, Cazorla D, Cuartero F, et al. Analysis of the SET E-commerce protocol using a true concurrency process algebra[C]// Proceedings of the 2006 ACM Symposium on Applied Computing. 2006:879-886.

[12] 司亚利,刘文远,卢贝. 颜色Petri网的电子商务协议攻击分析方法[J]. 计算机工程与设计, 2014,35(3):814-818.

[13] 薛锐,冯登国. 安全协议的形式化分析技术与方法[J]. 计算机学报, 2006,29(1):1-20.

[14] 贺志宏,曾庆凯. 基于SPIN的LTL属性分解方法研究[J]. 计算机应用与软件, 2014,31(7):43-46.

[15] 黎升洪,冯艳清. 第三方支付的基于SPIN的形式化分析[J]. 计算机时代, 2008(12):23-25.

[16] 张若岩,刘晓霞,张宏. SET协议形式化模型的建立和安全性分析[J]. 计算机应用与软件, 2009,26(5):81-84.

[17] 高悦翔. 电子商务安全协议的设计与形式化分析[D]. 成都:西南交通大学, 2013.

基于小系统理论的简化SET协议

Simplified SET Protocol Based on Small System Theory

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 11

编辑推荐

Metrics

本文评价

[1]	管金平, 杨晋吉, 杨成龙. 基于概率模型的Raft协议形式化验证[J]. 计算机与现代化, 2023, 0(09): 77-81.
[2]	刘林武，张弛. 模型检测中虚假反例检测方法[J]. 计算机与现代化, 2017, 0(9): 29-32,44.
[3]	刘维维，庄毅，李蜜. 一种嵌入式软件可靠性建模与评估方法[J]. 计算机与现代化, 2017, 0(8): 78-.
[4]	毛良文1，徐亮2,3. 基于SMT的PTACTL限界模型检测方法[J]. 计算机与现代化, 2016, 0(3): 41-45.
[5]	黄鸣宇,石玉峰. 基于χChek的软件产品线多值模型检测方法[J]. 计算机与现代化, 2014, 0(8): 87-90.
[6]	徐小丽. 基于SPIN的系统建模研究[J]. 计算机与现代化, 2012, 1(9): 209-214.
[7]	陈志辉. 基于时间自动机的信息物理融合系统建模与验证[J]. 计算机与现代化, 2012, 1(10): 125-130,.
[8]	温炽亮. 小额交易中SET协议的优化及SPIN验证的研究[J]. 计算机与现代化, 2011, 7(7): 201-206.
[9]	罗清胜. 一种基于Büchi自动机的LTL程序模型检测方法[J]. 计算机与现代化, 2010, 1(8): 58-61.
[10]	舒良春饶俊肖美华尹传文. 基于Promela的UML建模方法及其应用[J]. 计算机与现代化, 2010, 1(02): 101-104.
[11]	黎升洪;冯艳清. SPIN语义引擎执行方式研究[J]. 计算机与现代化, 2009, 1(11): 112-115.