资源描述：
《公钥加密体制自动化安全性证明方法研究new》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。
1、第11卷第4期信息工程大学学报Vol11No42010年8月JournalofInformationEngineeringUniversityAug2010公钥加密体制自动化安全性证明方法研究陈楠,李安乐,祝跃飞,顾纯祥(信息工程大学信息工程学院,河南郑州450002)摘要:可证明安全是目前分析密码协议安全性的一种重要方法,但是手工证明的难度较大,正确性也难以保证。利用计算机技术实现可证明安全性的自动化分析是目前的一个研究热点。文章在前人工作的基础上,设计了一个适用于更多密码协议的安全性证明的自动化证明工具。着重介绍了利用高级描述语言来描述的输入文件即初始攻
2、击游戏的结构,并以带Hash的ElGamal加密体制为例,利用证明工具,实现了其安全性的自动化证明。关键词:可证明安全;自动化;攻击游戏;ElGamal加密体制中图分类号:TN918.1文献标识码:A文章编号:1671-0673(2010)04-0472-05ResearchonAutomatedSecurityProofofPublicKeyEncryptionSchemeCHENNan,LIAnle,ZHUYuefe,iGUChunxiang(InstituteofInformationEngineering,InformationEngineeri
3、ngUniversity,Zhengzhou450002,China)Abstract:Provablesecurityisoneofimportanttechniquesforanalyzingthesecurityofcryptographicprotocols,whilemanualproofisdifficultandhardtoestimate.Automaticproofwiththehelpofcomputersisahotspotnow.Thispaperdesignsatoolwhichcansatisfymuchmorecryptographic
4、protocolsfortheautomaticproo.fItalsointroducestheframeworkoftheinitialattackgameandgavesanexample.Byusingthepioposedtoo,lthesemanticsecurityofthehashedversionofElGamalencryptionschemeisproved.Keywords:provablesecurity;automatic;attackgame;ElGamalencryptionscheme对安全协议进行分析以检测其安全性是网络安全
5、领域的一个热点。可证明安全是目前分析协议安全[1]性的一种有效的方法。可证明安全性其实是一种规约的方法,它是在定义合适的安全目标和建立适当的敌手模型的前提下,证明协议的安全性。在安全性的规约证明中,若对体制构建中的任何组成没有任何假设,便将安全问题约化到难解的问题上,则称该体制是标准模型(standardmodel)下可证安全的。由于公钥密码体制本身的复杂性以及应用的广泛性,使得在标准模型下证明安全性极其困难。为了方便证明,在安全性的定义模型中引入谕示,以此为基础证明体制的安全性,然后用相应的实例替换谕示。文献[2]于1993年提出随机谕示模型(random[3]o
6、raclemodel)。另一个较为受关注的安全性证明模型是由Nechaev首次提出的一般群模型(genericgroupmodel)。还有一个在密码中应用的黑盒域模型(blackboxfield),其主要讨论了数学难题的复杂度。不同安全性证明模型的引入大大拓展了可证明安全方法的适用范围,国内外学者纷纷将可证明安全作为评估密码协议安全性的主要依据,一大批快捷有效且可证明安全的密码协议被相继提出。但是,从当前的研究现状看,一个具体协议的安全性证明通常仍需要较多的经验和技巧,手工证明的正确性也难以保证。能否利用计算机技术实现可证明安全性的自动化分析,成为密码协议设计和安全
7、性分析领域的一个殛待解决的课题。收稿日期:2010-03-01;修回日期:2010-04-28基金项目:国家863计划资助项目(2007AA01Z471)作者简介:陈楠(1984-),女,硕士生,主要研究方向为密码学与网络信息安全。第4期陈楠等:公钥加密体制自动化安全性证明方法研究4732004年,文献[4]详细描述了如何使用游戏序列来组织安全性证明过程。同年,Barthe等利用交互[5][6]式定理证明器Coq设计了一个自动化证明工具。2005年,Halevi首次提出GameBased自动化证明的思想。文献[7]对基于Coq
