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

Improvement of SET protocol model and formal analysis via SMV

作　　者：鲁四美[1] 张建林[1] 

机构地区：[1]首都师范大学信息工程学院,北京100048

出　　处：《计算机工程与应用》2010年第8期113-116,共4页Computer Engineering and Applications

基　　金：北京市教委科技计划(No.KM200510028016)

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