摘要
在以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.
出处
《计算机工程与应用》
CSCD
北大核心
2010年第8期113-116,共4页
Computer Engineering and Applications
基金
北京市教委科技计划(No.KM200510028016)
关键词
安全电子交易
符号模型验证器
符号模型
模型检测
Secure Electronic Transaction（SET）
Symbolic Model Verifier（SMV）
symbolic model
model checking
