安全协议的定量分析：Dolev-Yao入侵者模型的扩展和协议攻击的可能性研究

理论计算机科学电子笔记164（2006）3-25www.elsevier.com/locate/entcs安全协议的定量分析PedroAdao1，5，6SQIG-IT，IST，里斯本，葡萄牙Paulo Mateus保罗·马特乌斯2，5SQIG-IT，IST，里斯本，葡萄牙Tiago Reis蒂亚戈·雷斯3，5，7瑞士苏黎世联邦理工学院计算机科学系，SQIG-IT，IST，里斯本，葡萄牙LucaVigan`o4瑞士苏黎世联邦理工学院计算机科学系摘要本文有助于进一步缩小形式化分析和具体实现之间的差距通过引入Dolev-Yao入侵者模型的一个定量扩展，对安全协议进行了研究。这个扩展的模型提供了一个基础，考虑可能的协议攻击时，入侵者有合理量的计算能力，特别是当他能够以一定概率猜测加密密钥或其他特定种类的数据（诸如散列消息的主体）时。我们还表明，这些扩展不增加计算复杂性的协议不安全问题的情况下，有限数量的交织协议会话。关键词：安全协议，Dolev-Yao入侵者，概率入侵者，符号协议分析，计算协议分析。1电子邮件地址：pad@math.ist.utl.pt2电子邮件地址：pmat@math.ist.utl.pt3 电子邮件地址：tireis@inf.ethz.ch4电子邮件地址：vigano@inf.ethz.ch5 通过CLC项目QuantLog POCI/MAT/55796/2004，由联邦开发署/联邦贸易委员会支持的工作。6来自联邦现金信托基金赠款的额外支助SFRH/BD/8148/2002。7来自联邦现金信托基金赠款SFRH/BD/22928/2005的额外支助。1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.07.0094P. Adão等人/理论计算机科学电子笔记164（2006）31引言在过去的几年中，已经提出了许多工具用于安全协议的形式化分析，例如[1，8，10，15，22，25，27，29，32]）。这些工具已经帮助证明了几个协议的正确性，并发现了其他几个协议中的漏洞然而，还有许多协议尚未被分析，事实上，它们超出了这些工具的范围。 其中一个主要原因是，这些工具在完美密码学的假设下分析协议，并且协议消息是在Dolev-Yao（DY）入侵者控制下的网络上交换的。也就是说，通过考虑标准的独立于协议的异步模型来分析协议，主动入侵者控制网络，但不能破解密码（特别是，入侵者可以拦截消息并分析它们，但只有当他拥有相应的解密密钥时，他才能从他的知识中生成消息并以任何代理名称发送它们）。因此，DY模型太弱，无法指定几种类型的安全协议，即那些包括掷硬币和内在密码原语（如零知识证明系统，不经意传输，安全计算和比特承诺）。此外，众所周知，有一些协议可以被证明对于DY模型是安全的，但在考虑特定的密码系统时是不安全的。例如，Needham-Schroeder-Lowe协议的然而，当前一代的安全协议分析工具并没有解决协议的实际实现问题，即使当利用与符号和复杂性模型相关的结果[2，3，4，5，6，9，11，12，14，19，20，23，24，30，31，35，36]时，等价性也是可以忽略的函数，因此当我们在“现实世界”中我们工作的主要目标是通过引入经典Dolev-Yao模型的定量扩展，进一步缩小安全协议的形式化分析和具体实现之间的差距，我们称之为pDY。 这使我们能够考虑当入侵者具有合理的计算能力时可能发生的协议攻击，特别是当他能够猜测加密密钥或其他特定类型的数据时。我们形式化这样一个入侵者模型扩展DY模型与addi- tional结构和入侵者的能力。作为一个例子，虽然在DY模型中加密被认为是一个类似地，作为另一个相关的例子，我们还引入了一个演绎规则，允许入侵者演绎散列消息的主体。正如人们可以预期的，这些操作（应该）仅以小概率发生在“现实世界”中，因此使用这些规则获得的推导也应该反映几乎不可行的攻击。P. Adão等人/理论计算机科学电子笔记164（2006）35当使用DY模型时，习惯上将协议的交错执行形式化为无限状态转换系统，然后可以搜索代表协议攻击的状态（例如，入侵者掌握了一些数据的状态，这些数据原本是两个诚实代理之间的秘密）。这个转换系统以标准的方式定义了一个计算树，其中根是初始系统状态，子节点表示状态在一次转换中的演化方式。在pDY模型中，我们扩展了这个搜索树，使得每个可能的转移都有一个概率来加权;例如，一个有可能猜到密钥的状态将有一个包含该密钥知识的后继状态，但是这个转移将用猜到密钥的概率来加权。由于树的每个转移都将与该转移的概率加权，因此我们可以计算与树的分支相关的概率，并且最终我们将能够知道每个攻击的概率是多少。我们的工作的另一个贡献是表明，在有限数量的交织协议会话的情况下，协议不安全的计算复杂性并没有增加我们的扩展。例如，在[26]中，当考虑有限个协议会话时，在经典DY入侵者模型中搜索攻击是NP完全问题，并且我们证明了如果我们考虑扩展的概率入侵者模型pDY，则该问题仍然是NP完全的。我们按以下步骤进行。在第2节中，我们介绍了经典DY入侵者模型的入侵者推断问题，并对有限个协议会话的模型检验算法的决策版本进行了复杂性分析。在第三节中，我们介绍了经典DY模型的一个定量扩展，并对相应扩展的模型检测算法进行了复杂性分析。在第4节中，我们考虑一个简单的例子来说明我们的概率入侵者pDY可以应用于协议分析。 第五部分对相关工作进行了比较，并对未来的研究方向进行了展望。2 Dolev-Yao入侵下的模型检验协议粗略地说，Dolev-Yao入侵者[16]是完全控制网络但无法破解密码的代理。通过控制网络，我们的意思是入侵者可以冒充其他代理，阻止消息到达目的地，或将它们重新路由到其他代理。入侵者也可以从他所获得的知识中生成消息并将其发送给任何代理，但是除非他知道相应的密钥，否则他无法破解加密，并且除非他已经知道，否则无法出于这个原因，入侵者的知识在DY模型中起着基础性的作用事实上，安全协议分析的核心问题之一就是所谓的入侵者推导问题：给定协议执行的状态，入侵者能否推导出给定的消息M？这里的推导是相对于入侵者当前知道的术语而言的，即相对于在他的初始知识的一组推导规则下的闭包而言的，所述初始知识是用他在协议期间观察到的消息来扩充的6P. Adão等人/理论计算机科学电子笔记164（2006）3执行.入侵者推断问题为解决许多实际相关的协议分析问题提供了基础例如，我们可以用它来确定入侵者是否能够构造出某个诚实的代理人期望接收的形式的消息，或者他是否能够获得一个意图成为秘密的消息，例如由两个诚实的代理人共享的密钥。由于DY入侵者模型抽象了密码学、复杂性和概率，它减少了对意外协议交织的攻击，从而将因此，安全性被简化为检查安全条件;粗略地说，入侵者是否从未获得/产生某些私有数据？模型检测是特别有吸引力的处理这些问题。模型检查安全条件的基本思想是检查是否有可能达到条件失败的状态。模型检查算法包括生成所有可能的可达状态，并检查这些状态中的每一个是否满足条件。一般来说，在可以以交错方式执行的任意数量的协议会话的情况下，问题是不可判定的，因为它可以简化为停机问题。在有限数量会话的限制下，在DY入侵者模型中搜索攻击的问题是NP完全问题[26]（因此检查协议是否安全是co-NP完全的）。本文所考虑的方法是通用的，与技术无关的，因此可以有效地结合到不同的安全协议 分析技 术和 工具中 。为了 具体起 见， 我们考 虑基于 约束 的模型 检查 器OFMC[1，7，32]。[8]我们现在将总结OFMC（以及许多其他方法和工具）的关键定义和结果，然后在第3节中我们将扩展到我们在这里考虑的概率入侵者模型更具体地说，我们现在给出了一个模型检查算法的启发OFMC的方法有限数量的会话，并提供了详细的复杂性分析该算法。为此，我们首先考虑[7]中给出的上下文无关文法，用于形式化协议描述：定义2.1设C和V是不相交的可数常数集（用小写字母表示）和变量集（用小写字母表示）。 我们的语法8OFMC是在AVISPA项目范围内开发的。AVISPA工具是一个完全自动化的协议分析环境，包括OFMC和其他三个工具（称为CL-AtSe，SATMC和TA 4SP），并已成功应用于大量的按钮分析。工业规模的安全协议P. Adão等人/理论计算机科学电子笔记164（2006）37协议规范语言由以下上下文无关语法定义ProtocolDescr：：=（State，Rule_Rule_State）规则：：=LHSRHSAttackRule：：=LHSLHS：：=State NegFactCondition RHS：：=StateState：：= PosFact（. PosFact）NegFact：：=（. not（PosFact））PosFact：：= state（Msg）|消息（Msg）|我知道（Msg）|secret（Msg，Msg）条件：：=（MsgMsg）Msg：：= AtomicMsg|合成消息ComposedMsg：：=发送Msg，Msg发送|{Msg}消息|{1}|MSG|}消息|消息（Msg）|Msg −1AtomicMsg：：= C| V|N|新鲜（C，N）我们把与非终结符n相关的上下文无关语言写成L（n）。我们写vars（t）来表示在（消息、事实或状态）项t中出现的变量集合，当vars（t）= 0时，我们说t是ground，并写ground（t）。我们直接将函数vars和ground扩展到更复杂的项。在本文中，我们给出了一个快速直观的自上而下的解释所使用的gram-mar。我们请读者参考[7]的详细解释。一个协议用L（ProtocolDescr）中的一个项来表示，即一个三元组（I，R，AR），其中I是初始状态，R是转换规则的集合，AR是用于识别攻击状态的规则集状态表示网络的内部状态，并由一组积极的事实表示。有四种类型的肯定事实：（i）状态（Msg），表示诚实代理的本地状态;（ii）消息（Msg），表示通过网络传输的消息（即发送但尚未接收的消息）;（iii）i知道（Msg），表示入侵者知道的消息;以及（iv）秘密（Msg，Msg），表示秘密消息，其中秘密（m，a）意味着m是秘密，并且允许代理a知道它。规则描述状态转换。规则r=lhsrhs的左侧lhs由一组正事实P、一组负事实N和一个条件Cond组成，其中vars（P）<$vars（N）<$vars（Cond）。否定事实是对肯定事实的否定，通常只考虑对国家和秘密事实的否定条件只是信息不等式的合取。直观地说，这些规则模拟了诚实代理执行协议的通信步骤更具体地说，规则对执行协议的诚实代理的转换进行建模，即过渡8P. Adão等人/理论计算机科学电子笔记164（2006）3诚实的代理发送一个消息来回复他们收到的另一个消息启用这种转换的状态由关联规则的lhs描述。步骤执行后的状态由规则的rhs描述，它只由肯定事实组成。攻击规则对可能对协议进行攻击的条件进行建模，并且仅由表征攻击条件成立的状态的lhs消息术语用于描述所有相关信息，如入侵者知识、密钥、网络状态等。消息可以是原子的，也可以是组合的。原子消息是一个常数、一个变量、一个自然数或一个新的常数。新鲜常数用于模拟随机数据的创建例如在协议会话期间的随机数在[7]之后，我们通过一个唯一的术语fresh（c，n）对每个新数据项进行建模，其中c是一个标识符，数字n表示c所针对的特定协议会话。消息可以使用封装文件m1、m2或密码或密码操作符m1来一个nd{|M2|}m1（f或用m1对m2进行非对称和对称加密），m1（m2）（用于函数m1到消息m2，表示散列函数或密钥表），或者m−1（对于m的非对称逆）。在我们提出上述语言中描述的协议的模型检查算法之前，我们考虑[7]中提出的简化 首先，我 们假设 AR仅由 一个攻击 规则构成 。此外 ，我们只 考虑规则r=lhs<$rhs∈R具有以下形式的协议（I，R，AR）：msg（m1）. 状态（m2）.P1. N1=Cond状态（m3）. msg（m4）.P2，（1）其中N1是不包含i knows或msg事实的否定事实的集合，P1和P2是不包含状态或消息事实的肯定事实的集合此外，委员会认为，我们要求如果i知道（m）∈P1，那么i知道（m）∈P2;这确保了入侵者的知识是单调的，即入侵者在转换期间不会忘记消息在规则的lhs和rhs中出现的状态事实意味着该规则描述了诚实代理人的一个转变。此外，在两端，我们都有一个msgfact，它表示代理为了进行转换（在lhs中）和代理对应于初始（相应地，最终）协议步骤的规则不包含传入（相应地，传出）消息。然而，规则形式（1）不是限制，因为总是可以插入可以由入侵者生成的伪消息。事实上，如[7]所述，形式（1）的规则足以描述非常大的一类工业规模的安全协议，包括Clark/Jacob协议库[13]中的协议以及Internet协议，如IPSec，SET，IPSec，IKE，TLS和H.530。协议描述（I，R，AR）模型检验的基本思想是从初始状态I（包含诚实协议代理和入侵者的初始知识）出发，建立一个状态转移系统，对协议的交错执行进行建模，并应用R中的转移规则计算每个后继状态。对于每个继承国，我们检查P. Adão等人/理论计算机科学电子笔记164（2006）39Mm∈MGm1∈ DY（M）m2∈ DY（M）Gm∈ DY（M）公理m∈ DY（M）对1 2m1∈ DY（M） m2∈ DY（M）Gm1∈ DY（M）m2∈ DY（M）G{m2}m1 ∈ DY（M）隐窝{|M2|}m1 ∈ DY（M）Scryptm1∈ DY（M）m2∈ DY（M）G<$m1，m2 <$∈ DY（M）Am（m）∈ DY（M）适用m∈ DY（M）对12i{m2}m∈ DY（M）m−1∈ DY（M）{m2}−1∈ DY（M）m1∈ DY（M）11Acryptm2∈ DY（M）{|M2|}m1 ∈ DY（M）m1∈ DY（M）A1m2∈ DY（M）−1隐窝m2∈ DY（M）ScryptFig. 1. 经典DY入侵者的产生和分析规则。是否可以应用AR中的攻击规则。如果是这种情况，那么我们已经发现了一个攻击，否则我们计算下一个后继状态，并重复这个过程，直到发现一个攻击或没有更多的状态可以生成。后一种情况只发生在有限数量会话的情况在下面的定义2.3中，我们给出了经典Dolev-Yao入侵者下有限个协议会话的模型检查算法（的决策版本该算法在[7]中（隐式地）给出，但其复杂性在那里没有研究。为了提供算法的复杂性分析，我们需要形式化生成后继状态和查找攻击的方法。我们首先描述如何生成后继状态。由于规则是协议步骤的模型，状态S的后继状态是通过分析适用于这个S的规则来获得的，也就是说，S“满足”与lhs相关联的前置条件的规则设置换σ是从V到L（Msg）的映射。正如我们将在下面正式定义的那样，一个规则适用于一个状态，如果（i）对于规则变量的某些替代σ，回想一下，规则lhsrhs的右侧rhs只是一组正事实，其中vars（lhs）vars（rhs）。状态S的后继者则是通过在S中将与某个适用规则的lhs的正事实相匹配的事实替换为该规则的rhs而生成的状态。可以看到，入侵者有能力用他知道的或者可以从他的知识中生成的任何消息来替换适用规则中涉及的消息。出于这个原因，描述入侵者所知道的消息集是至关重要的定义2.2对于一个消息集合M，我们将Dolev-Yao入侵者知识DY（M）定义为在图1中给出的生成（G）和分析（A）规则下闭合的最小集合。1.一、一10P. Adão等人/理论计算机科学电子笔记164（2006）3R生成规则表示入侵者可以利用配对、非对称和对称加密以及函数应用等方法从已知消息中合成消息。分析规则描述了入侵者如何分解消息。注意，没有给出允许入侵者分析函数应用的规则，例如从h（m）恢复m，其中h是某个散列函数。此外，请注意，这种形式化正确地处理了非原子密钥，对于-stancem ∈DY（{{|M|}h（k1，k2），k1，k2，h}）。我们现在能够对一系列继承国作出分析性介绍，但在此之前，让我们固定一些符号。 设P1是从P1中去掉所有我知道事实P1= P1\{f|好吧 f = i knows（m）}。我们通过将状态S和r的左侧lhs映射到基替换σ的函数Apply来定义形式（1）的规则r的适用性，在该函数下，规则可以应用于状态：适用lhs（S）={σ|ground（σ）dom（σ）= vars（m1）dvars（m2）dvars（P1）{m1σ}|i知道（m）∈ P1}<$DY（{m|i知道（m）∈ S}）n态（m2σ）∈S<$P1σ<$S1999年， 不是（f）∈ N1=<$fσ/∈ S）<$σ <$Cond}.此外，我们还定义了后继函数成功率R（S）=r∈R步骤r（S）即，给定形式（1）的规则的集合R和状态S，通过步骤函数产生相应的后继状态的集合步骤lhsrhs（S）={S}|好吧σ∈适用lhs（S）<$SJ=（S\（state（m2σ）<$P1σ））<$state（m3σ）<$i knows（m4σ）<$P2σ}.如前所述，通过将后继函数应用于协议的初始状态I，然后应用于其后继，来构建对协议（I，R，AR）建模的转换系统。 通过这种方式，我们获得了可达状态的集合，并且重要的是要注意这个集合是一个基础模型。由于我们定义转换的方式，没有可达状态包含变量。形式上，协议的可达状态集（I，R，AR）是Reach（I，R）= Succn（I）.n∈N最后，我们描述了如何描述不安全的状态。为此，我们引入了一个攻击谓词P. Adão等人/理论计算机科学电子笔记164（2006）311isAttackAR（S），当攻击确定为12P. Adão等人/理论计算机科学电子笔记164（2006）3根据攻击规则，在状态S处发现AR。如果规则AR可以应用于状态S，则该攻击谓词isAttackAR（S）为真，即， 适用AR（S）/= 0。为了简单起见，我们在这里只考虑模型检查算法的决策版本。这意味着算法只是判断是否存在攻击，而攻击本身不会返回。我们将S初始化为入侵者和诚实协议代理最初可用的知识，也就是说，给定协议P=（I，R，AR）状态S等于I。定义2.3有限数量协议会话的模型检查算法的决策版本：ModelCheck（P）输入：方案P =（S，R，AR）输出：如果协议是安全的，则为1，否则为1. If（isAttackAR（S））then返回0;2. 对于每个r∈R，计算集合Applicablelhs（S），其中r=lhs<$rhs;3. 计算SuccR（S）;4. 对每个SJ∈SuccR（S）;5.B=ModelCheck（SJ，R，AR）;6.如果（B==0），则返回0;7. 返回1.在进行复杂性分析之前，我们引入一些符号并进行一些观察。首先，我们归纳地定义消息的深度m∈ L（Msg）如下：• 如果m是原子，则深度（m• depth（c（m））=1+depth（m）如果c是一元构造函数;• depth（c（m1，m2））=1+depth（m1）+depth（m2）如果c是二元构造函数。请注意，在上述算法的步骤2中，需要相应地计算一组替换，其中包含可应用的lhs（S）。这些替换允许入侵者用他知道的消息替换消息此外，通过查看定义2.2，很容易认识到，由于生成规则，入侵者知道的消息集是无限的。然而，通过将会话的数量固定为s并假设每个会话最多由j个步骤组成，很容易看出只有有限数量的消息才能导致攻击。这一事实背后的直观论点是，与代理的交互只能增加/减少计算中涉及的消息的深度。由于会话的总步骤数是有限的，因此存在限制k，使得如果存在攻击，则存在具有以至多k的深度交换的消息的攻击。 该值取决于协议的所有参数：初始状态、规则和攻击规则;以及并行执行的协议会话数。此外，不失一般性，P. Adão等人/理论计算机科学电子笔记164（2006）313我们假设k大于协议中出现的所有消息项的深度。仍然在消息术语的上下文中，下面的结果给出了从代数签名自由生成的直到某个深度的术语数量的上限。引理2.4对于具有b个二元构造函数、u个一元构造函数和a个原子符号的自由代数，深度小于或等于k的项数为：2K时间复杂度为O（（a+b+u））。我们现在讨论一项议定书的平行会议的数目问题。假设一个协议有s个会话，其中j个步骤并行运行由于我们用规则r∈R对协议的每个步骤（会话）进行建模，因此每个会话都有j条规则。此外，没有什么可以阻止协议完全并行，也就是说，没有什么可以阻止R中的所有规则适用于除最终状态之外的所有可达状态。因此，我们知道，对于协议的s个会话和j个步骤，我们最多可以有j×s=n个规则适用于每个状态。现在我们可以开始复杂性分析了。从引理2.4，我们得出结论，生成的深度小于或等于k的消息项的数量2K从一个原子符号是O（（a+ 5） ）（有4个二进制构造函数和1个一元构造函数消息项的构造函数）。由于我们假设k是协议的消息项深度的上限，因此入侵者每次消息交换最多只能学习k个原子符号。 如果我们假设入侵者最初知道原子消息，我们得出结论，入侵者2K时间复杂度为O（nk+i+ 5） ）=num i know. 通过假设lhs和rhs如果R中的规则中有一个最多有v个变量，则检查它们是否适用的替换次数为O（num i knowv）= O（（nk + i + 5）v2k）= num sub。因为对于每个规则，我们最多有num个新的后继状态，并且给定最多有n个规则，给定状态的后继数为O（n×num_sub）= O（n（nk + i + 5）v2k）= num_sub。观察模型检查算法的递归树的深度是j×s=n，因此递归树将最多生成O（num<$n）=O（nn（nk+i+ 5）<$2k）=num tot st total states。在最坏的情况下，谓词必须在所有这些状态上进行检查，因此步骤1的总时间复杂度通过将num tot st乘以检查isAttack谓词的时间复杂度来获得回想一下，isAttack（S）谓词简化为检查适用AR（S）/= 0。因此，时间复杂度的上限是计算适用AR的时间复杂度。对于任何lhs，为了计算适用的lhs，我们需要在v个变量的所有num个子基替换上由num i已知的项来 确 定范围，入侵者，而且如果某些条件成立，则验证这些替换中每一个。 后一个验证在lhs的大小上需要多项式时间，为了简单起见，我们认为对于所有规则r∈R，最多需要g时间。假设14P. Adão等人/理论计算机科学电子笔记164（2006）3入侵者知道的所有消息项都存储在内存中，访问时间为O（1），为了生成所有num_sub可能的替换，它需要O（num_sub×v×log（num_idknow））（这对应于在一个以num_idknow为基数的v位数上生成num_sub_increment）。因此，计算可应用lhs（S）的时间复杂度为：O（g×num sub×v×log（num i know））=O（gv（nk+i+5）v2klog（（nk+i+5）2k））时间复杂度：O（nk+i+5）=时间app。因此，我们得到在所有状态上检查isAttack谓词的时间复杂度为时间复杂度O（timeapp×numtot st）=O（gv2knn（nk+i+5）（n+1）v2klog（nk+i+5）），它负责算法的步骤1为了计算步骤2的复杂度，我们只需将状态总数num tot st乘以计算可应用lhs（S）的时间复杂度时间app和规则总数n，从而获得时间复杂度为O（gv 2 knn+1（nk + i +5）（n +1）v 2k log（nk + i +5））.步骤3的时间复杂度包括生成后继状态，其由状态的总数限定由于我们假设入侵者在每个状态下的知识都存储在内存中，所以我们需要更新它。在最坏的情况下，入侵者在每个状态下所知道的消息项的数量是O（num i know）。将消息项更新到深度k所需的时间是有界的 通过O（num i know2）乘以DY模型中存在的二进制规则的数量加上O（num i know）乘以一元规则的数量。 其思想是考虑所有已知消息对，并应用所有可能的二元规则，同样适用于单一规则。详细地说，对于每个二进制规则，我们必须考虑入侵者知道的每对消息，应用规则（如果可能的话）并验证我们是否获得未知消息。如果是这种情况，我们必须将此消息添加到入侵者的知识中，并从此考虑与此新消息的配对。一个类似的方法来更新入侵者的知识是一元规则。由于有七个二元规则和一个适当的一元规则（G公理不需要考虑），并通过假设所有DY入侵者规则最多需要d时间来应用，我们得出结论，更新入侵者知识的总时间为O（d（7 num i know2+ num i know））= O（d（nk + i +5）2k+1）= updknow.最后，由于我们需要为每个非初始状态更新入侵者知识，因此步骤3的总体复杂度由下式给出：时间复杂度为O（nk + i +5）（2+ i）2k）。该算法的其余步骤对应于遍历递归树，因此我们得出结论：P. Adão等人/理论计算机科学电子笔记164（2006）315命题2.5在经典Dolev-Yao入侵者下，对于有限数量的协议会话，模型检查算法Mo-delCheck（P）的总体复杂度为：时间复杂度为O（gv 2 knn+1（nk + i +5）（n +1）v 2k log（nk + i +5）+dnn（nk + i +5）（2+ n）2k）.上述分析给出了模型检查算法的复杂性的上限，并表明朴素模型检查器在协议步骤、协议会话和每步交换的消息的数量上是指数的，在入侵者需要知道的消息的最大深度上是双指数的，并且在其余因子上是多项式的。然而，它暗示，所提出的算法是相当昂贵的时间。事实上，这主要是由于过渡系统的后继状态数量过多，这是由入侵者在每个协议步骤中获得的大量消息引起的（这导致了入侵者需要知道的消息避免这个问题的一种方法是考虑一个象征性的“懒惰”入侵者（参见[ 7 ]和那里的各种参考文献），一个在步骤2中的替换被推迟并受到实质性限制的对于懒惰的入侵者来说，实现了更好的性能，但是复杂性分析超出了本文的范围，并且远不是简单的。上述计算的目的是为比较经典Dolev-Yao入侵者下的模型检查复杂度与我们在下一节介绍的入侵者概率扩展3扩展入侵者模型经典的Dolev-Yao入侵者模型假设密码学是完美的，并且只有当入侵者知道相应的解密密钥时，他才能解密加密的消息由于我们工作的最终目标之一是以允许入侵者对密码学进行攻击的方式来增强入侵者模型（例如，表示他可以以一定的概率破坏加密），因此我们不能再忽略协议规范中使用的底层密码学方案。我们的方法允许入侵者例如，入侵者可以猜测密钥来解密加密的消息，或者从散列值猜测散列函数的参数这种新的能力可能会导致入侵者知识的显著增加，从而为攻击开辟新的途径。因此，通过简单的猜测或诉诸密码分析技术来准确地测量正确检索数据的概率是很重要的。一般来说，使用这种新的入侵者模型，我们希望在协议流的重要位置检测由错误选择的密码系统引起的协议中的漏洞，例如重复使用相同的加密密钥，允许入侵者收集足够的信息，以便能够以高成功概率计算密钥，或者使用具有低安全参数的密码函数16P. Adão等人/理论计算机科学电子笔记164（2006）3为了量化入侵者的行为，我们遵循一种基于给定密码系统的密钥空间和密码函数的共域的维度的方法，考虑到额外的知识可能会显着减少密钥空间。[9]为了形式化协议描述，我们考虑定义2.1中给出的上下文无关文法，并将其扩展以表达入侵者使用猜测时的转换概率。为了跟踪转移概率，我们用一个新的正事实plabel（R）扩展了语言，并且我们还引入了函数p：L（Msg）× P（L（PosFact））→R使得p（m，IK）返回当入侵者的知识是IK时他知道m∈ L（Msg）的概率，即形式为i knows（Msg）的一组肯定事实。我们将在后面解释这个概率是如何计算的。作为一个具体的例子，我们现在考虑用三个特定的猜测规则来扩展入侵者的演绎能力。定义3.1对于一个消息集合M，我们将pDY（M）定义为在图2中给出的规则下闭合的最小集合：生成规则（G），分析规则（A），两个规则guessSK和guessPK，用于入侵者猜测对称和逆（私有）密钥，以及一个规则guessHash，该规则指出，只要入侵者拥有消息的哈希值，他就可以检索该消息或其部分（注意，我们假设哈希函数对所有参与者都是已知的，因此对入侵者来说也是已知的）。请注意，我们在这里考虑的猜测规则有助于我们说明我们的方法的原理，但是，在存在其他密码运算符的情况下，我们当然可以添加其他类似的猜测规则。例如，我们还可以引入嵌套哈希规则H（. H（. 我... ）... ）∈pDY（M）mi∈pDY（M）或甚至考虑更一般的规则mi∈pDY（M）表示入侵者可以猜出任何消息。对所有不同的可能性进行批判性的比较将是今后工作的主题为了在入侵者模型中包含这些变化，状态转换必须考虑入侵者在导出消息时可能使用了猜测规则这一事实。因此，我们需要区分确定性转移和概率性转移。为了进行这种区分，我们用我们获得的值来标记每个转换9请注意，可以使用其他方法，例如暴力攻击所需的计算能力，或者在给定密码分析时间范围的情况下成功攻击的可能性。 当然，这些方法高度依赖于对入侵者计算能力的假设，尽管如此，它们可以被调整以反映相对强大的入侵者的能力。 还要注意的是，我们在这里提出的方法是不同的，事实上是互补的，符号，演绎的方法，在[18]中提出的o-线猜测。P. Adão等人/理论计算机科学电子笔记164（2006）317M1m∈MGm1∈pDY（M）m2∈pDY（M）Gm∈pDY（M）公理m∈pDY（M）对1 2m1∈pDY（M）m2∈pDY（M）Gm1∈pDY（M）m2∈pDY（M）G{m2}m1∈pDY（M）隐窝{|M2|}m1∈pDY（M）Scryptm1∈pDY（M）m2∈pDY（M）G<$m1，m2 <$∈pDY（M）Am（m）∈pDY（M）适用m∈pDY（M）对12i{m2}m∈pDY（M） m−1∈pDY（M）{m2}−1∈pDY（M）m1∈pDY（M）11Acryptm2∈pDY（M）{|M2|}m1∈pDY（M）m1∈pDY（M）A1m2∈pDY（M）−1隐窝m2∈pDY（M）Scrypt{|M2|}m1∈pDY（M）{m2}m1 ∈pDY（M）guessSKm1∈pDY（M）m−1∈pDY（M）guessPKH（m1，. 我...，mk）∈ pDY（M）mi∈pDY（M）guessHash图二. pDY入侵者的演绎规则。从函数p，其中p返回1，如果不需要猜测。 当一国如果发现S触发攻击规则AR，我们通过向后遍历攻击轨迹（从S到I）并乘以所有概率标签来确定攻击概率。请注意，这样做，我们只是我们通过扩展函数pApply定义规则r的扩展适用性，该扩展函数将状态S和r的左手侧lhs映射到对σ，σ ∈R，其中σ是基替换，并且σ∈R，在该扩展函数下，规则可以应用于状态：p适用lhs（S）={σ，|ground（σ）dom（σ）= vars（m1）dvars（m2）dvars（P1）{m1σ}| i知道（m）∈P1}<$pDY（{m| i知道（m）∈S}）n = n∈co-dom（σ）p（t，{m |i知道（m）∈ S}）n态（m2σ）∈S<$P1σ<$S1999年，不是（f）∈N1 =<$fσ/∈S）<$σ <$Cond}.为了计算p（t，{m| iknows（m）∈S}），我们首先假设一个算法prule来计算p DY入侵者模型的猜测规则的每个实例ρ的概率prule（ρ）。该算法依赖于密码学的假设，并且假设是针对模型检验算法给出的给定δ的导数一18P. Adão等人/理论计算机科学电子笔记164（2006）3Rm使用pDY规则，通过δ知道m的概率pδ（m）通过乘以与规则ρ在δ中出现的实例相关联的所有概率prule（ρ）来给出。然后我们有p（t，IK）= max {pδ（m）|δ是使用知识k}的m的导出。我们将在扩展的模型检查算法中讨论一种计算p（t，IK）的（朴素）方法 现在，让我们观察到，人们可能会试图将p（t，IK）定义为所有导子导致m的概率之和。但是，这可能导致值大于1。我们的方法背后的想法是，与推导相关联的概率值给出了当入侵者的计算能力被消耗时应用规则的成功的度量如果他试图应用某个概率规则而失败了，那么他将耗尽他的计算能力，并且不能再次应用这个或另一个概率规则另一方面，如果他成功地应用了一些概率规则，那么我们假设入侵者没有用尽他所有的计算能力，因此，他可以继续进行其他推导。两个推导可能导致相同的消息m，其中一个的概率为0。另一个概率是0。9.得到这个消息的概率是0。9，因为入侵者的最佳选择是尝试通过二阶导数获得m。另一个误导性的想法可能来自于认为如果规则的成功概率为0。9，那么一个人应该尝试应用它几次，直到取得成功。然而，与规则相关联的度量并不模仿伯努利随机变量。尝试多次相同的我们定义后继函数pSuccR（S）=r∈Rp步骤r（S）给定形式（1）的规则集R和状态S，通过阶跃函数p步骤lhsrhs（S）={SJ|好吧好吧∈p适用lhs（S）<$SJ=（S\（state（m2σ）<$P1σ））<$state（m3σ）<$i knows（m4σ）<$P2σ<$plabel（）}。在这种新的设置中，协议的可达状态集（I，R，AR）是pReach（I，R）=pSuccn（I）。n∈N给定攻击规则AR和状态S，攻击谓词ispAttackAR（S）为真当且仅当规则AR可以应用于状态S，即pAppliedAR（S）/= p。P. Adão等人/理论计算机科学电子笔记164（2006）319此外，给定攻击规则AR，如果ispAttackAR（S）为真，则概率这种攻击的p攻击AR（S）由下式给出p攻击AR（S）=x.x ∈{t|plabel（t）∈S我们现在能够在扩展的Dolev-Yao模型中陈述有限数量会话的入侵者推断问题的概率版本，并讨论定量模型检查算法。定义3.2给定pDY模型中的协议（I，R，AR），概率入侵者推断问题在于确定入侵者是否可以学习某个消息，概率大于或等于p，由AR定义，当协议的s个会话运行时。很容易看出这个问题是NP完全的。首先注意，通过取p= 1，入侵者扣除问题的非定量版本可以简化为这个问题，因此该问题是NP困难的。此外，给定攻击的踪迹（包括入侵者知识的推导），我们可以在多项式时间内检查该攻击是否以大于p.因此，有一个多项式证人验证算法的情况下，可能的攻击。此外，如果没有发生攻击，提供的任何证人（痕迹）都不会导致证实攻击。所以这个问题是NP问题，因此是NP完全的。定理3.3在p-DY入侵者模型中，有限个会话的概率入侵者推断问题是NP-完全的。关于模型检查算法，我们提出的扩展并没有改变定义2.3中给出的伪代码。定义3.4定量模型检验算法的决策版本：qModelCheck（P，p）输入：协议P=（S，R，AR）和概率p输出：如果协议以概率p安全，则为1，否则1. 如果（ispAttackAR（S））≥p，则返回0;2. 对于每个r∈R，计算pApplicablelhs（S），其中r=lhs <$rhs;3. 计算pSuccR（S）;4. 对每个SJ∈pSuccR（S）;5.B=ModelCheck（SJ，R，AR）;6.如果（B==0），则返回0;7. 返回1.我们继续分析定量模型检测算法的复杂性。注意，经典入侵者和概率入侵者需要知道的相关项的数量是相同的，即，深度为20P. Adão等人/理论计算机科学电子笔记164（2006）3大多数K。因此，在最坏的情况下，递归树的状态总数对于经典模型检查器和定量模型检查器是相同的（渐近地），也就是说，时间复杂度：O（nn（nk+i+5）<$2k）=num tot st，其中n=j×s是协议的步骤数j和会话数s的乘积，i是入侵者已知的初始原子消息的数量，v是R和AR中lhs规则中存在的变量的最大数