符号安全证明：Otway-Rees协议密码可靠性的密码学保密性证明.

理论计算机科学电子笔记155（2006）111-145www.elsevier.com/locate/entcs基于符号安全的证明1迈克尔·巴克斯IBM苏黎世研究实验室mbc@zurich.ibm.com摘要我们提出了著名的Otway-Rees协议的第一个加密安全证明。更确切地说，我们表明，该协议是安全的，对任意的主动攻击，包括并发协议运行，如果它是使用可证明安全的密码原语实现。我们证明了交换密钥的保密性与公认的真实或随机保密的密码学定义有关，即，交换密钥和随机密钥的不可否认性，给出了一般密码攻击者的观点。虽然我们在密码学定义下实现了安全性，但我们的证明是在与稍微扩展的Dolev-Yao模型相对应的确定性设置中执行的;特别是，它不必处理密码学的概率方面，因此在当前证明工具的范围内。原因是，我们利用最近提出的理想的密码库，它有一个可证明安全的密码实现，以及最近的结果链接符号和密钥保密。除了建立Otway-Rees协议的密码安全性之外，我们的结果还举例说明了这个密码库的潜力和最近的保密性定理，用于符号但密码学上可靠的安全性证明。保留字： 密码可靠性，Otway-Rees，实或随机保密性，Dolev-Yau模型1引言许多实际相关的加密协议，如SSL/TLS，S/MIME，IPSec或SET，以黑盒方式使用加密原语，如签名方案或加密，同时添加许多非加密功能。从早期1 [4]的扩展和修订版本1571-0661 © 2006由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2005.11.054112M. Backes/Electronic Notes in Theoretical Computer Science 155（2006）111认证协议，如Needham-Schroeder [38，20]，经过仔细设计的事实标准，如 SSL 和 PKCS [44 ， 17] ， 直 到 目 前 广 泛 部 署 的 产 品 ， 如 MicrosoftPassport [22]。然而，长期以来，证明此类协议的安全性一直是一项非常令人不满意的任务进行这种证明的一种方法是加密方法，其安全性定义基于复杂性理论，例如，[24、23、25、14]。密码协议的安全性是通过约简证明的，即，通过表明破坏协议意味着破坏关于其密码定义的底层密码原语之一。这种方法捕获了一个非常全面的对手模型，并允许数学上严格和精确的证明。然而，由于概率论和复杂性理论的限制，迄今为止，这些证明都是手工完成的，这产生了错误和不完善的证明。此外，这样的证明对于更大的协议来说很快变得过于复杂。另一种方法是形式方法，它关注的是使用模型检查器和定理证明器的自动化证明。由于这些工具目前无法处理密码学细节，如错误概率和计算限制，因此使用密码学的抽象。 它们几乎总是基于所谓的Dolev-Yao模型[21]。该模型大大简化了大型协议的证明，并产生了大量关于使用各种形式验证技术分析协议安全性的文献，例如，[35、33、29、18、41、1]。在Dolev-Yao模型中典型分析的协议中，Otway-Rees协议[39]旨在通过可信第三方在两个用户之间建立共享密钥它在过去被广泛研究，例如，在[40，28，41]中，各种新的方法和用于安全协议分析的形式化证明工具通过证明它们可以在Dolev-Yao模型中证明协议而得到验证（分别是，如果底层模型本身不提供足够的类型，它们可以找到众所周知的类型攻击;我们的证明所基于的模型排除了这种攻击）。然而，所有现有的Otway-Rees协议的安全性证明都局限于Dolev-Yao模型，即，不存在允许将现有证明的结果延续到具有其更全面对手的密码方法的定理。因此，尽管对Otway-Rees协议进行了大量的研究，但基于可证明安全的密码原语的实际实现在密码安全定义下是否安全仍然是一个悬而未决的问题。我们通过在加密方法中提供Otway-Rees协议的第一个安全证明来缩小这一差距。我们证明了该协议对任意主动攻击M. Backes/Electronic Notes in Theoretical Computer Science 155（2006）111113如果对称加密的基于Dolev-Yao的抽象是使用对称加密方案来实现的，该对称加密方案对于选择密文攻击是安全的，并且还确保了密文的完整性。更确切地说，我们证明了交换密钥的真实或随机保密性，即，我们表明，没有密码攻击者能够区分新鲜的、随机的密钥和实际上在两个诚实的参与者之间交换的密钥，除非底层的密码学可以被破坏。这是公认的密码学定义密钥保密此外，我们表明协议的一致性，成功地建立了共享密钥的parties有一个一致的看法，谁的会话的同行。2选择密文的安全性和完整性密文是认证对称的标准安全定义，RIC加密方案[16，15]和在这个意义上可证明安全的有效对称加密方案在合理的假设下存在[15，43]。显然，在密码学方法中建立证明的前提是处理上述密码学细节，因此人们自然会认为我们的证明严重依赖于复杂性理论，并且远远超出了当前证明工具的范围。然而，我们的证明不是在密码设置中从头开始执行的，而是基于最近提出的密码库[10，11，8]，其提供了密码忠实的，确定性的密码原语抽象，即，可以使用实际的密码术来安全地实现抽象。此外，该库允许以任意方式嵌套抽象，与原始的Dolev-Yao模型非常相似。虽然这在[10]中针对公钥加密和数字签名进行了说明，随后在[11]中扩展了消息认证码，但该库的最新扩展进一步纳入了对称加密[8]，它构成了Dolev-Yao模型的典型证明中最常用的密码原语，并且还作为表达和分析Otway-Rees协议的中心原语。然而，如[8]所示，在[10]中使用的强安全性意义上，从对称加密提供合理的抽象存在内在的困难。非常粗略地说，只有在不发生所谓的承诺问题的情况下，才能建立对称加密的合理的Dolev-Yao式抽象，这意味着每当对手不知道的密钥被诚实的用户用于加密时，该密钥将永远不会被泄露给对手。我们将在本文中更详细地阐述这个问题的起源。虽然[8]讨论了这个问题的几种解决方案，但实际上采取的是将其留给周围的协议来保证承诺问题不会发生，即，如果使用对称的协议2在[28]中已经指出了这种一致性属性的违反，这是由于 可信第三方的不同建模我们将在下面讨论这一点114M. Backes/Electronic Notes in Theoretical Computer Science 155（2006）111加密应该被忠实地分析，另外还必须表明，一旦诚实的参与者开始使用密钥，该协议保证密钥不再以可能使对手知道它们的形式发送。我们的证明表明，这是一个易于管理的任务，可以很容易地纳入整体的安全证明，而不会对证明者施加重大的额外负担。一旦我们证明了Otway-Rees协议不引起承诺问题，我们就基于确定性抽象证明了Otway-Rees协议的安全性。结合最近关于符号和密码密钥保密性的结果[9]，这允许我们对Otway-Rees协议执行保密性的符号证明，并从中导出所需的密码密钥保密性。类似地，我们建立了基于抽象的一致性属性，并利用一般的完整性保持定理[6]来推导密码设置的一致性属性。由于证明是确定性的和严格的，它应该很容易在形式证明工具，特别是定理证明。即使是手工完成的，我们的证明也比在密码学方法中从头开始进行的简化证明更不容易出错。我们还想指出的是，我们的结果不仅提供了迄今为止缺少的Otway-Rees协议的密码安全性证明，而且还举例说明了密码库[10]，其扩展[11，8]以及基于该库[6，9]的连接符号和密码属性的相应一般定理的有用性，用于密码协议的密码可靠验证进一步相关工作。Dolev-Yao模型的密码学基础首先由Abadi和Rogaway在[3]中解决。然而，它们只处理被动对手和对称加密。在[2，30]中扩展了处理的协议语言和安全属性，但仍然仅适用于被动攻击者。这排除了攻击协议的大多数典型方式，例如，中间人攻击和通过在不同位置重用消息部分或并发协议运行的攻击。Dolev-Yao模型的完整加密证明，即，对于任意主动攻击和任意周围交互协议，最近在[10]中首次给出，并在[11，8]中进行了扩展。基于在[10]中证明了其可靠性的特定Dolev-Yao模型，在[7]中证明了著名的Needham-Schroeder-Lowe协议，在[5]中证明了3 KP支付协议的变体。除了我们在本文中提出的证明之外，[7，5]中的证明是我们所知道的唯一Dolev-Yao式的计算上可靠的证明。然而，它们比我们在这项工作中提出的要简单得多，因为它只涉及完整性M. Backes/Electronic Notes in Theoretical Computer Science 155（2006）111115性质，而我们的证明另外建立了保密性;此外，Needham-Schroeder-Lowe协议和3 KP协议不使用对称加密，因此承诺问题不会发生，这大大简化了 证 明 。 Needham-Schroeder-Lowe 协 议 的 另 一 个 密 码 学 合 理 证 明 由Warinschi同时开发[45]。证明是从头开始进行的加密方法，使它的正式证明工具的范围之外Laud [31]最近提出了主动攻击下对称加密的Dolev-Yao模型的密码学基础他的工作与形式证明工具有直接的联系，但它是特定于某些机密性属性的，将周围的协议限制为特定语言中的直线程序，并且没有解决与Dolev-Yao 模 型 剩 余 原 语 的 连 接 。 Herzog 等 人 。 [26] 和 Micciancio 和Warinschi [34]最近也给出了主动攻击下的加密基础。他们的结果比[10]中的结果更窄，因为他们是专用于公钥加密的，但考虑稍微简单的实实现;此外，前者依赖于更强的假设，而后者严重限制了可以使用此原语分析的协议和协议属性的类别。[34]的第6节进一步指出了他们的工作的几个可能的扩展，这些扩展在[10]的早期工作中已经存在。Canetti和Herzog[19]最近将相互认证和密钥交换协议的理想泛函与形式语言中的相应表示联系起来。他们把交换的随机数作为密钥，把他们的技术应用到Needham-Schroeder-Lowe协议中。他们的工作仅限于上述功能，与加密库[10]相反，因此没有解决可靠性问题Dolev-Yao模型的一般性。所考虑的语言不允许循环和运算器公钥加密作为唯一的加密操作。此外，他们遵循[34]的思想定义理想和真实迹线之间的映射的方法仅捕获基于迹线的属性（即，完整性属性）;关于保密性属性的推理还需要特别的和功能特定的参数。也正在进行一些尝试，以制定用于处理概率和多项式时间考虑的语法演算，特别是[36，32，37，27]，并且作为第二步，将其编码为证明工具。 这种方法还不能以任何程度的自动化来处理协议。它是对证明密码学的简单确定性抽象的方法的补充，并且在密码学仅以黑盒方式使用的情况下使用这些方法116M. Backes/Electronic Notes in Theoretical Computer Science 155（2006）111纲要第2节介绍了本文中使用的符号，并简要回顾了上述密码库。第3节展示了如何基于该库对Otway-Rees协议进行建模，以及如何在底层模型中表示初始共享密钥。第4节包含了Otway-Rees协议的符号和密码安全属性。第5节证明了符号属性，第6节展示了如何为协议的加密实现导出加密属性。第7节结束2预赛在本节中，我们将概述[10，11，8]的理想密码库，并简要概述其可证明安全的实现。我们首先介绍本文中使用的符号2.1符号让↓表示可作为所有函数和算法的域和范围的加法的误差元素。列表操作被表示为l：=（xl，.，x j），并且参数可以明确地检索为l [i]，其中l [i]=↓ if i> j。数据库D是一组函数，称为条目，每个条目在有限域称为属性。对于条目x∈D，属性写的是x。att. 对于涉及属性的谓词pred，D[pred]表示其属性fullpred的条目的子集。如果D[pred]只包含一个元素，我们对这个元素使用相同的符号2.2理想密码库与现实密码库综述[10，11，8] o的理想（抽象）密码库为其用户提供抽象密码操作，例如加密或解密消息的命令，制作或测试签名以及生成随机数。所有这些命令都具有简单的确定性语义。为了允许反应式场景，该语义基于状态，例如，谁已经知道哪些术语;状态表示为数据库。每个条目具有类型（例如，“密文”），以及指向其参数的指针（例如，密钥和消息）。此外，每个条目包含那些已经知道它的参与者的句柄。发送操作使其他参与者知道条目，即，它将句柄添加到条目。理想的加密库不允许作弊。例如，如果它收到一个命令，用某个密钥加密消息m，它只需要为密文创建一个抽象的数据库条目。其他用户只能M. Backes/Electronic Notes in Theoretical Computer Science 155（2006）111117如果他已经获得了密文和密钥的句柄，则请求解密该密文。为了证明密码的可信性，该库基于[42]中介绍的异步反应系统的详细模型，并表示为确定性机器THH，称为可信主机。参数-eter H {1.，n}表示诚实的参与者，其中n是参数图书馆的总面积表示参与者的总人数。取决于所考虑的集合H，可信主机为对手提供稍微扩展的能力。然而，对于当前目的，可信主机可以被视为稍微修改的Dolev-Yao模型以及网络和入侵者模型，类似于真正的密码库向其用户提供与理想密码库相同的命令，即，诚实的用户通过句柄对加密对象进行操作。这些对象现在是真正的密钥、密文等，由真正的分布式机器处理。在不安全的通道上发送一个术语会将实际的位串释放给对手，对手可以随心所欲地使用它。攻击者还可以在非真实信道上插入任意位串。命令的实现基于根据标准密码定义的任意安全加密和签名系统，具有某些附加功能，如类型标记和附加随机化。[10]的安全性证明指出，真实库至少与理想库一样安全。这是使用反应式模拟性的概念来捕获的[42，13]，该概念指出，无论对手在实际实现中可以实现什么，另一个对手都可以在给定理想库的情况下实现，否则底层密码学可能会被破坏。这是真实系统和理想系统之间可能存在的最强密码关系。特别是，它涵盖任意主动攻击。 此外，在底层模型[42，12]中存在一个组合理论，它指出人们可以用真实的库安全地替换较大系统中的理想库，即，而不破坏已经建立的可模拟性关系。2.3密码库状态的详细描述我们以理想密码库的状态的严格定义来结束本节。[10，8]中对用于对Otway-Rees协议建模的理想库的命令以及对略微扩展的对手能力建模的本地对手命令进行机器THH在u中有端口？outu！对于来自每个用户的输入和输出，u∈H，并且对于u=a，表示对手。符号118M. Backes/Electronic Notes in Theoretical Computer Science 155（2006）111n，L遵循CSP惯例，例如，密码库在u中获得消息？已在u！中输出除了用户的数量n之外，理想的密码库还通过长度函数的元组L来参数化，该长度函数用于计算抽象条目的此外，L包含消息长度和每个端口接受的输入数量的界限这些界限可以是任意大的，但必须是多项式有界的安全参数。使用[10]的符号，理想的密码库是一个系统哭，IDn，L由多个结构（{THH}，SH）组成，每个值对应一个结构参数H。每个结构都由一组机器组成，这里仅包含单个机器THH，以及集合SH：={inu？，outu！| u ∈ H} denotingthose ports of THHthat the honest users connect to.形式上，我们获得Syscry，id：={（{THH}，SH）|H {1，...，n}}。在下文中，为了简单起见，我们省略参数n和L。3THH的主要数据结构是数据库D。D的条目是系统运行期间产生的数据的抽象表示，以及关于谁知道这些数据的信息。D中的每个条目都具有以下形式（请回忆一下第2.1节中的注释）（ind，type ，a rg ，hndu1， . . ，hnd um，hnda，len），其中H={u1，.，um}。对于每个条目x∈D：• X. ind ∈ IN DS，称为索引，连续编号D中的所有条目。集合IN DS同构于N，用于区分索引参数。索引用作数据库的主键属性也就是说，我们将选择D[ind=i]写成D[i• X. type∈ typi表示x的类型。• X. arg =（a1，a2，.，aj）可能是空的参数列表。 许多值a i是D中的其他条目的索引，因此也是IN DS中的索引。我们有时用上标“ind“来区分它们• X. hndu∈ HN DS <${↓} for u ∈ H <${a}是用户或对手u通过其知道该条目的句柄。X. hndu= ↓表示u不知道该条目。 集合HN DS是与N同构的另一个集合。 我们总是用上标“hnd “表 示句 柄。• X. len∈N0表示条目的“长度”;它是通过应用来自L的函数来计算的。[3]因此，这些参数在形式上也是理想Otway-Rees系统的参数SysOR，我们在3.2节中介绍的ID。SysM. Backes/Electronic Notes in Theoretical Computer Science 155（2006）111119u，vu，TT，u最初，D是空的。THH对于D的当前大小具有计数器大小∈INDS。对于句柄属性，它的计数器curhndu（当前句柄）初始化为0。3奥特韦-里斯协议Otway-Rees协议[39]是一个四步协议，用于在两个用户之间建立共享的加密密钥该协议依赖于一个区别的可信第三方T，即， T∈ {1，.，n}，并且假设每个用户u最初与T共享秘密密钥Kut。 在典型方案符号，Otway-Rees协议工作如下。41.u→v：M，（Nu，M，u，v）Kut2.v→T：M，（Nu，M，u，v）Kut，（Nv，M，u，v）Kvt3.T→v：M，（Nu，Kuv）Kut，（Nv，Kuv）Kvt4.v→ u：M，（Nu，Ku v）Kut.3.1在抽象库为了捕获用户和可信第三方之间共享的密钥已经生成并分发，我们假设数据库中已经存在密钥的合适我们将u的句柄表示为与v共享的秘密密钥，其中u ∈ {1，... ，n}且v = T或反之亦然，如skse_hnd。更正式地说，我们从一个最初为空的数据库D开始，对于每个用户u∈H，添加以下形式的两个条目（第一个作为实际秘密密钥的公钥标识符，如下所述，更多详情）：（ind：=pkseu，type：=pkse，arg：=（），len：= 0）;（ind：=skseu，type：=skse，arg：=（ind−1），hndu ：=sksehnd，hndT：=sksehnd，len：= skse len（k））。这里pkseu和skseu是两个连续的自然数;将公钥标识符视为长度为0是[8]证明中的技术性问题，而skse lenk（k）表示密钥的抽象长度。这些长度在下文中将不重要。第一个条目必须被合并，以反映对手在现实世界中可能具有的关于对称加密方案的特殊能力。例如，对手必须有可能对抗[4]为了简单起见，我们省略了在第一个和第二个消息的未加密部分中显式包含u和v，因为加密库已经提供了消息的（声称的）发送者的身份，这对我们的目的来说是足够的120M. Backes/Electronic Notes in Theoretical Computer Science 155（2006）111u不uuuu不理想的库，用于检查是否已经使用相同的加密密钥创建了加密，因为对称加密方案的定义并不排除这一点，因此它可以在真实系统中发生。对于公钥加密，这在[10]中通过用相应的公钥标记密文来实现，以便可以比较公钥。对于对称加密，这是不可能的，因为不存在公钥，因此这个问题通过用一个无意义的“公钥”标记抽象密文请注意，秘密密钥的参数指向其密钥标识符。在下文中，公钥标识符将不再重要。我们省略了如何通过命令gen symenc key添加用户u的这些条目的细节，然后是命令send s，用于通过安全通道发送秘密密钥3.2使用抽象库我们现在在[42]的框架中使用理想的密码库对Otway-Rees协议进行建模。对于每个用户u∈ {1，.，n}我们定义一个机器MOR，称为协议机，它执行上面概述的参与者身份协议。联合它通过端口KS outu！，在u？（outu？我们进一步将可信第三方建模为机器MOR。它不连接到任何用户，而是通过T！T？的协议机器MOR、可信第三方MOR和uT可信主机THH是理想的Otway-Rees系统SysOR，id。如图1所示;H和A对任意联合诚实用户和对手进行建模，分别使用[10]的符号，我们具有S ysOR，id：={（MH，SH）|H{1 ， . ， n}} ， 参 见 第 2.3 节 中 理 想 密 码 库 的 定 义 ， 其 中 MH ：={THH}<${MOR|u∈H<${T}}和SH：={KSinu？，KSou tu！ |u∈H}，即，对于给定的诚实用户集合H，只有协议机器M或u∈H实际存在于协议运行中。其他人都被归入敌手。协议机M OR的状态由位串u和形式为（nhnd，mhnd，v，j）的对的集合Nonce u组成，其中nhnd，mhnd是句柄，v∈ {1，.，n}，且j∈ {1，2，3，4}。 直觉上，一对（nhnd，mhnd，v，j）状态该MOR在会话中的协议的第j步中生成句柄nhnd使用v和会话标识符mhnd运行。集合Nonceu最初是空的。可信第三方MOR维护初始空集合SIDT以存储已经处理的会话ID。M. Backes/Electronic Notes in Theoretical Computer Science 155（2006）111121uu不WWuuuu系统OR，IDSyscry，idFig. 1. Otway-Rees理想系统我们现在定义协议机MOR评估输入。 他们或者来自u中端口KS的用户u？或从港口出口U的THH？。两种情况下的MOR的行为分别在算法1和3中描述我们将在下面描述可信第三方MOR仅接收输入，其行为在算法2中描述。我们将算法j的步骤i称为步骤j.i。如果对密码库的命令没有产生期望的结果，例如，如果解密请求失败。为了可读性，我们在算法描述中省略了这些中止检查;相反，我们对所有三个算法都施加了以下约定。约定1对于所有w∈ {1，.，n}{T}以下情况成立。如果MOR在w！并在输出端口W接收↓？作为密码库的即时答案，则MOR中止执行当前算法，除非命令的形式是list proj或send i。方案开始。协议机MOR的用户可以与用户v∈ {1，.，n}\{u}通过在u？中的端口KS处输入（new prot，Otway Rees，v）来实现。我们的安全证明适用于所有对手和所有诚实的用户，即，特别是那些与对手（分别是恶意用户）一起启动协议的协议，与诚实用户的协议并行。在这样的输入时，MOR根据算法1使用理想密码库建立对应于第一协议消息的项。命令gen nonce生成理想的nonce以及会话标识符。MOR将所得到的句柄nhnd和mhnd存储在随机数u中以用于将来的比较，以及v的身份和这些句柄是在随机数u的第一步骤中生成的指示符H你知道吗？KS _in u！KS_outv？K S _inv！KS_outu！KS_inu？KS_outv！KS_inv？M或uM或vM或不出去吗？inu！出V？在v！T？在T！outu！在u？出来V！在v？出T！在T？出一THH一中122M. Backes/Electronic Notes in Theoretical Computer Science 155（2006）111uu1uv我我2乌库特我1我22v3Kvt算法1. 来自用户的输入评价（方案开始）输入：（新保护，OtwayRees，v）在KS（u）？ 其中v ∈ {1，. ，n}\{u}。1：nhnd←gennonce（）.2：IDhnd←gen nonce（）。3：Nonce u：= Nonce u {（nhnd，ID hnd，v，1）}。4：uhnd←store（u）.5：vhnd←store（v）.6：lhnd←list（nhnd，IDhnd，uhnd，vhnd）.1U7：chnd←sym encrypt（sksehnd，lhnd）.1u， T18：mhnd←list（IDhnd，chnd）.1 19：发送i（v，mhnd）。议定书命令库将任意应用程序数据输入密码库，这里是用户标识u和v。命令列表形式列表和sym加密是对称加密。最后的命令send i意味着MOR通过不安全的通道将结果项发送给v其结果是，对手获得了一个术语的句柄，可以决定什么”（《易经》卷一）“以其为上，以其为下，以其为下。算法2. 可信第三方的行为Input：（v，T，i，mhnd）atoutT？其中v∈ {1，. ..， n}。1：IDhnd←list proj（mhnd，1）.{IDhnd}HND2：type 1← get type（ID）.3：c（3）hnd←listpr oj（mhnd，3）.{c（3）hnd{N，M，u，v} }4：l（3）hnd←symdecrypt（s k sehnd，c（3）hnd）.{l（3）hnd{N，M，u，v}}T，vv5：yhnd←listpr oj（l（3）hnd，i），其中i=1，2，3，4。6：yi←retrieve（yhnd）for i = 3，4.7：if（IDhnd∈SIDT）（type8：中止9：如果结束/=nonce）（yhndIDhnd）（y3/∈ {1，.，n}\{v}）n（y4v) 然后10：SIDT：= SIDT{ID hnd}。11：c（2）hnd←listpr oj（mhnd，2）.{c（2）hnd{N，M，u，v} }12：l（2）hnd←symdecrypt（s k s ehnd，c（2）hnd）.{l（2）hnd{N，M，u，v}}T，y3u13：xhnd←listpr oj（l（2）hnd，i），其中i=1，2，3，4。HND14：type2←get type（x）.15：xi ← retrieve（xhnd）for i = 3，4.亨德亨德16：if（type2/=nonce）<$（x y）<$（x3 /= y3）（x4 （4）y，第17章：放弃18：如果结束19：sksehnd← gen symenc key（）.{sksehndKuv}20：l（2）hnd← list（xhnd，sksehnd）.{l（2）hnd {N ，K}}313uUV21：c（2）hnd←symencrypt（s k sehnd，l（2）hnd）.{c（2）hnd}{N， K } }个文件夹3T，y333U紫外线库特22：l（3）hnd← list（yhnd，sksehnd）.{l（3）hnd {N ，K}}313vUV23：c（3）hnd←symencrypt（s k sehnd，l（3）hnd）.{c（3）hnd}{N， K } }个文件夹3T，v 33V紫外线Kvt24：mhnd←listt（IDhnd，c（2）hnd，c（3）hnd）.{mhndM，{N， K 个文件夹，{N，K}}33 325：发送i（v，mhnd）。3U紫外线库特vuvKvt1M. Backes/Electronic Notes in Theoretical Computer Science 155（2006）111123uuuuu不协议机的网络输入评估。协议机MOR在端口outu处接收到来自密码库的输入时的行为？（对应于通过网络到达的消息）在算法3中类似地定义。 通过构造THH，这样的输入总是（v，u，i，mhnd）的形式，其中mhnd是列表的句柄。为了增加可读性，并澄清算法描述和通常的协议符号，我们在算法的右侧增加解释性注释，以描述哪个句柄对应于哪个Dolev-Yao项。我们进一步使用命名约定，传入和传出消息被标记为m，其中传出消息具有对应于协议步骤的附加下标。加密被标记为c，加密列表被标记为l，两者都具有合适的子和上标。MOR首先确定会话标识符，如果它不是nonce类型，则中止。MOR然后检查所获得的消息是否对应于协议的第一、第三或第四步。（回想一下，第二步仅由T执行。）这通过在集合Nonceu中查找会话标识符来实现。之后，MOR通过利用Nonceu的内容来检查所获得的消息是否确实是针对特定步骤和特定会话ID的适当构造的消息。如果是，则MOR根据协议描述构造消息，将其发送到预期的接收者，更新集合Nonceu，并且可能向其用户发信号通知密钥已经成功地与另一用户共享。可信第三方的行为。MOR在接收到来自密码库的输出端口T处的输入（v，T，i，mhnd）时的行为？在算法2中定义类似。我们省略了一个非正式的描述。3.3关于多项式时间为了使用底层模型的现有合成结果，协议机MOR和MOR必须是多项式时间的。 类似于cryp-w不拓扑图库，我们定义这些机器中的每一个都维护显式的消息长度和每个端口接受的输入数量的多项式界限。124M. Backes/Electronic Notes in Theoretical Computer Science 155（2006）111uuvKv.2我2142我21v2uv vvvuuv KutuUV库特算法3. TH H（网络输入）的输入评估Input：（v，u，i，mhnd）atoutu？其中v∈{1，...，n}\{u}。1：IDhnd←list proj（mhnd，1）.{IDhnd}HND2：type 1← get type（ID）.3：如果类型14：中止5：如果结束nonce则6：如果v/=Tj，nhnd：（nhnd，IDhnd，v，j）}/∈Nonceu，则{输入第一消息}7： c（2）hnd←listpr oj（mhnd，2）.{c（2）hnd{N，M，v，u }8： nhnd←gen nonce（）.9： Nonce u：= Nonce u {（nhnd，IDhnd，v，2）}。10： uhnd←store（u）.11： vhnd←store（v）.12： l（3）hnd←list（nhnd，IDhnd，vhnd，uhnd）.{l（3）hnd<$N，M，v，u}2U2U13： c（3）hnd←symencrypt（s k s ehnd，l（3）hnd）.{c（3）hnd{N，M，v，u }2u， T22uKut14： mhnd←listt（IDhnd，c（2）hnd，c（3）hnd）. {mhnd<$M，（N，M，v，u），（N，M，v，u）}2215： 发送i（T，mhnd）。2v Kvtu库特16：否则，如果v=T，则{第三消息被输入}17： c（2）hnd←listpr oj（mhnd，2）.{c（2）hnd{N， K） }的情况18： c（3）hnd←listpr oj（mhnd，3）.{c（3）hnd{N， K） }的情况19： l（3）hnd←symdecrypt（s k s ehnd，c（3）hnd）.{l（3）hnd}N， K 个文件夹u，T20： yhnd←listtpr oj（l（3）hnd，i），其中i=1，2。uUVHND21： type 2← get type（y）.22： if（/否！w∈ {1，.，n}\{u}：（yhnd，ID hnd，w，2）∈Nonce u）（type/=skse），则第二十三章：放弃24：如果结束25： Nonceu：=（Nonceu\ {（yhnd，IDhnd，w，2）}）{（yhnd，IDhnd，w，3）}。1 126： mhnd <$list（IDhnd，c（2）hnd）.{mhndM，{N， K } }个文件夹4 427： 发送i（w，mhnd）。28： 输出（ok responder，Otway Rees，w，IDhnd，yhnd），KS outu！vUVKvt29：else if vT！nhnd：（nhnd，IDhnd，v，1）则{输入第四消息}30： c（2）hnd←listpr oj（mhnd，2）.{c（2）hnd}{N， K } }个文件夹31： l（2）hnd←symdecrypt（s k s ehnd，c（2）hnd）.{l（2）hnd}{N， K }}个文件夹u，T32：对于i = 1，2，xhnd←listpr oj（l（2）hnd，i）。u uvHND33： type3←get type（x）.34： ifxhnd=/第35章：放弃36：如果结束n型/=skse然后37： Nonceu：=（Nonce u\{（xhnd，IDhnd，v，1）}）{（xhnd，IDhnd，v，4）}。1 138： 输出（ok initiator，Otway Rees，v，ID hnd，xhnd）在KS输出u！39：其他第40章：放弃41：如果结束4安全属性23M. Backes/Electronic Notes in Theoretical Computer Science 155（2006）111125在下文中，我们形式化了理想的和实际的Otway-Rees协议的安全性该性质由密钥保密性和一致性组成。我们首先形式化了理想密钥保密属性，它是基于理想密码库的任意协议的一般密钥保密定义的实例化。[9]它是在[9]中引入的，并且是象征性的。126M. Backes/Electronic Notes in Theoretical Computer Science 155（2006）111基于术语不是对手知识集的元素的典型概念在给定的Dolev-Yao式库中，对手然后介绍了密码学的概念，基于真实密码库的真实或随机密钥保密。最后，我们表示的一致性属性，我们区分完美的和计算的性质的实现。4.1关键秘密财产的定义定义符号密钥保密性的第一步是考虑理想的Dolev-Yao风格库的一种状态，并定义句柄指向对称密钥，该密钥在符号上不为对手所知，并且没有用于加密。在这些符号条件下，我们可以希望证明相应的真实密钥与对手的新随机密钥是不可区分的。注意，在这个意义上，Otway-Rees协议对新密钥执行的操作是允许的。对于定义中的条件（3），请注意密文项的参数是（l，pk），其中l是明文索引，pk是公共索引标记，其中pk=sk-1表示密钥索引。定义4.1（符号秘密加密密钥[9]）令{T} H{1，.，n，T}，TH H的数据库状态D，以及用户和句柄的一对（u，lhnd）∈ H×HN DS. 令i = D [hnd u= lhnd]。ind是对应的数据库索引（u，lhnd）（1）下的项是对称加密密钥i，D [i]. type= skse，（2）在符号上是未知的（对于对手）i D [i]。hnda=↓，（3）还没有被用于加密，或短是未使用的，i对于所有索引j∈ N，我们有D [j]。type=symencD [j]. arg [2]/= i-1，以及（4）是符号上的秘密密钥i，它具有前面的三个性质。秘密密钥置信函数是一种用来指定需要证明其秘密性的密钥的通用方法。[9]的基本理论就是基于这样的函数。我们将它们实例化为Otway-Rees协议，从而基本上用于所有单独的密钥交换协议。秘密密钥置信函数将用户视图映射到用户、句柄和类型的三元组（u，lhnd，t对于Otway-Rees协议，我们定义了秘密密钥信任函数seckeys initiator OR用于发起者和seckeys responder OR用于指定交换的密钥。定义4.2（用于Otway-Rees协议的秘密密钥置信函数）集合H的秘密密钥置信函数是将用户的每个视图映射到（H ×HNDS×{skse}）n的一个元素的函数seckeys。秘密密钥信任函数 seckeys发起者OR和seckeys响应器或的的Otway-Rees议定书地图每个M. Backes/Elec