一种新的认证协议自动验证方法  

A Novel Automatic Verifying Method for Authentication Protocols

作　　者：肖跃雷 朱志祥 张勇 

机构地区：[1]西安邮电大学,物联网与两化融合研究院

出　　处：《微型电脑应用》2015年第8期4-6,共3页Microcomputer Applications

基　　金：国家自然科学基金(61402367);陕西省信息化技术研究项目(2013-008);西安邮电大学青年教师科研基金项目(401-1201)

摘　　要：为了实现对认证协议的自动验证,首先,通过对认证协议的协议主体行为分析,给出了驱动模型(Driving Module,DM)的定义。然后,根据串空间模型中的常规者串和攻击者串分别构建了常规者DM和攻击者DM。最后,提出了基于常规者DM和攻击者DM的自动验证算法。实例分析和定理证明表明,该算法的搜索过程不仅是全面和正确的,而且能有效地避免状态空间爆炸问题。To implement automatic verifying for authcntion protocols,the definition of Driving Module(DM) is given by analyzing the action of protocols participants of authentication protocols.Then,regular and penetrator DMs are formed respectively according to regular and penetrator strands in the Strand Space Model(SSM).Finally,an automatic verifying algorithm is proposed based on these regular and penctrator DMs.Case analysis and theorem proofs show that the scarch process of this algorithm is all-sided and correct,and can avoid the state space explosion problem.

关 键 词：自动验证 驱动模型 串空间模型 认证协议 

分 类 号：TP393.08[自动化与计算机技术—计算机应用技术]