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

Simplified SET Protocol Based on Small System Theory

作　　者：罗敏[1,2] 方琳[3] 施炜利 

机构地区：[1]江西省计算技术研究所,江西南昌330003 [2]江西省软件工程技术研究中心,江西南昌330003 [3]江西警察学院刑事科学系,江西南昌330100

出　　处：《计算机与现代化》2014年第12期97-102,共6页Computer and Modernization

基　　金：江西省科技计划项目(20123BBE50106)

摘　　要：基于Lu&Smolka的SET协议支付过程简化模型,在小系统理论的基础上,运用Promela语言对协议进行形式化建模,采用线性时态逻辑LTL公式对协议的认证性进行形式化描述。在网络环境被入侵者控制的假设下,运用SPIN发现攻击;采用atomic和Bit-state hashing等优化策略,降低模型检测的复杂性,提高验证效率;最后针对协议存在的漏洞提出协议改进方案。In this paper , we use the Promela language to model formally for the simplified SET payment protocol proposed by Lu＆amp;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 im-prove the efficiency of verification .Finally, we put forward the improvement solution for the existing vulnerabilities of the SET protocol.

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

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