| SET协议模型的改进与SMV分析 |
| |
| 引用本文： | 鲁四美,张建林.SET协议模型的改进与SMV分析[J].计算机工程与应用,2010,46(8):113-116. |
| |
| 作者姓名： | 鲁四美 张建林 |
| |
| 作者单位： | 首都师范大学 信息工程学院，北京 100048 |
| |
| 基金项目： | 北京市教委科技计划(No.KM200510028016) |
| |
| 摘 要： | 在以Lu&Smolka对SET协议支付过程的简化模型为研究对象的情况下，进行形式化建模和有限状态机模型。同时应用CTL对相应的安全性质进行形式描述，并在网络环境被入侵者控制的假设下，利用SMV分析了协议的认证性、保密性和完整性，发现攻击并对该攻击所产生的影响进行了讨论。最后修改其协议模型对改进后的协议进行分析和检验，说明了SET协议独具特色的双重签名在整个协议运行中至关重要。
|
| 关 键 词： | 安全电子交易 符号模型验证器 符号模型 模型检测 |
| 收稿时间： | 2008-9-12 |
| 修稿时间： | 2008-12-8
|
Improvement of SET protocol model and formal analysis via SMV |
| |
| 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. |
| |
| Authors: | LU Si-mei ZHANG Jian-lin |
| |
| Affiliation: | College of Information Engineering，Capital Normal University，Beijing 100048，China |
| |
| 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 ... |
| |
| Keywords: | Secure Electronic Transaction(SET) Symbolic Model Verifier(SMV) symbolic model model checking |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《计算机工程与应用》浏览原始摘要信息 |
|
点击此处可从《计算机工程与应用》下载全文 |
