基于StrandSpace模型的安全协议形式化分析研究.pdf

西南交通大学

硕士学位论文

基于StrandSpace模型的安全协议形式化分析研究

姓名：程娜

申请学位级别：硕士

专业：密码学

指导教师：何大可

20060501
摘要随着网络的普及以及电子商务和电子政务的蓬勃兴起，网络安全问题曰显突出。安全协议，作为解决安全问题最行之有效的方法，也就变得越来越重要。然而，在复杂的网络环境中，要确保安全协议的正确睦却是件很难解决的问题，它已成为一项重要的研究课题。20年来，为了应对这一挑战，科学家们在安全协议分析这一领域投入了大量的精力。在已有的理论和方法中，本文深入研究了s圩andspace理论，并用该理论分析了若干协议：3．Isl支付协议。将S订∞dspace理论运用到电子商务协议公平性的分析space模型；公平性；代理多重签名西南交通大学硕士研究生学位论文形式化分析方法的成果较为突出。在各种形式化分析方法中，被普遍认为最有前景的晶新研究成果是由Fabrega，Herzog和Gunm孤三人提出的S汀andSpace模型。它充分吸收了前人的研究成果，使用一种节点问存在因果关系的有向图来表示协议中主体、入侵者的动作序列，利用证明的方法推导协议的正确性，可以防止状态空间爆炸。它是一种直观、简洁、严格、有效的形式化分析方法。l‘Yahalom协议。建立了Yahalom协议的strandspace模型，并进行了深入的讨论；2．一种传输模型的认证协议。建立了该协议的Strandspace模型，通过分析，发现协议存在漏洞，并构造出了一种攻击方法，最后针对漏洞对协议进行了改进；中，得到了与其他分析方法一致的结果。此外，本文在基础理论部分对代理多重签名进行了研究，提出了一种增强的代理多重签名方案。关键词：安全协议；形式化分析；strand
ofmalompa脚ems岫eAbstractmechods，fbmalf0皿al肌alysis西南交通大学硕士研究生学位论文第1I页ne研。止肌dd嘶ngof蜘messWithimport肌cesubjectdimcultyModel(SSM)broughtfomlalfomlerrelationshipme锄8SSM，缸d1．Y她alo。pmtoc01auth％ncationwithdropper触dimpmvem髓t；we印plymeSSMtothe蛆alysisprcs叨tIntemetmostla唱e．Itintrud盯of出emeValidityanal”esSSMSSM，wefindmakepopulanzaIionofapplications，securlIyissuesbecomingmorea11dimportantAccordiⅡgly’security．protocol，theeffectivewaysoIvesecurityisBues，isBut“iseasyworkthevaliditysecufnyprotoc01insophisticatednelworkenvironmenl，whichhasbecomeimponantresearchGTeateffbrtshavebeenmadebyscientistsme。Itllischallenge20years，whichshows'[1leprotoc01sanalysisAmonga11eXistmgtheoriesandaIlalysisisoutstalldingTheupdaIedfhlit—StrandspaceforwardFabrega，HerzogaIldGultnlanbe8tprospectamongvadetiesa11alysismemodsfullyabsorbsre8earchingresultskindordergraphbet、Veenitsnodesexi“ingcasualdemonstrateactionsequencemainbodydeducecerti6cation．npreventbur8tingpractical，imuniVest打ctforsecu打typmtoc01．ThispaperdocsfIlrthersnldythennurnbefsprotocolsbaseditf01lows：EstablishprotocoIandconductfLlItllerdjscussion；2．A妯Ildbas亡dtraIlsmissionmodelnsanewattackonthisprotocol3．ISlprOtOc01ofE_businessprotocol-AdditioⅡally，westudymulti—si911amreschemebasictheorya士1dstrengthenedproxymulti—si