|
|||||
|
|
| 基于Spin的安全协议形式化验证技术 | |
| 引用本文： | 冉俊轶,吴尽昭. 基于Spin的安全协议形式化验证技术[J]. 计算机应用, 2014, 0(Z2): 85-90 |
| 作者姓名： | 冉俊轶 吴尽昭 |
| 作者单位： | 1. 中国科学院 成都计算机应用研究所，成都610041; 中国科学院大学，北京100049 2. 广西混杂计算与集成电路设计分析重点实验室 广西民族大学，南宁530000; 北京交通大学 计算机与信息技术学院，北京100044; 中国科学院大学，北京100049 |
| 基金项目： | 国家自然科学基金资助项目(11371003)；广西自然科学基金资助项目(2011GXNSFA018154，2012GXNSFGA060003)；广西区主席科技资金资助项目(10169-1)；广西教育厅科研资助项目(201012MS274)。 |
| 摘 要： | 针对安全协议的形式化验证问题，运用模型检测方法，以一种改进的入侵者Promela语义模型，对双方密钥分配中心协议进行Spin模型检测，验证发现其不满足线性时序逻辑（ LTL）公式描述的安全性，得到了原协议的安全漏洞。针对该漏洞，提出了一种协议改进方案，并针对改进后的协议，给出新的Promela语义模型的建模方法。改进的入侵者模型建模方法比起原方法：模型检测过程中的存储状态数减少，使模型复杂度降低约40'；迁移状态数减少，使验证效率提升约44'。 |
| 关 键 词： | 安全协议 形式化验证 Spin模型检测 Promela语义模型 LTL公式 密钥分配中心协议 |
Formal verification technologis of security protocol based on Spin |
|
| RAN Junyi , WU Jinzhao. Formal verification technologis of security protocol based on Spin[J]. Journal of Computer Applications, 2014, 0(Z2): 85-90 | |
| Authors: | RAN Junyi WU Jinzhao |
| Abstract: | |
| Keywords: | security protocol formal verification Spin model checking Promela semantic model Linear Timing Logic ( LTL) formula key contribution center protocol |
| 本文献已被 CNKI 万方数据 等数据库收录！ | |