Dolev-Yao约束的可满足性及其应用

理论计算机科学电子笔记125（2005）109-124www.elsevier.com/locate/entcsDolev-Yao约束LaurentMazar'e1VerimagGrenoble，法国摘要在一定的假设下，保密问题等价于涉及Dolev-Yao算子的约束的满足性。对这些约束条件进行适当的限制，证明了它们的可满足性是NP完全的。然而，为了检查不透明性[11]或一些修改版本的保密性，需要为更大类别的谓词找到类似的结果。本文开始扩展这个可判定性的结果，更一般的限制，特别是允许不平等，并给出了一个简单的决策过程的重写系统的基础上。关键词：安全性，形式验证，Dolev-Yao约束，重写系统，不透明性。1介绍在过去的十年中，安全协议的验证得到了广泛的研究。大多数研究都集中在使用形式化方法证明保密性（参见例如[4]，[6]，[5]或[9]）。这些方法已经导致了有效的算法，从而产生了用于验证保密性的具体工具，如EVA项目[3]或Avispa项目[2]提出的那些。主要结果是：在Dolev-Yao模型（见[ 8 ]）中，考虑一个主动入侵者和有限个会话数，秘密是可判定的，是一个NP完全问题。证明这个结果的一种可能的方法是使用基于Dolev-Yao算子的约束。这一点在[12]或[14]中都有体现。Dolev-Yao约束是EDm形式的原子约束的合取，其中E是一个环境（即一个有限的消息集），m是一个消息，它们都可能是不封闭的。1电子邮件：laurent. imag.fr1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.05.022110L. Mazaré/Electronic Notes in Theoretical Computer Science 125（2005）109因此，在这种情况下，保密问题等价于给定约束的满足性。本文在给出Dolev-Yao约束的形式化定义后，研究其满足性. 在第一部分中，我们将把自己限制在“良构”约束中。这些约束将形成众所周知的约束集的扩展，其满足性完全等同于具有有限会话数的Dolev-Yao模型中的这个扩展将增加使用/=运算符的可能性。因此，检查接收到的变量不是给定变量的协议（例如，验证随机数以前没有使用过的协议）可以通过检查这种约束的满足性来验证。利用一种基于项重写的方法，证明了这种约束的满足性是可判定的，并给出了具体的判定算法。此外，其中一个关于良构约束的假设可以被移除。这将定义准良构约束，其满足性也将被证明是可判定的。除了协议检查不等式之外，在扩展经典Dolev-Yao约束时还有两个主要动机。第一个，导致良构的定义，是在主动入侵者的情况下研究不透明性[11]而不是保密性。在这种情况下，不透明度将等同于良构约束的可满足性。定义“准良构”约束的标准这些约束的另一个用途是对两个不允许通信的不同入侵者进行的攻击进行建模。应用程序，这些限制不透明度将不完全详细在这里，将是一个未来的文件的对象本文的其余部分组织如下。在第2节中，我们将简要回顾导致Dolev-Yao约束的通常定义，并给出良构和拟良构的适当定义。然后，在第3节中，我们将使用重写系统来证明良构约束的满足性是可判定的。第四节将把这个结果推广到拟良型约束的情形。在第5节中，我们将快速解释为什么约束的满足是NP完全的。第6节将展示如何将这些结果 最后，第7节将结束本文。2Dolev-Yao约束设A，X，F是三个不可数的不相交集合。A是原子消息的集合，通常写为a，b等。X是消息变量的集合（写为x，y，.）而F是函数的集合（写作f，g，...）。L. Mazaré/Electronic Notes in Theoretical Computer Science 125（2005）109111定义2.1设f是签名Af {pair，encrypt}F，其中pair和encrypt是两个二进制函数。原子消息假设是常数函数，每个函数f都有一个固定的arityar（f）。那么一个消息是一个在X和变量集合X上的一阶项，即T（X，X）的一个元素。 如果一个消息是T（X，X）的闭项，即T（X）的项，则称该消息是闭的。在本文的其余部分，我们将使用众所周知的符号<$m1，m2<$=pair（m1，m2）和{m1}m2=encrypt（m1，m2）。消息m的高度可以很容易地递归定义，并将被记录下来。|M|.消息m中使用的变量集记为var（m），这不是var的通常定义，因为我们将考虑f（. ）是var（a）=0var（x）={x}var（f（. ））=var（m，n）=var（m）var（n）var（{m}n）=var（m）var（n）从X到T（X，X）的置换σ按通常定义。 的应用消息m的σ将被记为mσ（而不是σ（m））。如果σ由xσ=n和yσ=y定义，对于任何其他变量y，那么我们可以写m[x\n]而不是mσ。置换的定义域σ是变量的集合dom（σ），使得xσ x。使用pair运算符，可以引入n元组。 那就使用tn符号表示使用n次相同消息组成的元组t. 形式上，tn递归地定义为t1=t和tn+1=t，tn我们将使用Dolev-Yao入侵者模型[ 8 ]。入侵者控制网络：他可以拦截任何消息，利用其初始知识和先前拦截的消息伪造消息，并将这些消息发送给其他代理，盗用代理的身份。为了伪造新的信息，入侵者使用Dolev-Yao理论。如果E是一个有限的消息集（通常称为环境），m是一个消息，Em意味着可以使用经典推理从E推导出m。在本文中，我们只考虑对称密码。然而，当考虑公钥密码学时，我们所有的结果仍然成立，但为了简单起见，我们将保留这个假设。Dolev-Yao约束是用经典逻辑算子和一个新的三级算子D.该运算符用于原子谓词，如TDm[U]，其中T（环境），m（消息）和U（环境）可以是非封闭的。这个谓词112L. Mazaré/Electronic Notes in Theoretical Computer Science 125（2005）109Tm[U]，除了解码规则之外，它被定义为经典的符号。T<${m}u[U]u∈UT<$m[U]唯一允许解码消息的密钥是U中的密钥，并且这些密钥不能被证明是可推导的。定义2.2[约束] Dolev-Yao约束根据以下语法定义：C：：=|不|CC|C C|CACA：：= T D m [U] |m/= n其中T和U是有限的消息集合，m和n是消息。对于一个约束C，出现在C中的原子约束TDm[U]的左部的集合T称为C的环境。模型的经典概念用于像“=”这样的运算符。 我们将扩展它，说σ是TDm [U]的模型，记为σ| = TDm [U] i <$T σ，mσ和Uσ是闭的，并且存在Tσ<$mσ [Uσ]的证明.定义2.3 [模型]置换σ是约束C i的模型，Cσ是闭的，且σ| = C，其中σ| =. 是验证关于T，和的经典推论以及以下两个推论的最小谓词：mσ/= nσσ| = m/= nTσ<$Tmσ[Uσ]σ| = TDm [U]使用标准的边界规则，任何约束都可以转换为C=其中Coi=CA。 Coi约束称为合取组成C. 我们通常假设约束遵循以下形式因为需要检查它们是格式良好还是准格式良好。定义2.4[良构约束]一个约束C被称为良构，如果没有一个环境是空的，并且对于构成C的任何合取Co，以下两个条件成立：• 如果TDm[U]和TJDmJ[UJ]在Co中，则T<$TJ或TJ<$T（环境包含）。• 若TDm[U]∈Co且x∈var（T），则存在TJDmJ[UJ]∈Co使得x∈var（mJ），UJ<$U且TJ<$T（变量引入）.L. Mazaré/Electronic Notes in Theoretical Computer Science 125（2005）109113仅满足变量引入要求并且在其所有环境中存在相同的封闭消息m的约束将被称为准良构的。很 容 易 注 意 到 ， 对 于 合 式 约 束 中 的 合 取 ， 在 Co 中 存 在 一 个 约 束TxDmx[Ux]，使得Tx是最小的，并且x∈var（mx）。下面将使用该符号Tx关于Tx的直接性质是x∈/var（Tx）。此外，我们还可以注意到，任何良构约束都是准良构约束。由于我们现在对Dolev-Yao约束有了适当的定义，我们将给出一个非常经典的约束例子。为了实现这一点，能够形式化经典的Dolev-Yao约束是实用的：消息m可以从写为TDm的消息T的集合中推导出来。这个约束可以通过量化密钥被泄露的顺序，使用带有[]的约束来描述。m将是可推导的i如果存在k1，...，在T或m中有kn个不同的键，使得k1可以不用任何解码就推导出，k2可以只用k1推导出，以此类推。最后，m需要只用键k1到kn从T推导出。命题2.5设m是一个消息，T是一个有限的消息集合。然后，对于任何置换σ，以下等价成立。Tσmσ惠σ |=k 1，...，kn∈keys（T，m）（T D k1 [] T D k2 [k1]. T D m [k1，.， kn]）这个属性可以扩展到带有多个D运算符的谓词。如果谓词的环境是有序的，则可以假设键对环境T的妥协是对TJ的妥协，验证TTJ。让我们称之为T1和T2的环境. Tn. 因此，我们在之前的顺序是k1，...，kα，并且对于每个环境Tj，对于T j中的ij 的 值 ，k∈k1到kij都是一致的（并且，我们必须考虑i1≤i2≤. ≤in）。命题2.6F或i在1和n之间，设mi是一个消息，Ti是有限的一组信息。 若1≤i≤nTiσ D mi是良型的且T1<$T2<$. 那么，对于任何置换σ，下列等价成立。1≤i≤nTiσmiσ惠σ |=k1，...，k α ∈ keys（T，m）1≤i1 ≤ i2≤. ≤in ≤n（T1D k1 []. T 1D m1 [k1，.， ki1]）n（T2D ki1 + 1 [k1，...， ki1]. T 2D m2 [k1，.， ki2]）我...（TnD kin−1+ 1 [k1，.， kin−1]. T nD mn [k1，.，kin]）114L. Mazaré/Electronic Notes in Theoretical Computer Science 125（2005）109C这个性质给出了以下结果：保密性等价于一个形式良好的Dolev-Yao约束的满足性。Needham-Schroeder约束Dolev-Yao模型中会话数有界的秘密可以与良构约束的满足性联系起来。 这在[7]中有解释。可以使用形式化方法发现的攻击的通常例子是Lowe在1995年发现的对Needham-Schroeder协议的攻击[13]。满足性等价于这种攻击存在的约束NS如下所示。由于它描述了Dolev-Yao模型中的攻击，因此环境描述了入侵者的知识，从而验证了环境包含和变量引入。这就是为什么，这个约束是格式良好的，它的满足性可以被验证。这里考虑的两种情况发生在A和入侵者C之间，以及C篡夺A为了尽可能简单，这个例子使用了公钥加密。设E为入侵者的初始知识C，E ={A，B，C，KA，KB，KC，K−1}。NS=E，{NC，A}KCE， {NC，A}KD{x，A}K，{x，NB}KD{NC，y}KCC， {NC，A}KC一，{x，NB}KA，{y}KC一DNB3形式良好约束在本节中，我们将提供一个原始的决策过程，以满足良构约束。对于只使用D的约束，众所周知，满足性问题是NP完全的：例如参见[14]，[12]或[7]中XOR的扩展。我们的决策过程将使用重写系统的约束。我们必须证明我们的系统是终止的，我们的规范形式的可满足性是可判定的，并且最终证明我们的系统是正确的和完备的，也就是说，一个约束的模型就是这个约束重写后的模型。知道了这一点，我们就能够提供一个满足性的判定过程，即把约束重写到它的范式，然后在这个范式上检查满足性与这种约束的可判定性证明（在文献中很容易找到，参见[12]作为起点）相比，我们的主要目标是提供一个非常简单但可扩展的决策过程。重写系统的定义需要一些解释。我们的重写系统是由条件触发的。由于我们将检查终止而不考虑该条件，因此这不会导致任何问题。第一步BL. Mazaré/Electronic Notes in Theoretical Computer Science 125（2005）109115我们的决策过程是测试不同环境和消息的子项之间的所有可能的统一。这是使用一个大的量化（quantitation）来完成的。在这一步之后，两个不同的非封闭消息（原始约束的子消息）应该用不同的封闭消息实例化（即它们不能被统一）。利用这一点，一个原子a可以从T（利用U）推导出来，ia出现在T中（只受出现在U中的键的保护）。 同样的想法也用于{}，而对于{}的情况则是微不足道的。定义3.1重写系统→通过以下三个规则在良构约束上定义，这些规则仅适用于对所有x∈var（T），TxDx[Ux]与Ux<$U发生相同的结合。(1)TDa[U]→T(2)TDa[U]→ A(3) T D f（m1，.， mn）[U] →T(4) T Df（m1，.， mn）[U] →(5)TDm，n[U]→TDm[U]<$TDn[U](6)TD{m}n[U]→T(7)TD{m}n[U]→TDm[U]<$TDn[U]• 规则1在T中出现时被应用，T只受U中出现的键的保护，否则规则2被应用。• 规则3被应用于i = f（m1，...，mn）只受出现在U中的键的保护，否则应用规则4。因此，如果我们把原子看作常数函数，则规则1和规则2是无用的。• 规则5是配对的直观规则。• 如果{m}n出现在T中，并且只受出现在U中的键的保护，则应用规则6（这是可以使用分解获得{m}n的情况），否则应用规则7（在另一种情况下，{m}n是使用合成操作获得的）。在T上表示的条件旨在强制执行命令- 是的因此，如果T1≠T2，则在处理T2 D m 2之前，模式T1Dm1将被完全重写。最后，这些规则很容易扩展到公钥密码学的情况。在这种情况下，在应用不同规则的条件下，首先要检查的是，在将→应用于良构约束之后，结果仍然是良构的。这可以用以下方式表示116L. Mazaré/Electronic Notes in Theoretical Computer Science 125（2005）109财产命题3.2如果C和CJ是约束使得C→CJ且C是良构的，则CJ是良构的。第二件事是证明我们的重写系统终止。然后，可以将任何约束转换为具有完全相同模型的标准形式的约束。这很容易表现出来，因为在重写时，每个约束的正确成员被分解，或者约束被重写为埃克塞特湖 因此，通过对约束s（C）进行简单的测量，定义为：卢恩s（T1D m1 [U1] s... T nD mn [Un]）=i=1s（mi）这就给出了s（T）=s（T）= 0。 而s在消息上递归地定义为：s（a）= 1s（f（. ））= 1s（m1，m2）=s（m1）+s（m2）+1s（{m1}m2）=s（m1）+s（m2）+1使用基于此度量的顺序，以下属性是立即的。命题3.3重写系统→终止。在将约束转换为其范式之后，我们要检查两者是否具有相同的模型集。形式上，如果C→Cj，则对任何置换σ，σ是Ci的模型，σ是CJ的模型。 这将证明，如果标准形式满足，那么原始约束也满足，倒数是真的命题3.4重写系统→对于良构约束是正确和完备的.注意，为了证明这个结果，使用了变量引入假设。否则，规则就不再是正确和完整的了。例如，如果我们考虑以下约束：a，{b}aDx[a]a，{b}a，xDb[]这个约束将被重写为a，因为b不会出现在a，{b}a，x中。但是，通过使用x=b，我们知道这个约束是可满足的。这就是为什么大多数规则只有在变量引入假设得到尊重的情况下才是正确和完整的。最后，最后一步是证明我们的正规形式的可满足性是容易判定的。首先，格式良好的约束的范式是良好的-L. Mazaré/Electronic Notes in Theoretical Computer Science 125（2005）109117形成了约束。 它们具有以下形式：.Σ（TDx[U]）（m/=n）在这一点上，如果最低环境T0非空（根据良构的定义，这总是成立的），并且如果不等式的合取是可满足的，则每个良构的范式都是可满足的。为了证明这一点，让t是T0中的消息（t总是存在，因为T0不为空）。由于环境T0是封闭的（这可以通过对T0应用变量引入假设来看出），t是封闭的。然后，对于原子约束中的每个变量，我们将使用形式为tn的消息。显然，使用D的谓词的合取是满足的。通过改变变量n的值，如果/=部分是可满足的，我们将通过给n一个小于不等式个数加上变量个数的值来满足它。 直觉告诉我们，如果一个合取m1n2不满足，那么它满足于任何一个其他数nJn.我们将使用σk表示法，其意义xσk是由k乘以xσ组成的元组。xσk=（xσ）k= xσ，...，xσ命题3.5（解不等式）设P为约束m1/=n1/n... 其中mi和ni是消息。 如果P是可满足的，则对于任何置换σ，使得Pσ是闭的，并且对var（P）中的任何变量取不同的值，存在整数k，使得k≤j +1，并且σk是P的模型。证据 证明使用以下引理：设m和n是两个消息，σ是一个置换，使得mσ和nσ是闭的，并且xσ = yσ <$x = y。如果存在两个不同的整数i和j使得mσi=nσi和mσj=nσj，则我们有m=n。Q这种性质非常普遍，可以应用于其他运算符，而不是=。例如，同样的事情也适用于[11]中引入的算子，这将允许证明本文定义的谓词的类似扩展的可满足性的可判定性。这种可判定性（和NP-完全性）将证明，当考虑一个主动入侵者（Dolev-Yao模型）和有限数量的会话时，不透明度问题最终，满意度等同于部分的 这最后一满足性很容易通过例如否定这个连词来检验。这给出了仅使用等式的约束。然后，通过应用经典的统一，可以检查这个最终约束是否总是满足的。118L. Mazaré/Electronic Notes in Theoretical Computer Science 125（2005）109（因此，使用unification重写为T）或不（因此，其对立面是满意的或不满意的）。最后，本文的主要结果是前面所有性质的一个推论。定理3.6（主要定理）良构约束的可满足性是可判定的。这个结果并不是新的，例如在[1]中已经可以找到。然而，这里使用的演示似乎更容易适应其他情况。特别是，有了像f这样的一阶符号，这个定理将在下一节中非常直接地应用于展示不透明性的可判定性。Needham-Schroeder约束前一个重写系统已经在一个原型中使用ocaml实现。 然而，它已被修改，因此它不必测试所有可能的统一。这使得该方法更容易理解，对表现非常不利。这就是为什么我们的算法只在需要的时候才进行统一。例如，规则3和规则4将被替换为尝试f（...）的所有可能的统一的规则。）和环境中以f开始的可达模式。这种方法的优点是，通过查看重写系统所要求的统一，我们获得了不同参数的值，并且这种算法不必查看所有可能的统一，而只需查看“合理的统一”。在形式证明和其他作品中，一般的第一个想法是猜测子消息之间所有可能的等式，并使用最大的unifier消除它们（参见[7]如何将其应用于异或）。它已被测试的Needham-Schroeder约束。它的结果当然是这个约束是可满足的，唯一可能的变量在这次检查中，已经测试了五个可能的单位。其中三个涉及两个无法统一的消息，因此只研究了两个案例。一个很快导致满意，而另一个则不满意。将不等式y/=NB添加到初始约束，我们立即得到约束不再满足。这给了我们一个可能的解决方案：如果代理A能够确定nonceNB的起源（通过将其替换为一对nonce，即nonce的创建者的身份这是Lowe在[10]中出现的该协议的固定版本背后的想法。这个fix将代理的身份添加L. Mazaré/Electronic Notes in Theoretical Computer Science 125（2005）1091194准良构约束前面的定理可以推广到拟良型约束。至少有两种可能的方式来证明这一点。• 第一个解决方案是注意，我们使用第一个假设的唯一地方是证明规范形式的可满足性是可判定的。这就是为什么我们添加了最后一个关于准良构约束的假设，因此存在所有环境共有的封闭消息进行的修改旨在证明修改后的性能：命题4.1如果C和CJ是约束使得C→CJ且C是拟良型的，则CJ是拟良型的。对于任何类型的约束都证明了终止性，所以这不会是一个问题。正确性和完整性也可以调整。命题4.2重写系统→对于拟良构约束是正确和完备的。最终，当考虑范式时，证明不会改变：使用消息m的元组，可以验证满足性，因为消息m可以从任何涉及的环境中推导出来。• 另一种方法是指出准合式合取等价于合式合取的合取。在最初的结合中，原子约束TDm[U]可以替换为TDm[U]<$TJDmJ[UJ]，其中引入T中的不同变量的合取被添加，并且引入不同mJ中的变量的合取被添加（为了形式化，我们需要一个固定点）。由于初始约束中的合取数是有限的，因此结果是格式良好且有限的合取。本演示的其余部分将缩短，因为它将使用前一部分的结果。这就是为什么，这些连词可以重写。 这样，我们得到了一个等价的规范形，它是一个拟良型约束。正如我们之前所看到的，这个约束的满足性很容易检查。还有不等式部分要检查，但这仍然可以使用上述方法来完成。这两个证明框架允许我们证明以下定理。定理4.3拟良构约束的可满足性是可判定的。除了令人满意之外，我们还提供了一个已经实施的决策程序，并且似乎表现得很好。120L. Mazaré/Electronic Notes in Theoretical Computer Science 125（2005）109BC1Needham-Schroeder约束如前所述，我们进行此扩展的主要动机是将其应用于不透明度。然而，它还有其他可能的用途。环境包含假设成立，因为环境代表了入侵者由于入侵者只能学习新的消息，因此这个集合只能增长，并且假设没有限制。然而，通过抑制这一假设，现在可以用不同的环境来模拟不同的知识。具体地说，这个扩展可以很容易地对两个不能相互通信的入侵者进行建模。例如，让我们考虑Dolev-Yao攻击的修改版本。 有两个入侵者C1和C2，A和C1之间有一个会话，C2（盗用A我们想知道入侵者是否有可能推导出秘密NA或NB之一。 设T0为入侵者的初始知识{A，B，C1，C2，KC，KC，K−1，K−1}。然后，约束变为：T0D{A，x}KB1 2C1C2T0，{A，NA}D{xJ，yJ}K（T0，{x，NB}KADNB{A，NA}K，{yJ}KDNA）这个约束看起来是准良构的，但不是良构的。通过使用我们的决策过程，我们知道这个约束是不满足的。因此，两个入侵者需要通信，以便可以执行对Dolev-Yao协议的经典攻击5np完全我们现在将讨论我们的方法的复杂性。首先，良构约束的满足性是NP难的（例如参见[15]或[14]）。 这是只涉及D的良构约束的情况。由于所有这些约束都在我们正在研究的约束集中，因此我们的满意度为了证明这个满足性问题是NP问题，因此是NP完全的，我们将依赖于[14]中给出的结果。证明了给定一个不含不等式的满足良构约束，存在一个模型，其大小是约束大小的多项式.这里使用的大小是不同子项的数量。同样的结果也适用于我们的方法。其结果是一个替代σ，使得xσ的大小是多项式的大小的约束。当求解不等式部分时，大小保持多项式：令|M|DAG是m中不同子项的数目.那么很容易证明|Mn|DAG=|M|DAG+ n− 1。所以在一L. Mazaré/Electronic Notes in Theoretical Computer Science 125（2005）10912111 221 2在最坏的情况下，我们只将不等式和变量的数量添加到模型的大小中。因此，我们的模型的DAG大小仍然是初始问题大小的多项式。这就是为什么我们可以得出结论，良构约束的可满足性是NP完全的。对于准良构约束，可以使用完全相同的决策算法这证明了这些约束的可满足性也是NP-完全的。6不透明度的应用在本节中，我们将快速查看如何使用前一种方法来证明在考虑Dolev-Yao模型时不透明度是可判定的。 在其他论文中，我们只研究了被动入侵者的情况。在这里，我们将开始将可判定性结果扩展到主动入侵者的情况首先，让我们对两个环境和两个消息E，E n，nJ的情况给出一个扩展的定义。这意味着，通过对两个环境进行相同的操作，可以从E和EJ推导出n和nJ的部分。例如，{a，b}，{c，d}a，b，c，d为真，因为两个消息都是第一个和第二个消息在环境中配对获得，{a，b}，{c，d}{a，b，c，d }{a，c，d}{b，c，d}{d}{a，c，d}{d}{c，d}{c，d}{c}{d}{c}{d}{c}E，E n，nJ在封闭消息n，nJ和封闭环境E和EJ上定义为：E，EJn1，nJE，EJn2，nJ1 2{n1，...， nk}，{nJ，...， nJ}<$ni，nJE，EJ<$$>n1，n2<$，<$nJ，nJ<$1ki1 2E，EJn1，n2，nJ，nJE，EJn1，nJE，EJn1，n2，nJ，nJE，EJn2，nJE，EJ<${n1}n，{nJ}nJE，EJ<$n2，nJE，EJn，nJE，EJn，nJ2122 11 22E，EJ<$n1，nJE，EJ<${n1}n，{nJ}nJ1212注意E和EJ必须具有相同的长度（事实上，由于这些集合将被假设为相似的，这将不会是一个问题）。此外，由于我们希望在两个环境上执行相同的操作，我们需要对环境进行排序。它们可以用列表来表示。不透明度的定义（例如[11]中给出的）是入侵者无法区分满足属性的运行和不满足属性的运行。为了区分两个消息，入侵者可以根据他的知识分解它们，但是如果他不知道密钥k，例如，他将无法区分由该密钥k编码的两个不同消息。然而，在本节中，我们将只考虑一个非常简单的不透明度版本。让我们考虑一个具有唯一参数的有限协议P122L. Mazaré/Electronic Notes in Theoretical Computer Science 125（2005）109我我v（称为投票），只能取两个值是（协议Py）或否（协议Pn）。我们会说v的值不是不透明的（事实上，属性v=yes不是不透明的），如果入侵者能够通过在两个协议上执行相同的操作来产生yes和no。入侵者必须执行完全相同的动作序列：例如，如果在第一个协议中，他发送一个常数A，然后接收一个消息，这是一个对，并最终发送对的左边部分，他将不得不对第二个协议做同样的动作。这将等同于满足以下约束：T0，T0Dm0，mJT0; n0，T0; nJDm1，mJ. Tn，TJD是，不是0 0 1n其中Ti= T0; m0;. ;mi−1. 消息mi和mJ所产生入侵者并被发送到协议Py和Pn。然后，协议应答是消息ni和nJ。两个会话都以相同的方式进行，我们要求在最后，入侵者能够告诉哪个会话v等于是，并且在哪个会话V等于否。为了将我们的新约束与Dolev-Yao约束联系起来，让我们为我们的扩展算子引入一个显式二元函数f。约束可以写成f（T0，T0）D f（m0，mJ）<$f（T0; n0，T0; nJ）D f（m1，mJ）<$. f（Tn，TJ）Df（yes，no）0 0 1n接下来，我们将通过使用下面的distrib运算符递归地将f函数分布在我们的约束中：distribf（f（m，nJ））={distr i b f（f（m，mJ）），dis tribf（f（n，nJ））}distribf（f（{m}n，{mJ}nJ））={distribf（f（m，mJ））}d istribf（f（n，nJ））我们已经得到了一个公式f（m）=m。应用distrib函数creaa aconta c onta t a t这在以下性质中形式化，可以使用证明结构上的归纳来如果E和EJ是两个环境，n和nJ是两个消息，使得f不出现在E，EJ，n或nJ中，则以下等价为真：E，EJDn，nJ惠distribf（f（E，EJ））Ddistribf（f（n，nJ））因此，不透明度等同于Dolev-Yao约束的可满足性。此外，通过构造，该约束是良构的。因此，前面定义的不透明度是可判定的，我们有一个NP完全算法来检查满足性。然而，我们只研究了一个非常严格的版本的不透明度，但我们相信，这一结果可以扩展到一般的不透明度问题。L. Mazaré/Electronic Notes in Theoretical Computer Science 125（2005）1091237结论在本文中，我们给出了一个简单的决策过程，以证明满足通常的Dolev-Yao约束的扩展版本。该算法使用重写系统，易于实现。此外，我们相信，这种方法可以很容易地用于其他约束来自Dolev-Yao的一个。这是通过一个原型来完成的，它在简单的例子中表现良好。这些新谓词的直接应用是在两个不允许通信的入侵者存在的情况下检查秘密。然后准良构约束将是有用的，因为它们允许描述环境的两个“分支”，而不必通过集合包含来排序。这些分支中的每一个都将由一个格式良好的约束来描述进一步的工作包括当然更精确地链接这些约束的不透明性问题的情况下，一个积极的入侵者。然而，仍然有一个悬而未决的问题：一般Dolev-Yao约束的可满足性是可判定的吗？我们没有设法证明，在一般情况下（没有假设在所有）确认作者希望感谢Romain Janvier阅读了本文的初步版本，以及Hubert Comon的DEA课程引用[1] R. M. Amadio和D.卢吉斯密码协议中的可达性问题在并发理论国际会议，LNCS1877卷，380-394页，2000年[2] 的 Avispa项目。http://www.avispa-project.org/，1999年。[3] L. 博兹加岛 Lakhnech和M。 P'erin.一个最佳的跟踪方法是为使用纸张的保密性而进行的。技术报告，EVA：http://www-eva.imag.fr/，2002年。[4] E.M. Clarke，S. Jha和W.马雷罗使用状态空间探索和自然演绎式消息派生引擎验证安全协议。IFIP关于方案拟订概念和方法的工作会议，1998年。[5] H. Comon-Lundh.和V. Cortier。安全性能：两种药剂足够。技术报告，LSV，2002年。[6] H. Comon-Lundh和V. Cortier。一阶逻辑片段的新可判定性结果及其在密码协议中的应用。在第14届国际会议重写技术和应用（RTA[7] Hubert Comon-Lundh和Vitaly Shmatikov异或情形下的入侵者推理、约束求解与不安全决策。在第十八届IEEE计算机科学中的逻辑。IEEE Computer Society Press，June 2003.[8] D. Dolev和A. C.耀公钥协议的安全性。IEEE Transactions on Information Theory，29（2）：198124L. Mazaré/Electronic Notes in Theoretical Computer Science 125（2005）109[9] Jean古博-拉雷克一 方法 为 自动密码 议定书核查。并行程序设计的形式化方法国际研讨会：理论与应用，LNCS，2000年第1800卷。[10] G. 洛对Needham-Schroeder公钥认证协议的攻击。Information Processing Letters，56（3）：131-133，1995.[11] L. Mazar'e. 使用统一的操作规程。 在中国。安全理论（WITS'04）中的一个问题出现于2004年。[12] 乔纳森·K米伦和维塔利·什马蒂科夫有界进程密码协议分析的约束求解。ACM计算机和通信安全会议，第166-175页，2001年[13] R.M. Needham和MD施罗德在大型计算机网络中使用加密进行身份验证。Communications ofthe ACM，21（12）：993[14] M. Rusinowitch和M.图鲁阿尼具有有限会话数的协议不安全性是NP-完全的。IEEE计算机安全基础研讨会，2001年。[15] 我的儿子现在和妈妈在一起. Protoclineriniterfsec ri nit e s e c rit e cr i n ite s ec r ites e c r i n ite se c rTheor. Comput. Sci. ，299（1-3）：451