摘要
为了能高效地利用模型检测技术对安全协议进行分析与验证,提高工作效率,提出了一种适用范围广,自动化程度及验证效率均较高的建模算法。开发了一个基于该建模算法"网络安全协议验证模型生成系统",该系统可高效地对安全协议进行分析与验证,系统在对攻击者建模时采用偏序规约、语法重定序及类型检查等优化策略以提高验证效率,有效地缓解了模型检测过程中的状态爆炸问题。
Aiming at a more efficient analysis and verification of the security protocol with the model checking technology,this paper proposes a more efficient modeling algorithm with a wider applicability and higher level of automation.Based on this modeling algorithm,the“Generative System of Network Security Protocol Verification Model” is developed.This system can efficiently analyze and verify the security protocol.During the modeling of the intruder,the system improves the efficiency of verification and solves the problem of state explosion by using such optimization strategies as the partial order reduction,syntax reordering and type checking.
出处
《计算机工程与应用》
CSCD
北大核心
2010年第2期79-82,共4页
Computer Engineering and Applications
基金
江西省自然科学基金(No.0411041
No.0611057
No.2007GZS1884)
2006年江西省科技攻关计划项目
2005年江西省教育厅科技计划项目(No.200543)
2007年南昌产业化科技项目~~
关键词
安全协议
模型检测
简单进程元语言解释器
状态爆炸
security protocol
model checking
Simple PROMELA Interprete（rSPIN）
state explosion
