第36卷第2期Vol.36No.2计算机工程ComputerEngineering•安全技术•文章编号：1000-3428(2010)02-0144—03文献标识码：A中图分类号：TP309TA4SP的认证性扩展朱文也，祝跃飞，刘楠，陈晨(信息工程大学信息工程学院，郑州450002)摘要：认证性是安全协议检测的重要特性之一，但TA4SP自动协议证明器无法对安全协议的认证性进行检测。针对该问题，提出一•种TA4SP的认证性检测方法。该方法基于对TA4SP设计原理的分析，采用分层认证思想，实现对其认证性的理论扩展，其结构淸晰、易于形式化。实例表明，通过该方法改进后的TA4SP能有效检测安全协议的认证性。关键词：TA4SP系统；项重写系统；树自动机；认证性CertificationExpansionofTA4SPZHUWen-ye,ZHUYue-fei,LIUNail,CHENChen(CollegeofInformationEngineering.InformationEngineeringUniversity.Zhengzhou450002)[Abstract]Certificationisimportantpropertiesofsecurilyprotocols,butTreeAutomatabasedonAutomaticApproximationfortheAnalysisofSecurityProtocols(TA4SP)cannotdetectcertificationofsecurityprotocols.Tosolovetheaboveproblem,thispaperproposesacertificationdetectionmethodforTA4SP.BasedontheanalysisofTA4SP,themethodintroducesthehierarchicalcertification,andachievestheexpandingofcertificationlorTA4SP.Themethodisaclearstructureandeasytofoamal.Examplesshowthattheadoplionofimpovedmethodcandetectcertificationofsecurityprotocolseffectively.[Keywords]TA4SPsystem;TermRewritingSystem(TRS);treeautomata;certification1概述安全协议的形式化方法大致可分为3类：形式逻辑方法,模型检测方法和定理证明方法。其中，定理证明方法由于其能证明无限主体和无限会话下协议的安全，而成为研究热点。然而这种方法需要用户参与的程度高，不易实现自动化分析。Y.Boichut,P.CHeam和O.Kouchnarenko于2005年设计出了基于树自动机和项重写系统(TermRewritingSystems,TRS)的自动协议证明器TA4SP,它既能处理无限主体和无限会话，乂能实现高效的自动化分析，但TA4SP只考虑了协议的秘密性，对认证性没有检测。本文基于对TA4SP设计原理的分析，提出了一种对其进行认证性扩展的方法，并通过相应的实例，验证了该方法的有效性。2TA4SP的简单介绍2.1预备知识项垂写系统⑴实质上是一个满足某些性质的规则集，首先记F是一个有限符号集，X是变量可数集，则T(F,X)称为项集，□")称为基础项集(不含变量的项集)。对项teT(F,X),对它的一个位置p,若t(p)eF,则称为操作符位這，记为PosF(t)oPe⑴满足以下性质：(1)Pos⑴非空。(2)对每个pePos(t),若f(p)eFn,n^\,则Po$(f)}={1,2,•••,”}o(3)VpePos(t),若t(p)wXu",则［j\pjGPos(f)}=0o中的每个元素称为位置。定义1T(F,X)上的项重写系统R(简称TRS)是重写规则/->/■的有限集，其中，l,rwT(F,X),l^X,且Vai⑴二Val(t)o树自动机理论⑵近年来在自动理论证明方面应用广泛，相对普通的字自动机(wordautomata),它的优势在于可以处理比较复杂的树状结构，比如本文中所用到的项。定义2自底向上的不确定有限树自动机4是一个四元组(20,4尸)，其中，Qf^Q是终结状态集；Q是有限状态集；F是有限符号集；4是形如ciq的转移集，cwT(FoQ),qwQ。本文所提的树自动机都是指自底向上的不确定有限树自动机。树自动机接受的语言是基础项集。正规的树语言是指,存在一个树自动机，使得它接受的语言刚好就是这个语言集。2.2TA4SP方法介绍TA4SP(TreeAutomatabasedonAutomaticApproximationfortheAnalysisofSecurityProtocols)是AVISPA下的一个安全协议分析器，它采用DY・攻击者模型，其主要思想是试图找到一个树自动机，使得它接受的语言集刚好就足攻击者知识集，然而在无限主体、无限会话的条件下，攻击者知识通常不是正规的⑶，即无法用一个恰当的树自动机使得它接受的语言刚好是攻击者知识集。因此，TA4SP通过生成一系列的树自动机来逐渐逼近攻击者知识的精确集，可分为以下3个步骤：基金项目：国家“863”计划基金资助项目(2007AA01471)作者简介：朱文也(1984-),女，硕士硏究生，主研方向：信息安全;祝跃飞...