一种改进的基于认证测试的形式化分析方法  

An Improved Formal Analysis Method Based on Authentication Tests

作　　者：姚萌萌[1] 朱正超[1] 刘明达[1] YAO Mengmeng;ZHU Zhengchao;LIU Mingda(Jiangnan Institute of Computing Technology,Wuxi Jiangsu 214063,China)

机构地区：[1]江南计算技术研究所,江苏无锡214063

出　　处：《信息网络安全》2019年第1期27-33,共7页Netinfo Security

基　　金：国家自然科学基金[91430214;6732018];核高基重大专项[2017ZX01028101]

摘　　要：近年来,认证测试定理得到了改进,并应用于各种安全协议的分析。但是这些改进定理在应用范围和准确性方面存在一定的缺陷。针对这些缺陷,文章提出了一种改进的输入测试定理及加密测试定理,并给出了改进定理的证明。通过分析认证测试中常规节点的判定、证明过程中的错误、参数一致性证明过程中的不准确性和错误,指出了认证测试在使用过程中的缺陷。基于这些缺陷,文章提出了一种改进的基于认证测试的形式化分析方法——递归测试,并通过该方法证明了BAN-Yahalom协议。分析结果表明,该方法扩大了认证测试使用范围,且可以有效地、准确地分析安全协议。In recent years,authentication tests has been improved and applied to the analysis of various security protocols.However,these improvement theorems also have certain defects in terms of application scope and accuracy.In response to these defects,in this paper,improved incoming test theorem and encryption test theorem are proposed,and proof of the improvement theorem is given.This paper points out the defects of the authentication test in use by analyzing the judgment of the normal nodes in the authentication test,the errors in the proof process,and the inaccuracies and errors in the process of parameter consistency verification.Based on these defects,an improved formal analysis method recursion test is proposed.This method is used to prove BAN-Yahalom protocol,the result proves this method has expanded the scope of the use of authentication tests,and can analyze the security protocol effectively,accurately.

关 键 词：串空间 认证测试 形式化分析方法 安全协议 

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