基于Spin的安全协议形式化验证技术  

Formal verification technologis of security protocol based on Spin

作　　者：冉俊轶 吴尽昭[3,4,2] 

机构地区：[1]中国科学院成都计算机应用研究所,成都610041 [2]中国科学院大学,北京100049 [3]广西混杂计算与集成电路设计分析重点实验室(广西民族大学),南宁530000 [4]北京交通大学计算机与信息技术学院,北京100044

出　　处：《计算机应用》2014年第A02期85-90,共6页journal of Computer Applications

基　　金：国家自然科学基金资助项目(11371003);广西自然科学基金资助项目(2011GXNSFA018154;2012GXNSFGA060003);广西区主席科技资金资助项目(10169-1);广西教育厅科研资助项目(201012MS274)

摘　　要：针对安全协议的形式化验证问题,运用模型检测方法,以一种改进的入侵者Promela语义模型,对双方密钥分配中心协议进行Spin模型检测,验证发现其不满足线性时序逻辑(LTL)公式描述的安全性,得到了原协议的安全漏洞。针对该漏洞,提出了一种协议改进方案,并针对改进后的协议,给出新的Promela语义模型的建模方法。改进的入侵者模型建模方法比起原方法:模型检测过程中的存储状态数减少,使模型复杂度降低约40%;迁移状态数减少,使验证效率提升约44%。Aiming at the formal verification problem in security protocols, an improved Promela semantic intruder model was used to complete the model checking for key distribution center protocol, to find that it does＇t meet the security property described by LTL（ Linear Temporal Logic） formula, and to get a protocol vulnerability. An improvement program against vulnerability was proposed. A new Promela semantic modeling was put forward for the improved protocol. The improved intruder modeling method reduces the number of states stored in the model checking, thus the model complexity reduces about40%; and reduces the number of transiations, thus the verification efficiency increases about 44%.

关 键 词：安全协议 形式化验证 Spin模型检测 Promela语义模型 LTL公式 密钥分配中心协议 

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构]