密码协议书稿中文第9章

4章中提出的新鲜性原则已经被用来有效地分析密码协议的安全性，这是因为新鲜有效性[1-4]7章中，已经提出了基于可信任新鲜性的安全性分析的模态逻辑，即信任本章将给出一个基于新鲜性原则的协议安全性逻辑分析工具（4章SPEARII框架中的一些概念[5,6]。SPEARI，全称是“安全协议工程和分析资源”[8]J.P.Bekmann，P.GoedeA.Hutchison1997年开发，目的是帮助密码协议的设计和安全性分析。SPEARI的两个主要目标是使协议设计安全高效，并支持协议源代码的生成。SPEARI为密码协议的开发者提供用BAN逻辑进行协议的安全性分析[9]。SPEARIIII”[6]SPEARI基础上的协议工程工具。SPEARII工具的目的是使密码协议工程分析变得更容易，它通过为用户提供适GNYGNYGNY语句快速、准确和语法下细化一个协议的消息、初始假设和安全目标。在此之后，GNY规则集合被引入并在GNY为一个GYNGER分析者提供友好的用户界面。SPEAEII提供了基于图形的协议分析FDRFailuresDivergencesRefinement)[10–12]CSP[13]基础上的状性是否被满足。1995Lowe使用自动模型检验工具FDR成功发现了著名的次被发现有漏洞[10,11]。在FDR中，协议中的主体（甚至可能是一个攻击者）被看作是并发CSP进程，而攻击者进程可以执行多种攻击操作(窃听，冒充，重放等等)。协议的安全性由主体事件的序列来刻划，而FDR工具则被用来检验协议的主体各事件序列是否满足安全性质。CSP的模型检验工具在分析Needham-Schroeder公钥认证协议中获得了成功。NRL协议分析器[14]MeadowsProlog的模型检验工具，其中“NRL”是美国海军研究实验室的缩写。NRLDolev-Yao通信威胁模型[15]Dolev-YaoDolev-Yao模型中，攻击者的计算能力是多项式有界的，在协议执行之NRL协议分析器已被用来分析许多认证协议，并且成功发现或证明其中一些协议已知Needham-Schroeder公钥认证协议[16]（MeadowsNRL协议分析器进行的协议分析和使用文献[11]FDR的协议安全性分析进行了一个比较络密钥交换协议（IKE2”交换协议的签名中发现了反射攻击）[17,18]和安全Murφ是一种协议验证工具[20]，它已经成功的应用在一些工业协议上，尤其是在多处理器缓Murφ语言是一种描述有限状态异步并发系统的高级语言，而MurφMurφ程序C++MurφMurφ语言描述出来，然后用所需Murφ中表示，即布尔条件，在每一个达到的状态中都必须是正确的。Murφ系统将自动检查模型的所有可达状态是Murφ模型是不确但不是一般协议的正确性。如果一个包含一些违规不变量的状态是可达的，Murφ就能够给出对这个错误的追踪，一个从起始状态到出现问题状态的状态序列。Murφ证明了对一些已Needham-Schroeder公钥协议，TMNKerberosv5的一个简单版本是存在读写器JonathanMillen，SidneyClarkSherylFreedman1985Prolog能的攻击中如何能够获得数据项。读写器和它的相关的图形界面用LM-Prolog在一个是用来在多种应用领域生成特殊证明目标的通用证明工具。SyMP的核心工具是一个连接着值得注意的是，SyMP证明器并没有内置的模型检验器。SyMP有两套证明系统：默认的证明系统和Athena。默认的证明系统实现了一个广义的Athena证明系统用于密码协议的安全性验证，利用串空间[26]作为协议表示的基础，基DSongAthena[27]技术构建框架。Athena程序的文件后缀名是“.ath”。框架中的CAPSL(CommonAuthenticationProtocolSpecificationLanguage)，即通用认证协议描述语CAPSL中使用分析者提供。CAPSL环境包括了对这类信息的详细描述。环境描述（例如类型规格）与协议的定义是分开的。环境描述的内容和说明取决于分析工具。然而，CAPSL中不提供语法、关键字和组织，所以不同的工具都能够采用CAPSL分析器。名字主体和其他常量的声明可CAPSL环境中，协议会话也能被定义。CAPSL环境允许声明多个协议会话实例，BMFBMF（VisualBMF，BMF分析引擎（BMFEngineBMBMFEngineBMFBMFBMFBMFBMFVisual操作。BMFBMFBMFBMFBMFBMFVisualBMFBMF分析工具的一个用户界面友好的初始信息输入接口，输入组件包入协议的安全目标配置，如UA-安全，MA-安全，UK-安全和MK-安全。BMF分析引擎支持信任多集中术语、初始假设、安全目标、推理规则和公理的形式化BMF规则引擎，是信任多集扩充规则的用户输入界面。基于新鲜性原则，信任多集形BMFBMF失指出直接构造攻击的结构。因此，BMF攻击引擎支持信任多集形式化方法中关于攻击的程的复杂和乏味，为研究者提供一个用户界面友好、高效和具有可用性的环境。BMF分析BMFBMF分析工具中可视的BMF部分，BMF分析引擎部分和BMF分析结果显示部分的部分功能。信任类(4个子类：主体的信任子类、新鲜性标识符的信任子类、密钥的信任子类、主体知道某密钥的信任子类)等，参见图9.2。视化的输入界面以及分析结果的显示，参见图9.3。户而独立变化。例如，关联性规则类(6个子类：双方共享长期密钥子类、与可信第三BMF2[30]PrologProlog作为一种实现语言具有简单、可靠的特点。BMF2与SPEARII框架[7]GYNGER类似。BMF分析引擎（BMFGER）和结果显示界面（BMF结果显示SPEARII中的GNYGYNGERPrologBMFGER也采用前向链推导技术，通过对初BMFBMF的结果显以Prolog风格的信任多集形式化语句保存。信任多集形式化语句采用树形结构来表示，与将要分析的协议有关的消息和初始假设采用fact/3谓词的形式来表示，而协议安全目标用goal/2谓词的形式来表示。对于每个成功的安全目标，BMF结果显示部分将Prolog风格表示的信任多集分析结果，参见图9.4和图9.5。图 BMF分析工具2用户界图 BMF分析工具2分析结BMF分析工具的焦点是提供一个用户易用，有效且强大的工作环境，它基于可信任新9.2.22BMF分析工2BMFPrologBMF分析引擎，基于面向对象的方法使用Java源代码开发可视的BMFBMF结果显示。下最流行的人工智能语言之一，有许多免费的和商业的开发工具可用。Prolog编程逻辑用关系表示BMF，代表事实和规则，分析是在这些关系上运行一个查询而开始的。Prolog很适Java是一种面向对象的技术，使用它的目的是方便源代码的扩展和理解。Java在开发和调试用户易用界面（BMFBMF结果显示等）时具有明确、方便等优点。BMFGNY进行安全性分析，进而实现分析引擎，并在SPEARIIBMF分析工具在结构和安BMFProlog风格的BMF语法，通过可视的BMF界面指定协议的消息、初始假设和协议安全目标。随后基于PrologBMF规则在分析中被导入并使用，前向链推导引擎能够由初始假设集合、消息步BMF信任。指定的安全目标若获得成功，BMF分析工具就会生成一个英语语义风格的证明序列并显示给研究人员。这种BMF分析工具是可扩展的，它允许对协议进行扩展的安全性分析以满足将来的需要，因为推理规则库是独立于BMF分析工具存储的。出于简洁考虑，BMF分析工具中涉及的概念下面只进行简单介绍。有兴趣的读者，请假设必须以fact/3谓词形式在Prolog文件中进行说明。包括理想化的协议消息、初始假设，术语和中间结论。最后一个参数Reason(PremiseList，Rule)fact/3PremiseListfact/3子句所使用的其他fact/3Rulefact/3的分析StatementPremiseListRule将是‘Term’([],‘和分别表示主体‘IdentityStepStatement，整数‘Step’表示fact/3Index升序插入到事实getMaxFactIndex/1fact/3的索引为了执行一个基于信任多集形式化方法的协议安全性分析，设计者必须知道什么是所fact/3，协议的安全目标goal/2谓词来表示，并存储在目标库中。goal/2谓Indexgoal/2Statement表示预期的安全性目标（信任多集中的安全属性，包括主体的信任和新鲜性标识符的信任。信任用谓词BeliefBelief(Identity,3信任多集方法中的推理规则用谓词rules/0表示，存储于规则库中。对于每一个BMFrules/0谓词的实例，其中有些规则由于存在多个结论而需要更多实例。PrologaddedFacts原子也被插入到事实加入了Prolog数据库。A1(a){KN,N'K B( PP)B(<K1NK>)B(:{KN,N'K PiPji rulesfact(PremiseIndex1,told(P,encrypt(List,shared(K))),-),islist(List),length(List,LengthOfList),LengthOfList>1,fact(PremiseIndex2,believes(P,secret(shared(K))),-),fact(PremiseIndex3,believes(P,fresh(shared(K))),-),fact(PremiseIndex4,believes(P,associate(shared(K),P,Q)),-),listMemberIsFresh(P,List,PremiseIndex5),Conclusion=believes(P,bound(List)),not(fact(,Conclusion,-)),SPEARIIBMF环境使用树状结构表示BMF语句，并结合弹出菜单以便于人机交互，产生BMF信息的一个有意义的表示。BMFBMF语句由独立的树概念，尽管要能更有效地使用BMF分析工具他们最好能熟悉BMF逻辑。议将被翻译成图形显示，如图9.6所示：1.1.{A,3.2.{Na,NbBA图.9.6密码协议在BMF分析工具的表示这里，主体Alice用A表示，主体BobB表示。读密码读密码ABKAB是与通信参与主体A和B关联的.A(B)KAS(KBS是长期密A(B)知道KAS(KBSABKa1Kb1是保密9.7 是协议中应用的密码机制的标志：cipherFlag=1， 9.8和MK安全。协议目标以goal/2谓词形式表示，即Belief(Identity,Trust)。信任Trust是关于安全属性的谓词，包括Existing(Identity),Secret(Identifier),Fresh(Identifier)和Associate(Identifier,Identity)。谓词Existing(Identity)表示一个主体拥有关于这个主体Identifier的确参与通信的信任。谓词Secret(Identifier)表示一个主体拥有关于这个新鲜性标识符Identifier的保密性信任。谓词Fresh(Identifier)表示一个主体拥有关于这个新鲜性标识符Identifier的新鲜性信任，即新鲜性标识符Identifier是为这个协议新生成的一个TVP。谓词Associate(Identifier,Identity)表示一个主体拥有关于这个新鲜性标识符Identifier的关联性信.和Belief(A,Secret(kAB)),Belief(A,Fresh(kAB)),Belief(A,Associate(kAB,A))以及Belief(A,Associate(kAB,B))B协议要实现的安全目标是Belief(B,Existing(A)),Belief(B,Secret(kAB)),Belief(B,Fresh(kAB)),Belief(B,Associate(kAB,A))以及Belief(B,Associate(kAB,B))。BMFPrologBMF分BMF的自动化分析之前，和协议相关的要分析的消息、术语和初始假设已BMF分发送者读取接收者读取图 的，并显示‘FAILED!’。BMF规则引擎为新增加的信任多集形式化方法推理规则的输入提供了一个图形化的环BMF分析引擎中使用的推理规则进行扩rules:-fact(PremiseIndex1,Statement1ToBeInserted,-),...not(fact(-,Conclusion,-)),getMaxFactIndex(MaxIndex),NewIndexisMaxIndex+1,PremiseIndices=[PremiseIndex1,PremiseIndex2,...],将信任多集形式化方法中的新推理规则转换为Prolog格式的BMF分析工具中的推理规则。用信任多集形式化方法中新推理规则的条件替换Statement1ToBeInserted,Statement2ToBeInserted等。用信任多集形式化方法中新推理规则的结论替换ConclusionToBeInserted；用新推理规则的名字替换RuleNameToBeInserted。fact/3谓词指定这个规则的所有初始假设，PrologProlog是一种与人工智能相关的程根据信任多集形式化方法对协议进行安全性分析得来的安全属性缺失，BMF攻击引擎支持任新鲜性方法构造攻击的攻击引擎，如图9.10所示。B(A)构造“攻击”：图 5；如果N-S协议的安全性分析，AB在这个协议运行中的确参与了通信，并且共NANBABB相B没有得到任何确凿的证据来证明NAAB相关联。Message I(A)→ {A,NAMessage1 I(A)→B: {A,NA}KBMessage B→ {NA,NBMessage I(A)→ A所以无法得到新鲜性标识符NB。AA如果攻击者I想要生成消息{NB}KB，I必须知道NB。由于NB只出现在消息2和消息3中，AIIMessage ??→ {Message A→ {MessageA{A,??}Message{??,NB}MessageA到NB只能重放记录的包括{??,NB}KA的消息2{NA,NB}KA给A，即Message “??”Message A {A,NAMessage1 I(A)→B: {A,NA}KBMessage B→ {NA,NBMessage I(A)→ Message1’ A→I: {A,NA}KIMessage2’ Message3’ A→I:

MessageA{A,NAMessageI(A)→{A,NAMessageB→{NA,NBMessage{NA,NBMessageAMessageI(A)→ {A,N {A,NA{A,NA 3’. AB共享了秘密随机数NA和NB，以生成新的会话密钥。DongL,ChenK,ZhengY,HongX(2008)TheGuaranteeofAuthenticationProtocolSecurity.JournalofShanghaiJiaoTongUniversity,42(4):518–522(inChinese)ChenK,DongL,LaiX(2008)SecurityAnalysisofCryptographicProtocolsBasedonTrustedFreshness.JournalofKoreaInstituteofInformationSecurityandCryptology,18(6B):1–13DongL,ChenK,LaiX(2009)BeliefMultisetsforCryptographicProtocolAnalysis.JournalofSoftware,20(11):3060–3076(inChinese)DongL,ChenK,LaiX,WenM(2009)WhenisaKeyEstablishmentProtocolSecurityandCommunicationNetworks,2(6):567–SaulE(2001)FacilitatingtheModellingandAutomatedAnalysisofCryptographicMasterThesis,UniversityofCapeMaoW(2004)ModernCryptography:TheoryandPractice.PrenticeHall,NewSaulEandHutchisonA(1999)SPEARII:TheSecurityProtocolEngineeringandAnalysisResource.SecondSouthAfricanTelecommunications,Networks,andApplicationsAccessed9JulyBekmannJ,GoedeP.deandHutchisonA(1997)SPEAR:aSecurityProtocolEngineering&AnalysisResource.InDIMACSWorkshoponDesignandFormalVerificationofSecurityProtocols./Workshops/Security/program2/hutch/spear.html.Accessed9JulyBurrowsM,AbadiM,andNeedhamR(1990)Alogicofauthentication.ACMTransactionsonComputerSystems,8(1):18–36LoweG(1996)BreakingandFixingtheNeedham-SchroederPublic-keyProtocolFDR.In:TACAS’96Proceedingsofthe12thInternationalConferenceonToolsandAlgorithmsfortheConstructionandAnalysisofSystems,Passau,27–29Mar1996.LectureNotesinComputerScience(LectureNotesinSoftwareConfigurationManagement),vol1055.Springer-Verlag,Heidelberg,pp147–166LoweG(1995)AnAttackontheNeedham-SchroederPublicKeyAuthenticationInformationProcessingLetters,56(3):131–133,LoweG(1996)SomenewAttacksUponSecurityProtocols.InProceedingsofthe9thIEEEComputerSecurityFoundationsWorkshop,pages162–169,Jun.1996RoscoeAW(1994)ModelCheckingCSP.In:RoscoeAW(ed)AClasicalMind:EssaysinHonourofC.A.RHoare.Prentice-Hall,1994MeadowsC(1996)TheNRLProtocolAnalyzer:anOverview.JournalofLogicProgramming,26(2):113–131DolevD,YaoAC(1983)OntheSecurityofPublicKeyProtocols.IEEETransactionsonInformationTheory29(2):198–208MeadowsC(1994)AModelofComputationfortheNRLProtocolAnalyzer.In:Proceedingsofthe1994ComputerSecurityFoundationsWorkshop,Franconia,14–16June1994HarkinsDandCarrelD(1998)TheInternetKeyExchangeProtocol(IKE).IETFRFC2409,/rfc/rfc2409.txt.Accessed9July2012KaufmanC(2005)InternetKeyExchange(IKEv2)Protocol.IETFRFC4306,/html/rfc4306.Accessed9July2012SET(1997)SecureElectronicTransaction.TheSETStandardSpecification./set/.Accessed9July2012MitchellJ.C,MitchellMandSternU(1997)AutomatedAnalysisofCryptographicUsingMurΦ.Proc.of1997IEEESymposiumonSecurityandPrivacy,Oakland,California,pp141–153NeedhamRM,SchroederMD(1978)UsingEncryptionforAuthenticationinLargeNetworkofComputers.CommunicationoftheACM21(12):993–999Tatebayashi