Maude-NRL协议分析器的等式密码推理及应用

理论计算机科学电子笔记171（2007）23-36www.elsevier.com/locate/entcsMaude-NRL协议分析器中的等式密码推理SantiagoEscobara，1，4 CatherineMeadowsb，2 Jos'eMeseguerc，3aUniversi dadPolit'ecni cadeVale n ci a，Spain.b海军研究实验室。美国华盛顿特区c美国伊利诺伊大学厄巴纳-香槟分校。摘要NRL协议分析器（NPA）是一种用于加密协议的形式化规范和分析的工具，已在许多复杂的现实协议上得到了很好的应用。它最有趣的功能之一是，它可以用来推理安全性，以应对对协议中使用的函数的低级代数属性的攻击。最近，我们第一次给出了NPA推理系统主要特征的精确形式化规范：其基于语法的（共）不变式生成技术及其向后缩小可达性分析方法;两者都在Maude中实现为Maude-NPA工具。这种形式化的规范是在众所周知的重写框架内给出的，因此推理系统被指定为一组重写规则，这些重写规则模描述所涉及的密码符号的行为的方程理论。本文给出了一个高层次的概述Maude NPA工具，并说明了它如何通过一个简单的，但不平凡的，一个攻击的发现基本上需要等式推理的例子，支持等式推理的基础加密基础设施的属性。它还展示了基于规则的编程语言，如Maude和复杂的缩小策略，是如何有用的建模，分析和验证协议。关键词：密码协议验证，等式推理，缩窄，重写逻辑，Maude1引言NRL协议分析器（NPA）[16]是一种用于加密协议的形式化规范和分析的工具，已在许多复杂的现实协议上得到了很好的应用。它最有趣的特性之一是，它不仅可以用来证明或反驳使用标准Dolev-Yao模型的身份验证和保密属性[9]，而且还可以在面对1电子邮件：sescobar@dsic.upv.es2 电子邮件地址：meadows@itd.nrl.navy.mil3电子邮件：meseguer@cs.uiuc.edu4个S.Escobar得到了欧盟（FEDER）和西班牙MEC TIN-2004-7943-C 04 - 02项目、巴伦西亚省赠款GV06/285和欧盟-印度跨文化传播信息和通信技术ALA/95/23/2003/077-054项目的部分支持。1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.02.05324S. Escobar等人/理论计算机科学电子笔记171（2007）23实际上，它已被成功地用于复制或发现许多这样的攻击，从发现基于加密和解密的取消属性的认证攻击[15]，到复制Bellovin对使用密码块链接的封装安全协议版本的攻击NPA一方面，统一模代数性质（例如，加密和解密，连接和解连接）作为使用有限收敛的窄化（即，连续和终止）重写规则集，其中每个规则的右手侧是左手侧的子项或基础项[8]，允许该工具表示未被通常的Dolev-Yao自由代数模型捕获的对象。另一方面，通过使用归纳定义的共不变量来描述入侵者无法到达的状态，从而减少搜索空间的大小的技术允许我们从无限搜索空间开始，并在许多情况下将其减少到有限，从而使我们免于对会话数量进行任何先验限制的要求最近，我们第一次[10]给出了NPA推理系统主要特征的精确形式化规范：它的向后可达性分析方法和基于语法的协不变生成技术。这种错误的规范是在众所周知的重写框架内给出的，因此推理系统被指定为一组重写规则，这些重写规则以描述所涉及的密码符号的行为的方程理论为模。推理系统已经在Maude中实现，我们称之为Maude-NRL协议分析器（Maude-NPA）工具。我们已经使用重写框架来证明一些重要的元逻辑性质，例如其搜索算法的可靠性和完备性，即，该工具将发现用户指定类型的攻击，当且仅当这种攻击存在于模型，以及由语法表征的状态的不可达性，即，由这样的语法排序的急剧的状态空间减少不损害搜索算法的完整性。但是[10]也提供了一个模块化的基础，可以被视为实现长期目标的第一步扩展Maude-NPA的推理系统，以支持在比目前更广泛的代数属性下分析密码协议，最终计划是构建一个考虑到底层密码函数的代数属性的下一代基于重写的分析工具。在第3节中，我们通过演示如何将这些技术应用于类型混淆攻击的分析，说明了密码基础设施的新等式属性可以模块化地添加到Maude NPA类型混淆攻击，首先在[12]中详细讨论，是利用格式中的模糊性来允许攻击者说服主体数据S. Escobar等人/理论计算机科学电子笔记171（2007）2325一种类型（例如，名称）是另一类型的数据（例如， a nonce）。 由于所需的协议模型的详细程度，在密码协议的形式化分析文献中，类型混淆攻击的实际例子很少。此外，大多数现有的协议工具不允许例如将术语的串接与单个术语混淆或者将多个术语与整个术语混淆的可能性。然而，在[17]中，作者描述了一个使用NRL协议分析器来发现这种攻击的例子该攻击针对的是解释协议组域的早期版本[4]，该协议有两个部分，每个部分都以不同的方式使用数字签名消息在早期版本中一种方式是这种数据串可以在以后被解释为另一种类型的签名消息。然而，NRL协议分析器无法对级联的关联性进行建模，这意味着它只能找到其中一种攻击;另一种必须手动找到。在下面的例子中，我们考虑一个更简单的协议，它也会受到类似类型混淆的影响，并展示如何通过向Maude-NPA规范添加有限版本的结合性来处理它。例1.1该协议使用数字签名来实现双方（Alice和Bob）之间的身份验证。该协议涉及发起者 Alice、响应 者Bob 和提供 随机数的服 务器S。我们使 用常见的符 号A<$→B：M来代表使用主体X的公钥对消息M进行的加密由{M}X表示，其中我们假设公钥被所有主体（包括入侵者）所知。使用私钥进行加密用{M}X-1表示，其中我们假设私钥只有其所有者知道。解密是通过公钥和私钥的组合来完成的，即，{M}X只能由知道私钥的主体X解密X−1，{M}X−1 每个当事人都能解密 nonce表示为NX，表示由主体X创建的随机数。协议描述继续如下(i) S<$→A：NS服务器S向A发送随机数。(ii) A <$→B：{NS，S}A−1A将服务器提供的随机数和服务器名称发送(iii) A <$→B：{B，NA，S}A−1然后，A将B的名称、一个新的随机数和服务器在此协议的基于规则的表示中，主体未知的部分由变量表示。也就是说，由于随机数只有王子才知道， 我们说Alice收到消息X并生成消息，sages {X，S}A−1 和{B，N A，S}A-1，Bob收到消息{XJ，S}A-1 和{B，XJJ，S}A−1。如果我们问一个扮演鲍勃的校长是否会感到困惑，26S. Escobar等人/理论计算机科学电子笔记171（2007）23消息{B，XJJ，S}A-1，作为它的第二个消息，就好像它是它的第一个预期消息{XJ，S}A-1，那么我们可以直观地回答否，但我们将假设对消息进行某种类型检查。在协议的实际实现中，类型检查将通过格式检查来实现 如果格式的定义不明确，那么类型检查就不能正确地实现类型可能会混淆。 例如，这是分析中发生的情况GDOI协议。为了进行简单的类型混淆分析，我们将假设，尽管名称具有可识别的格式，因此具有可识别的类型，但随机数却没有。因此，例如，一个名字后面跟着一个nonce可能会与nonce混淆。因此，在本文中，我们不对第一个预期消息{XJ，S}A−1的变量XJ。 在这种情况下，当如果考虑配对（或级联）运算符的结合性，则在所生成的消息{B，N A，S}A-1和期望的消息{XJ，S}A-1之间存在可能的混淆5，即，消息{B，NA，S}A−1可以被理解为作为{B，（NA，S）}A−1或{（B，NA），S}A−1取决于谁接收它。在这个例子中，结合性是协议的密码学属性，为了找到协议中的密码，必须考虑它。然而，众所周知，一般的结合单位化问题可以产生无限数量的单位化器。[2]因此，我们的方法是为多达3个元素提供结合性的近似。另一方面，请注意，这种混淆仅在同时执行协议的两个会话时出现，即，消息{B，NA，S}A-1在一个会话中生成，预期消息{XJ，S}A-1在另一个会议上。这与其他施加几个限制的方法相比是相关的，例如在有限数量的会话的情况下，或者在有限数量的消息或新的nonce的情况下执行协议的近似ProVerif工具[5]允许无限数量的会话，但对新数据执行抽象，因此可以获得虚假攻击。AVISPA工具[1]中的OFMC工具遵循与我们类似的方法，因为它们考虑了然而，他们只考虑有限数量的会话。Scyther工具[7]允许无限数量的会话，并且不对新数据应用抽象，但不考虑加密符号。2Maude-NPA在Maude-NPA中，协议被指定为与串空间非常接近的符号[11]。在串中，由主体对协议的本地执行是由消息序列[msg-，msg+，msg-，.，msg−，msg+]，其中1 2 3k−1 k表示输入消息的节点被分配负号，并且节点表示发送输出消息被分配正号。 股随着时间的推移而进化，5从技术上讲，这种混淆只有在假设变量XJ在预期消息{XJ，S}-1是通用排序消息的变量，而不是排序随机数的变量一并且使得通用排序消息可以包含可变长度的消息，即，变量XJ序列{t1，. ......你好。 ，t k}，其中1 ≤ k ≤ 3。可以是S. Escobar等人/理论计算机科学电子笔记171（2007）2327J因此我们使用符号|把过去和未来分割成一条线，即，[msg±，. ，msg± |msg±，msg±，...，msg±]1j−1j j+1k其中msg±，. 、msg±是过去的消息，并且msg±、msg±、.，msg±are1j−1j j+1k未来消息（msg±是立即未来消息）。一个状态是一组链与入侵者的知识在这一点上。入侵者的知识用两种事实表示：一种是肯定的知识事实，由m∈I表示;另一种是非知识事实，由m∈/I表示，其中m是一种消息表达式。下面的例子说明了状态的概念，其中我们有两个在不同时间位置的链，入侵者知道消息{N，S}A-1，但还不知道消息{B，NA，S}A-1（注意，N是一个变量，其具体变量仍然未知）：[N −，（{N，S}A−1）+|（{B，N A，S}A−1）+]&[零|（{M，S}A−1）−，（{B，N A，S}A−1）−]&{（{N，S}A−1）∈I，（{B，NA，S}A−1）∈/I，K}链通过入侵者在它们之间通信，即， 通过向入侵者发送消息M，入侵者将把它发送回另一个链。当入侵者收到一条消息时，它就会学习它，即，在从具有事实m∈I的过渡中学习消息m，其中它是在其入侵者知识部分（在协议的前向执行中）中的基于事实m∈I的过渡入侵者具有读取和重定向trac的通常能力，并且还可以执行操作，例如，加密、解密、级联等，它收到的信息。入侵者操作是通过入侵者向自身发送消息来描述的，这些消息表示为不同的链，每个链对应一个操作。所有的入侵者和协议链都是符号化描述的，使用变量和常量的混合，因此一个指定可以代表多个实例。对主体的数量、会话的数量、随机数或时间没有限制，即，不执行数据抽象或近似。也可以将运算符的代数性质（密码学和其他）作为方程理论。Maude-NPA的可达性分析基于两个参数：由链表示的协议P，以及语法序列G = G1，.，G mm-1用于减少搜索空间。在Maude-NPA中通过从（不安全的）目标状态SSbad向后缩小搜索来进行分析。状态是（E-）统一的（反向）重写规则，通过缩小模方程理论描述状态转换E. GrammarsG1，.，Gm表示负信息（或共不变量），即，在入侵者无法到达的状态的有限集合中。这些语法在我们的框架中非常重要，因为在最好的情况下，它们可以将无限搜索空间减少到有限搜索空间，或者至少可以大大减少搜索空间。 该工具试图推断该协议对于SSbad是否安全。 如果协议是不安全的，Maude-NPA总是以入侵者学习序列终止，28S. Escobar等人/理论计算机科学电子笔记171（2007）23交换消息序列，提供了足够的时间和内存资源。在这种情况下，语法实际上可以通过减少要分析的状态数量来改善时间和内存消耗。如果协议是安全的，算法通常可以证明它，只要搜索空间是有限的。在这种情况下，语法是关键，并提供了搜索空间的急剧减少，使得无限搜索空间减少到有限搜索空间。如果协议是安全的，但搜索空间是有限的，Maude-NPA将永远运行。这提供了半决策算法。看到[10] 进一步的解释。要分析的协议作为签名包提供给工具，包括符号，排序和子排序信息（参见[19，6]），以及定义协议的链集合P。此外，该工具预期一些种子项1，.，sd nn，用于生成语法G1，.，G m∈，其中m≤n。尽管需要用户提供语法的种子项，但我们正在研究如何自动生成它们。这些种子术语包括1，.，sd n表示用户认为入侵者不知道的知识，并且工具从该知识生成形式语言，例如，，G m表示入侵者无法到达的几个无限状态集。在特定于协议的签名规范中，有一种特殊的消息排序Msg。用户将添加额外的符号，涉及排序消息。一个协议的特殊代数性质可以用符号和一组方程来指定，使得方程的项的排序必须是Msg或更小。在证券分析中，通常需要使用新的不可猜测的值，例如，暂时的用户可以在协议特定的签名中使用一个特殊的排序Fresh来表示它们。sortFresh变量的含义是它永远不会被向后可达性分析期间生成的E-unifier实例化。这确保了如果随机数是使用Fresh排序的变量表示的，它们将永远不会被合并，并且不需要对随机数进行近似然而，该框架是非常容易理解的，并且用户可以指定一些排序为Fresh的常量符号来使用确实可以合并的nonce，即，近似。由于sortFresh的变量以一种特殊的方式处理，因此我们在示例的链定义中明确表示它们，（规则1，...，r k：新鲜）[msg±，...，msg±]，1N其中r1，.，r，k是出现在msg±，...，msg±.1N我们对可以在我们的工具w.r.t.中指定的协议提出了要求用一组方程E来说明代数性质。直觉上，主体可以发送他/她喜欢的任何东西，但是由入侵者或被委托人攻击总是相对于r.t.被简化。 E. 我们→假设一个项t是→→-不可约的，如果它是w.r.t.的标准形式面向版本EE→E，即， E中的任何规则都不能应用于t。 我们说，项t是强→→-E不可约的，如果对任意代换σ和变量x使得σ（x）→→-不可约，E则σ（t）是→→-不可约的。然后，我们对协议E出现在可达性和语法生成阶段S. Escobar等人/理论计算机科学电子笔记171（2007）2329必须是强→→-不可约的，除了串中的输出消息（即，（m+）E以及肯定的知识事实（即， m∈I）。我们框架的另一个重要方面是，入侵者可以学习的一切都必须通过链学习，即，入侵者在初始状态下一无所知然而，这不是一个限制，因为我们可以为入侵者在初始状态下能够知道的任何消息M编写串[M+3用等式推理3.1方案规范继续例1.1，我们可以用n（X，r）表示随机数NX，其中r是排序为Fresh的变量。两个消息的连接由运算符表示，例如，n（A，r）;n（B，RJ）.用主体A的公钥对消息M的加密由pk（A，M）表示，例如， {NS，S}A表示为pk（A，n（S，r）;S）。用私钥对消息进行加密由sk（A，M）表示，例如，{N S，S}A−1记作sk（A，n（S，r）; S）。所有主体的名称都是固定的，因为它们只是角色，入侵者用常量i表示。唯一的密钥操作入侵者可以对已知消息m执行ISk（i，m）。定义协议的顺序排序签名如下：a：→名称b：→名称s：→名称i：→名称pk：Name×Msg→Encsk：Name×Msg→Encn：Name×Fresh→Nonce; ：Msg×Elem → Msg; ：Msg×Msg →Msg以及以下子排序关系名称随机数Enc Elem Elem消息<<使用E中的以下等式来描述加密/解密消除特性：pk（K，sk（K，M））=M sk（K，pk（K，M））=M其中K是排序Name的变量，M是排序Msg的变量。现在我们讨论连接运算符的代数性质。明显的要求是使;联想。然而，众所周知，一般的结合单位化问题可以产生无限多个单位化器[2]。这可能会导致我们的缩小算法中出现无限分支，并阻止Maude-NPA的终止我们的方法是通过结合论的一个较弱的子理论提供一个合理的近似，该子理论具有一个有限的统一算法。我们通过利用我们规范的有序结构和使用众所周知的窄化结果来实现这一点30S. Escobar等人/理论计算机科学电子笔记171（2007）23我们加到E上的结合性较弱的例子是等式6X;（Y;Z）=（X;Y）;Z其中变量X，Y，Z的排序为Elem。请注意，通过将E中的这个和前面的方程从左到右定向而获得的规则提供了一个连续的、终止的和排序递减的项重写系统。然后众所周知，基本窄化[13]提供了一个健全和完整的E-统一算法，如果E中每个方程的右手边是构造项7，左手边的子项或基础项[8]，则该算法是无限的。注意，加密/解密方程满足此要求。我们的结合性方程也是如此，因为当变量X，Y，Z是类Elem项（X;Y）时;Z是一个构造器项，因为重载类型;：Msg×Elem→Msg是一个构造器操作符，在脚注7中解释过。因此，窄化为我们的理论E提供了一个有限的E-统一算法。我们的结合方程当然是完整的结合论中一个非常严格的子理论，但它有一个重要的优点，即与加密/解密方程一起，通过基本的窄化产生一个有限的E-统一算法。使用顺序排序技术，我们可以类似地定义越来越多的表达有界结合理论，对于任何n≥3，最多n个元素这些理论的优点是，通过与这里给出的n= 3的论证类似的论证，它们通过缩窄的统一算法都是无穷的;见脚注6。在下文中，变量M、MJ、M1、M2、MJ、MJ都是Msg，变量1 2X，Y，Z的排序为Elm，变量N的排序为Nonce，变量r，rJ，rJJ，rJJJ的排序为Fresh，变量A的排序为Name。 注意，强→→-不可约E要求意味着没有pk（A，M）-，sk（A，M）-或（W;M）-形式的输入消息可以出现在协议的串中，其中A是排序为Name的变量，W是排序为S s. t的变量。S≤Msg，且M是排序Msg的变量。例如，pk（A，M）−中的M可以实例化为sk（A，MJ），则pk（A，sk（A，MJ））−不是→→-不可约的。 与图1所示的三个方案步骤相关的链PE示例1.1如下，协议中的每个主体（或角色）一个(s1)（r：新鲜）[n（s，r）+]这个串表示服务器向主体发送一个随机数。（s2）（rJ：Fresh）[N−，sk（a，N;s）+，sk（a，b;（n（a，rJ）;s））+]这条链表示主体a从主体接收随机数，然后[6]请注意，逆方程（X;Y）;Z=X;（Y;Z）作为本例的规则并不有用，因为必须将sk（a，b;（n（a，r）;s））项转换为sk（a，（b;n（a，r））;s）。此外，这种反向方程将使E-统一过程难以处理（即，因为我们可以通过缩小规则X;（Y;Z）→（X;Y）;Z然后规则（X;Y）;Z→X;（Y;Z）无限次地应用7构造函数术语是仅由构造函数符号和变量构成的术语。 给定一组重写规则s l1→r1， . .... . . 你 好 。 ，ln→rnoververamamanyny-sortedsignaturerebooks，afunctionionsymbolf：s1×. . . ×sn−→s在n中被称为构造函数，如果它不出现为任何左手边l 1，.的根符号。..，l n.在顺序排序的上下文中，这个概念有点微妙，因为符号f可以被重载，并且可以是某些类型的构造函数（在没有规则适用于它的意义上）和其他类型的定义符号。 也就是说，符号f确实可以出现在左手边l i，但它永远不可能出现在左手边li。类型是f的构造器版本。我们用结合性公理来说明这个微妙的观点。S. Escobar等人/理论计算机科学电子笔记171（2007）2331发送用他的私钥加密的两条消息，一条消息具有接收到的随机数和服务器(s3)[sk（a，M;s）−，sk（a，（b;N）;s）−]这个串表示主体b接收两条消息，他/她在第一条消息中查找名字s，在第二条消息中查找名字b和s以下几个部分描述了入侵者根据Dolev-Yao攻击者（s4）[M-，M-，（M1;M2）+]级联1 2(s5)[（M1;M2）−，M+，M+]解级联1 2(s6)[M-，pk（A，M）+]使用公钥的加密（s7）[M-，sk（i，M）+]使用私钥的加密如上所述，在我们的框架中，表示入侵者无法到达的几个无限状态集的语法非常重要，因为它们表示将用于减少搜索空间的负面信息（共不变量）在这种情况下（以及许多其他情况下），语法将无限搜索空间减少到有限空间。例如，通过在有限向后收缩中捕获以下内容，序列9：m~（M;m）~（MJ;M;m）~111···由Dolev-Yao链产生的用于上文所示的解链。 我们描述下面的语法生成。更详细的描述见[10]。3.2语法生成Maude-NPA从种子项开始，种子项表示用户认为入侵者不知道的知识。只有两种类型的种子项：（i）t → t∈L，表示Msg类的项t对于具有任意约束的入侵者是未知的，以及（ii）t|p∈/I<$→t∈L，如果子项t|p肯定是未知的，即，，提供了这一事实|p∈I是我们将在每个时刻处理的协议的状态的新的知识。例1.1的具体种子项如下：sd1<$M1<$/I<$→（M1;M2）<$L sd2<$M2<$/I<$→（M1;M2）<$Lsd3<$M<$/I<$→sk（A，M）<$Lsd4<$M<$/I<$→pk（A，M）∈L它们被理解为初始语法，例如，的 语言产生M∈/I<$→pk（A，M）∈Ldenote是一个任意矩阵的任意形式[8]请注意，我们简化了入侵者规则w.r.t.。[9]见[10，实施例3]的进一步细节。[9]为了便于阅读，我们故意省略了重写理论RP=（RNP，RP，EP），用于可达性阶段的每个缩窄步骤~RP，EP中使用的链;更多细节参见[10]我们还省略了额外的链信息，只编写入侵者要学习的相关消息，即，所有的作为输入消息m-出现在串中的消息。32S. Escobar等人/理论计算机科学电子笔记171（2007）23pk（t1，t2）使得子项t1的排序为Name，并且入侵者不知道而SortMsg.Maude-NPA生成语言的策略包括三个阶段。术语生成。在这个阶段，Maude-NPA采用由语言产生式定义的每个项，并通过向后缩小找到到入侵者知道该项的状态的路径的完整集合S例如，对于种子项sd1和sd2，我们有以下向后缩窄步骤10，其中我们指示串在该步骤中涉及变量M1、MJ、M2、MJ都是Msg类型的，变量1 2X、Y、Z是Elm类的：（M1;M2）~id，s4M1，M2（M1;M2）~[M1/（X;Y），M2/Z]，s4X，（Y;Z）（M1;M2）~id，s5MJ;（M1;M2）（M1;M2）~id，s5（M1;M2）;MJ1 2（M1;M2）~id，s7pk（i，（M1;M2））（M1;M2）~id，s6sk（A，（M1;M2））直觉上，步骤（M1;M2）~id，s4M1，M2意味着为了使入侵者学习消息（M1;M2），他/她需要在协议的先前状态中学习消息M1和M2步骤11（ M1;M2）~[M1/ （ X;Y ） ， M2/Z] ， s4X，（Y;Z）意味着入侵者必须学习消息X和（Y;Z）才能向主体发送消息（（X;Y）;Z）规则验证。在该阶段中，Maude-NPA检查每个路径并确定哪些路径已经被语法捕获，即，这些路径已经要求入侵者知道该语言的成员以便产生目标。该工具将这些路径从考虑中删除。对于一个例子，期望看到目标ms d1<$M1∈/I<$→（M1;M2）∈L和向后收缩步骤（M1; M2）~id，s4M1，M2，我们有一个矛盾，因为入侵者必须学习消息M1，但我们有一个约束，即该目标不知道M1（即，，M1∈/I）。 我们有一个相似的约束条件，即给定的终端sd2<$M2∈/I<$→（M1;M2）∈L，终端p（M1;M2）id，s4M1，M2，以及消息M2。 对于步长（M1;M2）~[M1/（X;Y），M2/Z]， s4X，（Y;Z），如何-[001 pdf 1st-31 files]项（Y;Z）属于种子项sd2的语言，因此，我们都在移动。通过在M2 ∈I→（M1;M2）∈ L上的线性代数方程组，Z ∈ I使s（Y ; Z）∈L. 对于这些预处理块，没有一个是分别由与sd1或sd2相关联的形式语言捕获的，因此没有一个是被区分的。[10]同样，为了便于阅读，我们故意省略了在语法生成过程中的每个缩减步骤中使用的重写理论RSP=（RSP，RSP，ESP）重写理论RSP是重写理论RP在语法生成阶段的简化，并且是从它自动获得的;参见[10]了解更多细节。11Onecould出口到 欧 洲的 货 物这斯德 普（ M1;M2 ）~[M1/ （ X;Y ） ， M2/Z] ， s4（X;Y）， ZI ns teadof （M1;M2 ）~[M1/ （ X;Y ） ， M2/Z] ， s4X，（Y;Z ）。然 而 ，这E-unificationproblemconsiderd 他说，是（M1;M2） =E（MJ;MJ）， 其中，当初始化为PP规则（MJ;MJ）时， →MJ， MJ1 2 1 2 1 2（其中该值是从存储器4获得的，并且存储在RSP中）到（M1;M2）。这是一个...unif iris[M1/（X;Y），M2/Z，MJ/X，MJ/（Y;Z）]，其中h是通过应用该更新规则获得的→1 2X;（Y;Z）→（X;Y）;Z（存储在E中）到项（MJ;MJ）。1 2S. Escobar等人/理论计算机科学电子笔记171（2007）23331211122直觉，在这阶段，消息X，（Y;Z），（MJ;（M1;M2））、（（M1;M2）;MJ）、pk（i，（M1;M2））和sk（A，（M1;M2））尚未被定义为sd1语言的成员，因此这些路径保留在下一阶段。类似地，消息（MJ;（M1;M2））、（（M1;M2）;MJ）、pk（i，（M1;M2））、1 2和sk（A，（M1;M2））对于种子项sd2保持在。规则生成。在规则生成阶段，Maude-NPA查看剩余路径，并根据一组语法生成一组新的语法规则。我们有四种策略H1，H 2a，H 2b，H 3，它们根据两种全局策略S1和S2使用。（H 1）这种启发式扩展了语言，本质上是寻找可以被它捕获但没有被捕获的术语。例如，关于向后缩小步骤（M1;M2）~id，s5MJ;（M1;M2），我们得到消息（MJ;（M1;M2））被入侵者从消息（M1;M2）中学习，并且由于（M1;M2）已经在sd1的语言中并且是（MJ;（M1;M2）），我们添加一个语法规则Y∈L <$→（MJ;Y）∈L，它允许1 1新语法来捕获消息（MJ;（M1;M2））。类 似 地，我们从缩窄步骤（M1;M2）~ id生成语法规则Y∈L<$→（Y; MJ）∈L，从缩窄步骤（M1; M2）~ id生成语法规则Y ∈L <$→ pk（i，（M1; M2）），从缩窄步骤（M1; M2）~ id生成语法规则Y ∈L<$→ pk（i，Y）∈L，从缩窄步骤（M1; M2）~ id生成语法规则Y∈L<$→sk（A，Y）∈L从缩窄步骤（M1;M2）~id，s6sk（A，（M1;M2））。（H2 a）这种启发式限制了语言。 它检测到存在约束u∈/I，该约束必须由该压缩的E-uni_i_r来初始化d。 这意味着入侵者可能会学习一些部分数据（由统一引入的符号），因此这些部分数据应该从语言中排除。对于缩窄步长（M1;M2）~[M1/（X;Y），M2/Z]， s4X，（Y;Z），约束M1∈I被实例化，因此我们引入约束M1（X;Y），其中X，Y是Elm类的变量。（H2b）这种结构的检测器也包含入侵者学习的对象，并将它们从语言中排除。 对于窄化步骤（M1; M2）~[M1/（X; Y），M2/Z]，s4 X，（Y;Z），我们引入约束（M1;M2）（（X;Y）;Z），其中X，Y，Z是Elm类的变量。 H2a的使用H2b在下面解释。（H3）该启发式算法扩展了现有文法G，但使用了约束u∈/I. 例如，当期望步骤p（M1;M2）=id，s7pk（i，（M1;M2））和步骤d1时，在M1∈/I中有一个角。如果M1不为入侵者所知，并且是消息pk（i，（M1; M2））的真子项，则pk（i，（M1; M2））一定不为入侵者所知. 因此，我们可以使用一个语法规则Y∈/I<$→pk（i，（Y;M2））∈L;但这并不意味着我们在最终文法中不真正包括这样的语言产生式，因为启发式H1的应用排除了启发式H3。按照以下全局策略S1或S2之一来应用这些策略。对于策略S1，按以下顺序应用语法：尝试H1，如果失败，则尝试H2a，如果失败，则尝试H3，否则停止该语法的整个语法生成过程。策略S2类似于S1，但尝试H2b而不是34S. Escobar等人/理论计算机科学电子笔记171（2007）23SDSD1H2a。策略S2和S1之间的差异（即，与策略S1相比，策略S2生成更多的受限语法，从而减少了术语，提供了更大的形式语言。 然而，战略S1可以是一个位于具有整数S2的整数序列中的p列，因为使用了∈/I的整数序列对于启发式H2a.因此，对于形式为t →t∈L的种子项，只有策略S2可以是有效的，而对于这一点，|q∈/I<$→t∈Lit通常最好从策略S2开始，如果失败，则尝试策略S1。在规则生成阶段之后，Maude-NPA重复这三个阶段，直到在规则验证阶段消除所有路径，在这种情况下，它成功地定义了一种语言，或者在规则生成阶段不能定义新的语言规则，在这种情况下，它未能定义一种语言。它也可能永远无法终止添加新规则。见[10]语法的例子，不能定义一个语言或不能终止。该工具生成以下语法G！1！sd2！sd3，G！4，分别为-使用策略S1：（g1.1）M∈L <$→pk（i，M）∈L（g2.1） M∈L <$→pk（i，M）∈L（g1.2）M∈L <$→sk（A，M）∈L（g2.2） M∈L <$→sk（A，M）∈L（g1.3）M2∈L<$→M1;M2∈L（g2.3） M2∈L<$→M1;M2∈L（g1.4）M1∈L<$→M1;M2∈L（g2.4） M1∈L<$→M1;M2∈L（g1.5）M1∈/I，M1n（a，r），M1（b;n（a，rJ））<$→M1;M2∈L（g2.5）M2∈/I，M2n（a，r），M2（n（a，RJ）;s）<$→M1;M2∈L（g3.1）M∈L <$→pk（i，M）∈L（g4.1） M∈L <$→pk（i，M）∈L（g3.2）M∈L <$→sk（A，M）∈L（g4.2） M∈L <$→sk（A，M）∈L（g3.3）M2∈L<$→M1;M2∈L（g4.3） M2∈L<$→M1;M2∈L（g3.4）M1∈L<$→M1;M2∈L（g4.4） M1∈L<$→M1;M2∈L（g3.5）M∈/I，M（（b;n（a，r））;s），（g4.5） M∈/I<$→pk（A，M）∈LM（N;s）›→sk（A，M）∈L例如，语法规则g3.5规定，如果子项M在前一个语法规则的执行时不被入侵者知道（即，，条件M∈/I是对这种状态的基本知识），并且消息M不是（b;（n（a，r））;s或N;s的形式。请注意，在这种情况下（以及许多其他情况下），语法将无限搜索空间减少到有限空间。例如，捕获以下有限向后收缩序列sk（a，（b;N）;s）~（M1;sk（a，（b;N）;s））~（MJ;M1;sk（a，（b;N）;s））~···因为表达式（M1;sk（a，（b;N）;s））属于种子项sd2的语言。也就是说，（M1;sk（a，（b;N）;s））由语法产生式g2.5捕获，因为facsk（a，（b;N）;s）选项卡页面上创建选项卡页面上创建S. Escobar等人/理论计算机科学电子笔记171（2007）2335∈/I是根据新的语法规则kabackardge而被重写的36S. Escobar等人/理论计算机科学电子笔记171（2007）23缩窄步骤sk（a，（b;M）;s）~（M1;sk（a，（b;M）;s））。3.3向后可达性分析作为系统输入的最终状态攻击模式为：[sk（a，M; s）−，sk（a，（b; N）; s）−|nil]&{K}其中链处于其最终位置（即，每个消息都是过去的），M是Msg类的变量，N是Nonce类的变量，K是表示入侵者知识的变量。请注意，M是Msg排序而不是Nonce排序，是混淆攻击的关键事实，参见脚注5。入侵者知识在向后可达性过程中是必不可少的，因此变量K将被适当地实例化;有关详细信息，请参见[10我们的工具能够找到协议的以下初始状态：[零|n（s，r）+]&[nil|n（s，r， J）+]&[零|n（s，r）−，（s k（a，n（s，r）;s））+，（s k（a，b;（n（a，rJJ）;s）+]&[零|n（s，rJ）−，（s k（a，n（s，rJ）;s））+，（s k（a，b;（n（a，rJJJ）;s）+]&[零|（s k（a，（b;n（a，rJJ））;s））−，（s k（a，（b;n（a，rJ JJ））;s））−]&{n（s，r）∈/I，n（s，rJ）∈/I，sk（a，（b;n（a，rJJ））;s）∈/I，sk（a，（b;n（a，rJJ））;s）∈/I}其中r、rJ、rJJ、rJJJ是排序变量Fresh，所有链都处于其初始位置（即，每个消息都在将来），并且入侵者不知道，但是它将学习在协议运行中交换的四个消息请注意，sk（a，n（s，r）;s）和sk（a，n（s，r，J）;s）是入侵者不感兴趣的具体消息交换顺序为：n（s，RJ）+. n（s，rJ）−. sk（a，n（s，rJ）;s）+. sk（a，b;（n（a，rJJJ）;s））+. n（s，r）+.n（s，r）−. sk（a，n（s，r）;s）+. sk（a，b;（n（a，rJJ）;s））+. sk（a，（b;n（a，rJJ））;s）−. sk（a，（b;n（a，rJJJ））;s）−4结论我们已经提出了一个高层次的概述重写为基础的形式化的NPA的可达性分析和语言生成机制，我们称之为Maude-NPA。我们已经说明了它的使用，在超出Dolev-Yao完美密码学或有限会话数假设的情况下，通过一个协议的攻击，只能通过考虑底层密码基础设施的等式属性来发现：在我们的例子中，消息级联运算符的as-sociativity。Maude-NPA原型已用于此示例，既用于生成语法又用于查找攻击。正如引言中所指出的，这项工作是长期研究项目中的第一步，该项目旨在使用类似NPA的机制分析协议，其中攻击可能利用底层加密函数的代数属性。例如，我们正在努力扩展Maude-NPA，S. Escobar等人/理论计算机科学电子笔记171（2007）2337能力模方程理论，其中存在无穷统一算法，例如，结合性-交换性，布尔理论和某些形式的模幂运算[18，14]。引用[1] Arm anddo，A.，D. A. Basi n，Y. Boi chut，Y. Chevali er，L. 来吧，J。 你会没事的。H. Dri elsma，P.- C. 嗨，奥。 Kouchnare nko，J. 我不能去，S。 M？oder s heim，D. 他在我身边，M。 我们现在不和你在一起了，J。很久以前，M. 图鲁安湖; Vigano`andL. Vi gneon，AVISPa ol o rauto to ，in：K. Etessami和S. K. Rajamani，编辑，CAV，Lecture Notes in Computer Science3576（2005），pp. 281-285[2] Baader，F.和W. Snyder，Unification Theory，in：A. Robinson和A. Voronkov，