认证协议内射性的语法判据及循环性质验证 - C.J.F.克雷默斯等 - 2005.

理论计算机科学电子笔记135（2005）23-38www.elsevier.com/locate/entcs认证协议内射性的一个句法判据C.J.F.克雷默斯a S. Mauwa E.P. de Vinka，ba埃因霍温理工大学数学和计算机科学系，P.O. Box 513，NL-5600 MB埃因霍温，荷兰bLIACS，Leiden University，Niels Bohrweg 1，2333 CA Leiden，the Netherlands摘要在研究认证协议的正确性时，内射性是必不可少的，因为非内射协议可能遭受重放攻击。验证内射性的标准方法要么使用计数参数，这似乎只适用于基于模型检查的验证方法，要么根据所使用的数据模型的细节得出结论。我们提出并研究了一个性质，循环性质，它可以被语法验证，是足够的 以保证注入性。我们的结果是通用的意义上说，它适用于广泛的安全协议模型，并不依赖于消息内容或随机数新鲜度的细节保留字：安全协议，注入性，认证，同步1介绍在安全协议分析领域中研究最多的安全性质是认证。与保密要求相反，对认证的含义事实上，正如Lowe [10]所指出的，认证属性有一个层次结构，其中最流行的是协议。协议是指协议中的两个参与方保证在协议成功完成后就变量的值达成一致。在[4]中，我们通过引入同步化的概念扩展了Lowe因此，同步是一种内涵属性，正如罗斯科在[13]中定义的那样。这很容易表现出来1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.06.00624C.J.F. Cremers等人/理论计算机科学电子笔记135（2005）23·单方认证pkR pkR，skR I R随机数nR{I，nR}skR同意（nR）Replay攻击a（I）b（R）入侵者a㈠随机数NB{a，nb}skb学习{a，nb}skb同意（nb）{a，nb}skb同意同步属性意味着一致性。此外，假设标准Dolev-Yao入侵者模型，它严格强于协议;一些协议满足协议但不同步。差异是相当微妙的，这是由几乎所有熟悉的（正确的）安全协议满足同步要求的事实证明的。众所周知，满足协议的安全属性仍然可能容易受到所谓的重放攻击。在重放攻击中，入侵者重放从不同上下文获取的消息，从而欺骗诚实的参与者，使他们认为他们已经成功地完成了协议运行[11]。图1中的左 侧 协 议 显 示 了 一 个 协 议 的 示 例 ， 其 中 各 方 同 意 变 量 的 值 （ 即noncenR），而右侧场景显示了对该协议的重放攻击。附图采用消息序列图的形式，并且必须如下解释。响应者R有一个公钥/私钥对pkR，skR，创建一个随机数，并将他的加密标识消息发送给发起者。在接收到该消息之后，发起者I可以断定他与响应者共享nR的值，如六边形中所表示的。在右边的MSC中，两个代理a和b分别以发起者和响应者的角色执行该协议。现在，入侵者可以无意中听到发送的消息，并可以在将来的运行中欺骗a，使其认为b发送了此消息。图1.一、易受重放攻击的身份验证协议为了排除这样的非法协议，需要在[10]中提出的内射性的附加性质。这相当于要求执行发起者角色的代理的每次运行对应于其运行响应者角色的通信伙伴的唯一运行。图1中的单边认证协议显然不满足注入性，如图右侧的重放攻击所示。一个简单的解决方法是让发起者确定随机数的值，如图2所示。C.J.F. Cremers等人/理论计算机科学电子笔记135（2005）2325·单方认证pkR pkR，skR I R现时数nI{I，nI}skR同意（nI）图二. 解决注入性问题。从发起者到响应者再回到发起者的因果消息链的引入似乎可以做到这一点。 我们称之为一条链子一个环。该性质在下面关于注入性的讨论中起关键作用。民间传说，例如，随机握手足以确保注入性。在这里，我们确定了一个更抽象的属性，即。循环的发生，它与数据模型无关，因此适用于广泛的安全协议模型。为了说明基于数据的方法的局限性，考虑一个协议，其中创建一个随机数n，并对其应用某个函数。结果f（n）被发送给响应者，响应者应用另一个函数并回复g（f（n））。现在，为了检查这样的协议是否可以基于基于数据模型中n的新鲜度来单射，我们需要知道f和g的一些细节。如果例如f（x）=x mod 2，则协议将不是单射的。我们的方法不需要任何关于消息内容的信息。大多数注入性方法通过使用计数策略使Lowe这个计数参数可以很容易地用在模型检查方法中。事实上，这就是在Casper/FDR工具链中验证注入能力的方式[9，14]。由于只能对有限和固定数量的sce- narios进行建模，因此这种方法只能提供注入性的近似值。安全协议的其他验证方法，例如基于逻辑（如[2]）或项重写（如[5]）的方法似乎不太注意注入性。串空间[15]方法，不提供正式的手段来处理内射性。相反，建议基于随机数检查认证，例如通过使用所谓的请求认证测试26C.J.F. Cremers等人/理论计算机科学电子笔记135（2005）23如[6]所示。这些测试基于随机数的新鲜度保证注入性。在这种观点中，认证和注入性是紧密相连的我们提到两个例子的安全协议形式主义，明确处理- itly与注入性。Gordon和Je Escherey设计了一种方法[7]来验证π-演算的内射对应关系。这种方法允许通过类型检查（内射）对应进行验证。 第二个例子是Adi，Debbabi和Mejri [1]的电子商务协议逻辑，其中模式匹配用于表达两方协议的注入性。然而，目前还不清楚如何有效地验证这一点。在本文中，我们研究的问题是，是否有一种方法来验证安全协议的注入性，这是通用的，在这个意义上说，它可以应用在一个大类的验证方法，无论使用的数据模型。我们研究的出发点是[4]中提供的内射同步这种内射性的定义并没有利用计数，而只是要求将代理分配给协议角色的函数是一个内射函数。我们将在后面回顾这个定义的细节。我们的主要结果是，对于一个大类的安全协议语义，上面介绍的循环属性保证同步协议也是单射的。类的安全协议的语义，我们的结果持有，其特征在于关闭下交换事件的执行轨迹集。这个类包含例如，标准Dolev-Yao入侵者模型的过程代数方法。除了这个交换属性，我们不需要对数据模型和入侵者模型做其他假设。由于循环性质可以通过对安全协议描述的静态分析来容易地验证，因此我们提供了一个验证注入性的实用语法标准。本文的成就是我们已经确定了一个允许内射同步的模块化证明的一般性质：一旦证明了非内射同步，就很容易证明内射同步。有趣的是，该属性不依赖于数据模型，因此不依赖于例如随机数的属性或应用于随机数的函数。本文件其余部分的结构如下。在第2节中，我们描述了一个正式的安全协议模型和我们的主要结果的基本假设。在第三节中，我们形式化了单射认证和循环性质，并证明了它们之间的关系。最后，在第4节中，我们得出了一些结论，并指出了未来研究的选择。C.J.F. Cremers等人/理论计算机科学电子笔记135（2005）23272安全协议安全协议被抽象地定义为从角色的有限集合Role到从集合RoleEvent获取的所谓角色事件的有限序列的集合RoleEvent的映射。对于一个安全协议p：Role→RoleEvent，一个roler∈Role表示一个参与p的主体，其活动为p（r）。发送和接收消息是这样的活动，以及提出索赔。我们假设RoleEvent事件队列{发送l（r，rJ，m），读取l（r，rJ，m），声明l（r，c）|l∈Label，r，rJ ∈Role，m ∈RoleMess，c ∈Claim}角色事件sendl（r，rJ，m）被解释为：角色r发送要传递给角色rJ的消息m，而readl（r，rJ，m）意味着角色rJ读取具有发送者r的形式m的消息。对于事件声明l（r，c），我们有，无论何时r主张c，主张c为真。角色事件都用标签装饰，通常从集合Label中获取。安全协议中的每个角色事件都有一个唯一的标签，除了相应的发送和读取事件。我们说发送事件sendl（r，RJ，m1）并且读取L（r，RJ，m2）与发送者r，接收者RJ匹配。 (Note我们允许消息通常是不同的，因为发送者的观点和接收者的观点也不同。RoleMess中消息的格式是未指定的，Claim中声明的格式也是如此。其他类型的角色事件也可以存在于RoleEvent在安全性协议p中，casali tyrr“p的定义是关于even s的一个部分。它被定义为RoleEvent上的最小自相关和传递关系，使得• e• 如果E = SENDL（R，RJ，M）∈ P（R），则对于R，RJ，EJ = READL（R，RJ，M）∈ P（RJ）.示例众所周知的Needham-Schroeder-Lowe协议（NSL）[12，8]如图3左侧所示，具有两个角色：发起者I和响应者R。角色末尾的内射同步声明，这里缩写为i-synch，将在3.1节中定义。假设两个代理都知道对方的公钥和私钥。28C.J.F. Cremers等人/理论计算机科学电子笔记135（2005）231 ） 2 ） 3 ） 4 ）5） 6）7 ） 8 ） 9 ）10 ） 11 ）12 ） 13 ）14 ） 15 ）16 ） 17 ）19 ） 110 ）119）1110）1119）11119）111119）1111119）111119111191senvd2senvd3 ）reavd3claivm4IVM5级图3.第三章。NSL协议及其事件的偏序性自己的钥匙。 形式上我们有NSL（I）=发送1（I，R，{I，nI}pkR）·读取 2（R，I，{R，nI，nR}pkI）·发送3（I，R，{nR}pkR）·声明 4（I，i-同步）NSL（R）=读取1（I，R，{I，nI}pkR）·发送 2（R，I，{R，nI，nR}pkI）·读取3（I，R，{nR}pkR）·权利要求5（R，i-synch）。图3中右边的格给出了NSL的计算顺序（其中发送1是最小元素）。安全协议的语义是一组跟踪。然而，为了处理由同一方执行多个角色定尼达姆-施罗德-洛pkR，skI pkI，skR I R现时数1{I，nI}pkR随机数nR2{R，nI，nR}pkI3{nR}pkR4i同步5i同步C.J.F. Cremers等人/理论计算机科学电子笔记135（2005）2329义的可能性 让代理成为集合的代理人。由代理执行的角色称为运行。由于每个代理可以执行多个（可能相同的）角色实例，因此我们假设已为每个运行分配了RunId中 具有run identi f ierrid的事件e由e rid表示。这会产生一组所谓的运行事件RunEventRunEvent{send l（a，aJ，m）rid，read l（a，aJ，m）rid，claim l（a，c）rid|rid∈RunId，l ∈Label，a，aJ ∈Agent，m ∈RunMess，c∈Claim}例如，发送L（a，aJ，m）RID是代理A在其运行RID的执行期间向代理aJ发送消息m。安全协议的精确语义在本文中是隐含的。为了我们的目的，它succes假设语义捕捉代理和一些特定的入侵者模型的操作行为，语义产生的痕迹的集合此外，语义学注意，30C.J.F. Cremers等人/理论计算机科学电子笔记135（2005）23运行标识符的手段，安全协议的多个实例。安全协议p的语义用Tr（p）RunEvent表示。迹α∈Tr（p）是游程的交织。对于这样的迹α，我们用αi表示α的第i个事件.请注意，标签和运行标识符不是消息的一部分，因此不受入侵者的控制。它们表示的信息往往隐含在语义模型中。标签表示事件执行时代理的状态，运行标识符表示事件发生在哪个运行中。读者可以填写他或她最喜欢的映射Tr的语义。然而，为了下面的推理，我们需要对这个映射有两个一般要求我们假设语义Tr（p）具有以下两个性质：-为所有eventseJread（，，）它认为，α;e rid;eJridJ;αJ∈Tr（p）<$α;eJridJ;e rid;αJ∈Tr（p）对于所有轨迹α，αJ，事件e和两个游程标识符rid/=ridJ。–α;sendl（m）ridJJ;αJ;e rid;readlJ（m）ridJ;αJJ∈Tr（p）<$α;sendl（m）ridJJ;αJ;readlJ（m）ridJ;e rid;αJJ∈Tr（p）对于所有轨迹α，αJ，事件e和运行标识符rid，ridJ，ridJJ，使得rid=/ridJ。这些属性表明，我们可以将非读事件向左移动，只要它不与同一运行的任何其他事件交叉。对于read事件，我们有一个额外的约束：我们只能将它移到左边，如果仍然有相同消息的早期发送。3内射性的句法判据在本节中，我们定义了一个认证协议的语法标准，称为循环属性，并证明它可以证明内射性。首先，我们定义一个强认证属性，称为同步。其次，我们定义了句法标准，并证明了主要结果。3.1同步同步是一种强大的身份验证形式无论何时代理要求同步，我们都要求交互到目前为止表现良好C.J.F. Cremers等人/理论计算机科学电子笔记135（2005）2331导致索赔的事件必须完全按照预期发生。参见[4]。同步的一般定义是指一个特定的协议p和一个声明标签。为了简化标记，我们将在下文中假设存在具有由claim表示的单个claim角色事件的单个协议p。但是，请注意，在一个跟踪中可能会发生多个声明运行事件。这种情况是当承载声明的角色已被分配给多个代理或多次分配给同一代理时。考虑图2中的协议，并假设agree声明已被ni-synch声明替换。 协议声明对所有跟踪都有效在协议中，跟踪中的每个实例化声明都是有效的。因此，如果在一个跟踪中，一个带有标识符rid1的run请求同步，我们(i) Runrid 1发送随机数。(ii) 运行rid2读取这个精确的随机数。(iii) Runrid 2发送一条包含签名的nonce的消息。(iv) 运行rid1会读取此消息。(v) 运行rid1声明同步。在这个例子中，由于runrid 2填充了角色R，我们要求每个ni-synch声明实例都存在因此，给定一个跟踪，我们要求每个声明实例都有运行，这些运行填充了其他角色。此关系由类型为{ rid}的角色实例化函数强制转换给出|iα i=claimrid}×Role→RunId。对于跟踪中的每个声明，它将运行与每个角色（即，该函数为每个声明运行给出协议的完整转换）。在上面的例子中，我们会有：cast（rid1，I）=rid 1和cast（rid1，R）=rid2。这是不确定的。我们要求，对于每一个索赔运行，对于索赔发生的协议的每一个角色运行，都存在满足其他角色的运行。对于跟踪中的所有声明，强制转换函数是组合该声明的角色实例化为了正式定义同步，我们引入sendrole和readrole函数来分别确定给定标签的发送角色和接收角色。sendrole（l）=r ifsendl（r，rJ，m）∈p（r）orreadl（r，rJ，m）∈p（rJ）readrole（l）=rJ ifsendl（r，rJ，m）∈p（r）orreadl（r，rJ，m）∈p（rJ）32C.J.F. Cremers等人/理论计算机科学电子笔记135（2005）23此外，我们使用claimrole来表示发生协议声明的角色的名称。请注意，在跟踪中可以有多个此角色的实例。接下来，我们表示跟踪中的声明实例何时有效。给定一个迹α，一个声明runrid，以及一个将角色映射到游程的关系转换，我们在域Tr（p）×（RunId×Role→）上表示辅助谓词χ。RunId）×RunId，χ（α，cast，rid）xx（rid，claimrole）=ridxGpclaimi，j∈N，a，b∈Agent，m∈RunMessI ji=sendl（a，b，m）cast（rid，sendrole（l））αj=readl（a，b，m）cast（rid，readrole（l））（一）这个谓词的第一个合取词表示这样一个事实，即执行声明角色的运行由参数rid固定。第二个合取词表示在迹α中，runrid的声明对于特定类型转换是有效的，即合作伙伴已经按预期执行了所有通信。在公式中，这是由发送和读取事件由预期运行执行的事实表示的，具有相同的消息m，并且以正确的顺序i j。使用这个谓词，我们将非内射同步定义为在跟踪中发生的所有声明的有效性，对于某些转换函数：NI-SYNCHα∈Tr（p）<$cast <$i，ridαi=claimrid<$x（α，cast，rid）因此，如果对于所有迹线都存在转换，使得对于声称同步的每个运行，χ谓词保持，则协议不存在。假设χ（α，cast，rid）成立，则cast有以下两个属性：首先，每个claim run都填充了claim role本身，因此：crafridcast（rid，claimrole）=rid。其次，cast只将运行分配给角色，当这些运行正在执行该角色时，所以我们有：craid ，rrole（cast（rid，r））=r。强制转换函数为引入注入性提供了一个自然的句柄注入性要求两个不同的声明实例与不同的伙伴运行同步因此，我们说角色实例化函数强制转换是单射的，如果n（rid1，r1）=（rid2，r2）cast（rid1，r1）cast（rid2，r 2）我们将这种注入性要求纳入NI-SYNCH的定义中。C.J.F. Cremers等人/理论计算机科学电子笔记135（2005）2333内射同步的定义如下：I-SYNCHα∈Tr（p）castinivei，ridαi=claimrid<$x（α，cast，rid）因此，在同步需求之上，我们现在要求对于在协议声明之前的所有通信，都有执行协议角色的唯一运行。在正式定义了同步之后，我们研究了同步协议的一些性质给定跟踪α中的runrid的有效同步声明，存在角色实例化函数cast，使得χ（α，cast，rid）保持。谓词χ告诉我们某些事件存在于迹中。因为我们想在下面对这些事件进行推理，所以我们决定将这组事件显式化。稍微滥用一下符号，我们使用e来表示与运行事件e对应的唯一角色事件。函数runid（e）简单地产生run事件e的run标识符。我们定义了一组事件χJ（α，cast，rid）通过χJ（α，cast，rid）={e|iαi=e假设χ成立，它的事件集χJ有两个有趣的性质。如果在这个集合中有一个read，那么在这个集合中也有一个匹配的send此外，委员会认为，给定集合中角色的事件，相同角色的所有先前事件也在集合中。为了证明我们的主要结果，我们给出了第二节中介绍的两个交换性质。然而，为了简化证明的解释，我们引入了两个引理。这些引理是由模型和两个交换属性所隐含的。第一个引理将两个事件的交换推广到一组事件的交换。引理不适用于任何事件集合：我们现在使用由x定义的事件集合获得的结果，这些事件涉及同步声明。根据这两个交换属性，我们可以将这些事件（按其原始顺序）转移到跟踪的开始。为了表达这样的移动的事件集，我们介绍了一个移动功能的痕迹。 我们定义一个跟踪转换函数移位：P（RunEvent）×RunEvent→RunEvent通过.位移（E，α）=αifαi（αi/∈E）e;shift（E，β;βJ）ifα=β;e;βJ<$i（βi/∈E）<$e∈E此函数有效地重新排序跟踪。下一个引理公式化的条件，确保在Tr（p）中的轨迹的重新排序也在Tr（p）中。34C.J.F. Cremers等人/理论计算机科学电子笔记135（2005）23引理3.1给定协议p和迹α∈Tr（p），声明runrid和角色实例化函数cast：χ（α，cast，rid）<$αJ=shift（χJ（α，cast，rid），α）<$αJ∈Tr（p）<$x（αJ，cast，rid）证据 关于有限集合χJ（α，cast，rid）的大小的归纳，因为χ（α，cast，rid）意味着读事件可以交换。Q引理直接推广到更多的索赔实例（相同的索赔）。因此，我们可以考虑多组索赔，而不是单个索赔。引理3.2给定一个迹α∈Tr（p），一组索赔游程CR∈ P（RunId）实例化函数cast：RunId×Role→RunId：（1）A= A（A =A），B= A（rid∈CRχJ（α，cast，rid），α）αJ∈Tr（p）<$（αJ，cast，rid）证据 类似于引理3.1的证明。Q如果我们将移位函数应用于系统的迹，并且满足引理的条件，我们得到一个重排的迹，也是在Tr（p）中。 新的跟踪由两个部分组成：在第一个部分中，CR中只有索赔运行的先前事件，所有其他事件都在第二个部分中。直观地说，这些引理表示，在一个有效的同步索赔所涉及的事件是独立于其他事件的痕迹。有效的同步可以发生在跟踪中的任何点，因为它不需要其他运行或入侵者的参与。但是，跟踪中的其他事件可能取决于同步中涉及的事件。因此，我们不能将同步事件移到右边;但是我们可以将它们移到左边，这确保了任何依赖性都不会被破坏。我们在下一节的内射性证明中使用这些引理。3.2LOOP属性我们定义了协议的一个属性，我们称之为LOOP属性。对于只有两个角色的协议，它类似于一个乒乓属性：首先声明角色执行一个事件，然后另一个角色，然后再次声明角色。例如，LOOP属性不适用于图1中的协议，但适用于图2和图3中的协议。C.J.F. Cremers等人/理论计算机科学电子笔记135（2005）2335我们将其推广到具有任意数量角色的多方协议。我们要求合作伙伴角色有一个必须在索赔运行开始之后但在索赔事件本身之前发生的事件。定义3.3安全协议p具有LOOP属性ieGpclaim，role（e）/=claimro leeJ （二）现在我们可以陈述主要定理了，它给出了一个协议的内射性的句法条件。定理3.4NI -SYNCH同步回路证据矛盾。假设这个推论不成立。 我这样NI-SYNCH双回路电机I -SYNCH（3）其余的证明分两步完成。证明的第一步是建立协议的迹α，其中有两个运行与同一个运行同步。在第二步中，我们使用移位引理将α转换为协议的另一个迹。对于这个新的迹线，我们将证明NI-SYNCH不成立，这与假设相矛盾.从现在开始，我们将省略α的类型信息，并在量化器中进行转换，并假设α∈Tr（p）。考虑到协议是单射的，但它不是单射的，我们从NI-SYNCH的定义推导出，I-SYNCH和公式⑶，α<$$>αcast内射<$i，ridαi=claimrid<$x（α，cast，rid）（4）我们将右边的否定推过量化器，得到α<$α<$cast<$（cast内射<$i，ridαi=claimrid<$ x（α，cast，rid））（5）基于（5）中的存在性量化器，我们选择迹α和实例化函数，使得i，ridαi=claimrid<$（cast内射的n_i，ridαi=claimridn_x（α，cast，rid））（6）36C.J.F. Cremers等人/理论计算机科学电子笔记135（2005）23注意，在（6）中，左合取词也作为右合取词中的子公式出现。重写收益率i，ridαi=claimrid使函数强制转换的非注入性显式，必须存在两个游程标识符，其中χ成立：（rid1，r1），（rid2，r2），rid3χ（α，cast，rid1）cast（rid1，r 1）=cast（rid2，r 2）n（rid1，r 1）/=（rid2，r 2）（8）从谓词χ和公式（8）中，我们得到运行类型转换（rid1，r 1）必须执行角色r1。因为cast（rid1，r 1）=cast（rid2，r 2），所以它也在执行角色r2。由于运行只执行单个角色，因此必须是r1 =r 2。来自存在量化器的不等式现在简化为rid1rid 2。设r=r1=r2。我们选择两个游程标识符rid1，rid 2，使得公式（8）对r成立。现在存在游程标识符rid3，使得cast（rid1，r）=cast（rid2，r）=rid 3从χ的定义，我们得到，如果r等于claimrole，我们将有rid3 =rid 1和rid3 =rid 2，这意味着rid1 =rid 2，与方程（8）矛盾。因此，我们有r/=claimrole。我们现在已经确定迹α至少包含三个游程。两其中的RID1和RID2正在执行声明角色，而第三个RID3正在执行不同的角色R。此外，我们还得到rid1和rid2的声明与rid3同步。这就完成了证明的第一步。在证明的第二部分中，我们现在将α变换成NI-SYNCH不能成立因为我们有χ（α，cast，rid1）和χ（α，cast，rid2），基于引理3.2我们可以使用rid1和rid2进行移位，得到迹αJ∈Tr（p）αJ=shift（χJ（α，cast，rid1）<$χJ（α，cast，rid2），α）在迹αJ中，我们现在有两个不同的线段。所有与rid1和rid2同步有关的事件现在都在αJ的初始段。这包括在声明之前的rid3事件。αJ的第二段包含所有其他事件，这些事件不包括在先前的rid1和rid2事件中。现在我们将重新排序αJ的初始段。为此，我们申请第二次换档功能，现在仅用于RID1。这也将产生协议的踪迹，因为引理3.2的条件对αJ成立，C.J.F. Cremers等人/理论计算机科学电子笔记135（2005）2337对α应用移位保持了移位集合中事件的顺序，这意味着χ（αJ，cast，rid1）成立。因此，我们也知道下面的迹是Tr（p）的元素：αJJ=shift（χJ（αJ，cast，{rid1}），αJ）因为移位函数保持了所涉及事件的顺序，所以我们有αJJ=β;γ;δ，其中<$iβi∈χJ（αJ，cast，{rid1}）iγi∈χJ（α，cast，{rid1，rid2}）\χJ（αJ，cast，{rid1}）与rid1和rid2的同步声明无关的所有事件rid2，在δ中。观察到β包括rid3中所有与runrid 1的声明相关的事件。因为所有事件都是唯一的，所以它们不是γ的一部分。从所涉及的事件集的构造中，我们知道角色r的所有所涉及的事件都是runrid 3的事件，因为所有其他运行都在执行其他角色（如强制转换所示）。这意味着在γ中根本不存在角色为r的事件：这些都在β中。现在我们遇到了一个矛盾。αJJ在集合Tr（p）中。与NI-SYNCH结合使用的循环属性要求每个角色都有一个在索赔角色的第一个事件之后的事件，发生在索赔之前。对于runrid2，所有事件都在γ中（包括开始和声明），但在此段中没有角色r的事件。因此，不可能有αJJ的强制转换，χ（αJJ，cast，rid2）成立。 这意味着NI-SYNCH不适用于这与假设相矛盾。Q4结论和今后的工作我们已经证明，对于一个大类的安全协议模型，认证协议的注入性是很容易验证的，一旦同步已经建立。到目前为止，注入性和认证性一直是紧密联系在一起的。我们的新结果表明，它succes验证同步的非内射变体。单注入性是一个简单而独立的任务，它不依赖于任何特定的（数据）模型。我们没有为此结果选择特定的安全协议模型相反，我们刻画了一类定理成立的模型这个类几乎包含了文献中的所有模型，例如StrandSpaces模型，Casper/FDR无时间模型和术语重写系统[15，9，5]。这些模型共享以下属性：38C.J.F. Cremers等人/理论计算机科学电子笔记135（2005）23示例协议I RI，R随机数nR{I，nR}skR不同意• 协议的多个实例是真正独立的。它们不共享变量、内存或时间。• 入侵者有能力复制消息。例如，这在标准的Dolev-Yao入侵者模型中成立。问题是这个定理是否在无入侵者模型中也成立。这实际上是一种情况，但不太感兴趣，因为当没有入侵者时，注入性始终适用于同步或同意协议。因此，LOOP属性可以很容易地实现。我们目前正在开发Scyther工具的扩展[3]。该算法是非循环有限图中的可达性问题的一个实例，因此是线性的。见图4。 一个单方面的协议，有LOOP，但不是单射的。几乎所有正确的协议都满足NI-SYNCH和LOOP。这似乎是一个必要条件，注入LOOP我们知道这适用于Dolev-Yao入侵者模型。然而，对于特殊的入侵者模型，LOOP不是内射性的必要条件。在模型中，循环也是注入性的必要条件，我们的结果意味着在多方认证协议的消息的最小数量。我们将在今后的工作中对此进行调查。这里我们只考虑了同步，而没有考虑一致性。这就提出了一个问题，是否存在类似的性质来显示注入性达成协议从图4中的示例可以看出，LOOP不能保证注入能力。该协议满足声明角色的循环属性，并且该协议满足非内射协议，但不满足内射协议。寻找一种替代协议是未来研究的一个有趣的挑战。C.J.F. Cremers等人/理论计算机科学电子笔记135（2005）2339引用[1] Adi ， K. ， M. Debbabi 和 M.Mejri ， A new logic for electronic commerce protocols ，Theoretical Computer Science291（2003），pp.223-283。[2] Burrows ， M. ， M. Abadi 和 R. Needham ， A logic of authentication ， ACM Transactions onComputer Systems8（1990），pp. 16比36[3] Cremers，C.，Scyther安全协议验证工具：文档，http://www.win.tue.nl/www.example.com[4] 克雷默斯， C.的方法， S. 莫乌 和 E. D. 文克， 定义 认证 在 一 微量 型号：T. Dimitrakos和F. Martinelli，editors，Proc. FAST 2003（2003），pp. 131-145[5] Genet，T.和F. Klay，Rewriting for cryptographic protocol verification，in：Conference onAutomated Deduction（2000），pp. 271-290。[6] Guttman ， J. D. 和 F. J. Thayer ， 认 证 测 试 和 捆 绑 包 的 结 构 。 ， Theor 。 Comput. Sci. 283（2002），pp. 333-380[7] Je Escherey，A.和A. Gordon，安全协议中的一对一和一对多对应，M。冈田湾C. Pierce，A.谢德罗夫Tokuda和A. Yonezawa，editors，Proc. ISSS418-434[8] Lowe，G.， 使用FDR打破和修复Needham-Schroeder公钥协议，在：T. Margaria和B. Ste Escheren，editors，Proc. TACAS147-166.[9] Lowe，G.，Casper：一个用于安全协议分析的编译器，在：Proc.CSFW18比30[10] Lowe，G.，认证规范的层次结构，在：Proc. CSFW31比44[11] Malladi ， S. ， J. Alves-Foss 和 R. Heckendorn ， 关 于 防 止 对 安 全 协 议 的 重 放 攻 击 ， 在 ：Proc.ICSM77-83.[12] 尼 达 姆 河 和 M. Schroeder ， Using encryption for authentication in large networks ofcomputers，Communications of the ACM21（1978），pp. 120比126[13] Roscoe，A. W.，Intensional Specifications of Security Protocols，in：Proc. CSFW28比38[14] 瑞安，P.，S.施耐德，M。Goldsmith，G. Lowe和B. Roscoe，[15] Thayer，F.，J. Herzog和J. Guttman，Strand Spaces：为什么安全协议是正确的，在：Proc. 安全和隐私研讨会，奥克兰（1998年），pp。160-171。