Dolev-Yao模型与哈希函数的可靠性计算模型

理论计算机科学电子笔记186（2007）121-139www.elsevier.com/locate/entcs基于Hash函数RomainJan vierandYassineLakhnechandLaurentMazar'e1VERIMAG，2 av. deVignates 38610 Gieres，FRANCE摘要在本文中，我们考虑一个Dolev-Yao模型与哈希函数，并建立其可靠性的计算模型。合理性意味着Dolev-Yao模型中没有攻击意味着对手在计算模型中执行攻击的概率可以忽略不计。确定性哈希函数的经典要求（例如单向性，无冲突性）不足以证明这一结果。因此，我们引入了新的安全要求，这些要求足以证明结果的可靠性，并通过随机预言机进行验证关键词：安全，密码协议，形式加密，概率加密，密钥哈希函数，Dolev-Yao模型，计算模型。1介绍动机从历史上看，加密协议的验证分为两个不同的分支。密码协议的符号验证（也称为形式验证）起源于Dolev和Yao的工作[14]。这种方法的基本部分是完美的密码学假设，可以大致总结如下：消息表示为代数项，新鲜随机数的创建是完美的，也就是说，随机数在无限域上的范围和新鲜度是绝对的，密钥创建也是如此。此外，没有办法猜测随机数或密钥，并且除非已知用于加密消息的密钥的逆，否则不能从加密消息中提取信息在这种方法中，有一个单一的攻击者被建模为一个无限的过程，其计算资源没有限制。尽管对密码学原语有很强的假设，但在被认为是1电邮地址：{romain.janvier，yassine.lakhnech，laurent.mazare}@ imag.fr1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.01.066122R. Janvier等人理论计算机科学电子笔记186（2007）121最著名的是G。[18]他们中的一些人在[10]中列出。关于这种方法的好消息是，已经开发了丰富的自动验证方法和工具[21，8，7，2]。在计算方法中，密码原语对比特串进行操作，其安全性被定义为任何攻击者的高复杂性和弱成功概率（例如[16]加密）。协议和攻击者都是随机的多项式时间图灵机。这种计算方法被认为比形式化方法更现实，然而，其复杂性使得设计自动验证工具非常困难建立符号验证的计算可靠性允许两全其美，即一方面是自动验证，另一方面是计算正确性。相关工作。在过去的几年里，一些作品集中在弥合这两种方法之间的差距 在他们的开创性论文[1]中，Abadi和Rogaway证明了符号模型中的消息不可否认性的概念在计算模型中是有效的，前提是用于实现消息的加密方案这意味着，如果两个消息在符号模型中不可区分，则它们的计算实现不能由图灵机在合理的（多项式）时间内分离。本文讨论的被动攻击者只能窃听，但不能改变或阻止消息。主动攻击者被认为是在[19，12，17]。这些论文证明，如果加密方案满足针对选择密文攻击的语义安全性，则符号模型中的安全性意味着计算模型中的安全性。Cortier和Warinschi在[12]中证明了使用非对称加密和数字签名的协议的符号模型的安全性，扩展了[19对于允许密钥传输的协议，类似的结果已经在[17]中得到了验证。Cortier，Kremer，Ku？stersanddWarinschi[11]利用随机预言模型用散列函数扩展了这些结果.符号分析的可靠性已经在Backes，Pittzmann和Waidner [3]的黑盒反应模拟（BRSIM）框架中得到了证明。最近，这个结果被推广到随机预言模型中的散列函数，并且证明了这种推广在标准模型中是不可能的。考虑到BRSIM模型的强度，这个不可能性结果不会自动延续到[11]中使用的Dolev-Yao模型。不依赖于随机预言模型的哈希函数的可靠性结果在[15]中给出。然而，只考虑被动的对手，哈希函数必须是概率性的[9]。捐款.我们在基于[19]的符号模型中建立我们的结果。这个结果并不直接依赖于随机预言模型，而是我们引入了新的安全要求，在随机R. Janvier等人理论计算机科学电子笔记186（2007）121123Oracle模型传统的哈希函数的要求是无冲突和前像抵抗，我们保持无冲突，但要求不可伪造性要求，而不是前像抵抗。由于散列函数是确定性的，因此要求对手不能产生他选择的消息的散列是不合理的。相反，我们要求对手很难计算包含随机采样的随机数的消息的哈希。这个随机数不给对手，但他可以请求包含这个随机数的消息的散列使用这些新的要求，哈希函数和语义安全的选择密文攻击的非对称加密，我们证明了计算的可靠性的符号模型的协议，使用非对称密码，图形和散列函数。纸组织。下一节回顾了使用计算模型的必要条件在第3节中，介绍了协议以及它们的符号和计算语义。在第4节中，我们介绍了我们对密码原语的要求。第5节包含了我们的主要结果：使用散列函数的原算法的计算可靠性。我们以简短的讨论结束本文2预赛2.1密码方案非对称加密方案AE=（KG，E，D）由三种算法定义。 密钥生成算法KG是随机化函数，其在给定安全参数η的情况下输出一对密钥（pk，sk），其中pk是公钥，sk是相关联的秘密密钥。加密算法E也是一个随机函数，它给出一个消息和一个公钥，输出由公钥加密的消息。最后，解密算法D将秘密密钥和密文作为输入，并输出相应的明文，即，D（E（m，pk），sk）=m，条件是（pk，sk）已经由密钥生成算法生成。这三个算法的执行时间被假设为多项式有界的η。带密钥的散列函数H[6]是确定性函数，其将密钥k和比特串bs作为输入，并输出与k相同长度的比特串。散列键可以是长度为η的任何位串。本文只考虑包含非对称加密方案和带密钥的散列函数的密码库CL，也只考虑长度保持的加密方案，即密文的长度仅取决于明文的长度和安全参数η。2.2随机图灵机与Oracle计算世界中的对手是概率多项式图灵机（PPTM），它可能会访问一些神谕。为了定义一个可以使用预言机O的对手A，我们写：124R. Janvier等人理论计算机科学电子笔记186（2007）121对手方和A/O：可以访问O的A的代码时间复杂度O（x）由PPTMF完成的具有oracle实现的A的执行由A/λs.F（s）表示。函数g：R→R是可忽略的，如果对于所有c >0，存在Nc，使得g（x） Nc。3协议的语义和语义在本节中，我们考虑允许各方使用公钥加密和哈希函数交换由身份和随机生成的数字构建的消息的协议。我们假设使用协议的每个参与者都使用相同的哈希密钥，因此我们不在协议的语法中表示这个密钥。在协议执行期间可以执行三种类型的指令：接收消息、发送消息或测试散列。为了描述一个特定的指令，我们使用自由代数中的术语，其排序如下• 随机数的随机数排序。• 主体标识的排序Ident• 公钥和私钥的排序分别为Pubkey和Privkey• 包括所有其他排序的排序术语签名包括以下功能符号及其对应的字母：• enc：Term×Pubkey→Term。我们使用{t}k作为enc（t，k）的简写• h：术语→术语。• pair：Term×Term→配对的Term，其中，pair（t1，t2）使用t1，t2我们假设从公钥到私钥的一对一映射将每个密钥k与其逆密钥k−1关联起来。这种映射从私钥扩展到公钥，使得（k−1）−1=k。协议是使用这个代数中的术语和类型化变量来指定的。 的是，我们允许不相交的变量集，范围在不同的排序。一个术语被称为原子，如果它是一个键，一个随机数或一个变量。基项，即变量自由项，称为信息。3.1协议通常，一个协议是由一个有限序列的主要身份与相关的角色。一个角色由一系列指令指定，这些指令可以由运行该角色的主体执行因此，一个n方协议是一个映射<$：[0，···，n-1] →Ident×Role，其中Role = inst，指令集inst定义如下：inst：：= Rec（t）|Snd（t）|[h（t）= x]R. Janvier等人理论计算机科学电子笔记186（2007）121125B一一一其中t是项，x是变量。 指令Rec（t）表示接收一条消息（以及使用原型t进行的模式匹配，它不应该包含哈希），Snd（t）表示t的发射，最后，[h（t）=x]检查x的值是否是t的值的哈希。角色R是一个有限指令列表，集合原子（R）包含出现在R中的每个原子或其逆（对于键）出现在R中。作为语义的并行组合的角色，我们采取通常的交织语义。我们只考虑有限数量的会话。现在，很容易看出，考虑了有限多个角色，并且每个角色由顺序执行的有限数量的指令组成，因此不同角色的并行执行的可能交织的数量有界为2。因此，为了简化演示，并且不失一般性（除了我们只考虑有界协议），我们考虑只包含单个角色的协议为了正确定义使用单个角色的协议，我们还必须指定角色中使用的原子最初被对手知道我们假设不诚实的参与者是在协议执行开始之前被选择的。因此，一个协议是一个对（R，IK），其中R是一个角色，IK是原子（R）的子集，代表对手的初始知识。集合IK包含来自R的用于非对称加密的所有身份和公钥。它还包含与不诚实的参与者相关的私钥。让我们在经典的Needham-Schroeder协议[18]上说明我们的定义和语法。BAN符号中的协议描述如下：A→B：{A，NA}pkBB→A：{NA，NB}pkAA→B：{NB}pkB让我们考虑两个会话：一个是A和B之间的会话，另一个是A和对手I之间的会话。该协议涉及两个角色，我们考虑交织，B的角色（与A通信）和A的角色（与I通信）：角色AB：Rec（{A，y}pk）。Snd（{y，NB}pk）BB A角色AI：Snd（{A，NJ}pk）。Rec（{NJ，x}pk）. Snd（{x}pk）A AIAA I该协议包括两个角色的并行组合和角色AI。让我们考虑对应于[18]的中间人攻击的单角色协议k =（R，IK）。角色R是：Snd（{A，NJ}pkI）A在会话A中发送其第一个消息，IRec（{A，y}pkB）. Snd（{y，NB}pkA）B在会话A，B中接收其第一个消息和答案Rec（{N J，x}pkA）. Snd（{x}pkI）A在会话A中接收其应答，I[2]虽然这个数字在会话数量上是指数级的，但许多自动工具被设计用于验证无限会话数量的协议。这些工具给出的安全结果确保了有限数量会话的安全性。126R. Janvier等人理论计算机科学电子笔记186（2007）121我入侵者的初始知识IK包含身份A、B和I以及公钥pkA、pkB和pkI和秘密密钥skI=pk−1，因为参与者I是不诚实的。3.2可执行协议我们现在定义可执行协议。定义3.1如果：(i) 出现在发送动作Snd（t）中的任何变量必须在接收动作Rec（tJ）之前出现。这确保了在执行Snd（t）时，t的(ii) 任何出现在动作[h（t）=x]中的变量必须在接收动作Rec（tJ）之前出现。此外，我们假设密钥不出现在发送的消息中。我们考虑两个不同的协议语义：一个在符号模型和计算模型。两者都定义了协议面对对手时的行为。这个对手完全控制了网络。此外，广告商冒充不诚实的参与者。在符号情况下，协议和对手交换符号消息。对手可以做出的演绎由演绎关系定义。在计算的情况下，它们交换比特串。对手是一个多项式随机图灵机，因此可以执行任何它想要的操作。3.3符号语义学为了定义协议的符号语义，我们引入了蕴涵关系 Em，其中E是一组有限的消息，m是一条消息。直觉上，Em意味着m可以从消息集合E[14]中推导出来。设H是由（R，IK）给出的协议。关系Em被定义为最小二元关系，它验证：(i) 如果一个原子a出现在IK中或不出现在atoms（R）中，则E是a。(ii) 如果m∈E，则E<$m。(iii) 如果E m和E n，则E m，n。(iv) 如果Em，n，则Em和En。(v) 如果Em和Ek，则E{m}k。(vi) 如果E{m}k且Ek−1，则Em。(vii) 如果Em，则Eh（m）。注3.2第一条规则引入了对手的初始知识。攻击者可以推导出IK中的任何原子，也可以生成新的原子（即原子（R）中一个符号跟踪是一个发送和接收消息的列表，R. Janvier等人理论计算机科学电子笔记186（2007）121127一一BA由Snd（m）和Rec（m）表示，其中m是消息。显然，有一些消息序列是不可行的。定义3.3[有效替换和有效迹]设k =（R，IK）是一个协议。设σ是一个基代换，RJ=inst1，···，instn是R的前缀. 对于任何i = 1，···，n，使得insti= Rec（t），令Ti={tJ|< i·instj= Snd（tJ）}。然后，如果满足以下条件，则σ是对σ的有效替换，对于i= 1，···，n：(i) 如果insti=Rec（t），则tσ可以从之前发送的消息中推导出来，即Tiσtσ。(ii) 如果insti= [h（t）=x]，则xσ=h（tσ）。如果σ是一个有效的替代，我们称消息序列m1，···，mk通过删除所有验证测试从RJσ获得一个有效的迹。 此外，所有有效迹的集合被表示为迹（Traces）。Q例3.4让我们再次考虑前面介绍过的Needham-Schroeder协议。[18]中提出的中间人攻击只使用了以下角色前缀：Snd（{A，N J}pkI）A在会话A中发送其第一个消息，IRec（{A，y}pkB）。Snd（{y，NB}pkA）B接收其第一个消息并回答Rec（{NJ，x}pkA）。 Snd（{x}pkI）A在会话A中接收其应答，I那么攻击对应于有效替换σ，定义如下：σ=. x→N，y→Nj下面给出相应的跟踪。很容易检查此跟踪是否有效。Snd（{A，NA}pkI）. Rec（{A，NA}pkB）. Snd（{NA，NB}pkA）.Rec（{NA，NB}pkA）. Snd（{NB}pkI）。Q3.4计算语义学我们想让对手对网络进行任意控制，就像在符号模型中一样，因此我们消除了网络。此外，对手通过向其他参与者发送消息和从他们那里接收消息来驱动计算。在计算模型中，交换的消息是位串（并且取决于安全参数η）。然而，我们假设对应于不同范围的密码原语的类型：主身份，随机数，公钥，私钥，密文，哈希和对，分别为Mag，Mn，Mpk，Msk，Ma，Mh和Mp此外，我们假设一个多项式时间类型检索函数type：M→Types，其中Types是所有类型的集合。我们还假设只有当类型一致时，位串的相等性才成立，即。bs=bsJ意味着type（bs）=type（bsJ）。关于对，我们假设有两个确定性多项式算法pr1和pr2使得pri（bs1·bs2）=bsi.128R. Janvier等人理论计算机科学电子笔记186（2007）121现在，计算轨迹是分别由Snd（bs）和Rec（bs）表示的比特串的发射和接收的序列，其中Snd（bs）是由主体发送并由对手接收的消息，而Rec（bs）是由主体接收并由对手发送的消息在本节中，设k =（kinst1，···，instlk，IK）是一个固定的任意协议。此外，设CL是由非对称加密方案AE=（KG，E，D）和带密钥的散列函数H组成的密码库。计算语义由图3.1中给出的随机算法Exec定义。• Exec作为输入被给予对手A、协议A =（inst1，···，inst1，IK）以及从位串到来自原子的随机数、密钥和身份的初始映射θ（inst1，···，inst1，IK）。θ的值是使用CL的密钥生成算法和生成随机数值的算法计算的。因此，我们写θ← Init（θ）来表示θ的初始值的采样。我们假设θ也将一个散列键与kH相关联。我们称IK（θ）为θ对IK中原子和kH的限制。• Exec的输出是一个计算轨迹，记录了攻击者和运行协议的主体之间的交互，以及攻击者的最终替换θ和最终内存θ。我们在第5节中的主要定理指出，所产生的计算迹对应于具有压倒性概率的有效当考虑协议上的属性时，使用其他输出θ和θ• Exec修改θ，它还使用一个列表跟踪，其中包含Exec最终输出的计算跟踪。Exec使用两个辅助函数：(i) concr，它将项t和计算替换θ作为参数，并返回计算值，即t的位串。(ii) parse以位串bs、项t和计算替换θ作为参数，并返回θ的更新版本（通过匹配bs和t获得）。由于空间的限制，我们没有给出比较明显的concr和parse算法。这两个算法使用CL的密码原语。• 在执行过程中可能会出现一些错误。当出现错误时，执行被中止，控制流被转移到Exec中的finalreturn语句。当散列验证测试失败时，Exec或解析函数可能会引发错误。此函数可能在以下情况下引发错误。 需要θ中x的值，但θ（x）未定义或没有期望值;在这种情况下，协议无法执行。当位串的类型不是预期的类型时，或者当对解密算法或投影算法之一的调用失败时，也会引发错误。R. Janvier等人理论计算机科学电子笔记186（2007）121129图3.1Exec算法Exec（A，IK，Xinst1. instlθ，θ）：跟踪：= [];跟踪：=IK（θ）;初始化对于i从1到l匹配instiwith[[h（t1）=t2]]哈希验证ifH（concr（kH，θ），concr（t1，θ））=/concr（t2，θ）then raise测试失败[Rec（t）]消息接收（bs，n）：=A（n）θ：=parse（bs，t，θ）trace：=trace：：Rec（bs）[Snd（t）]消息发射bs：=concr（t，θ）trace：=trace：：Snd（bs）A：=A（bs，A）endmatchendforreturn（trace，θ，θ）3.5协议属性对于符号模型和计算模型，迹属性由下式给出：一组轨迹;第一种情况下是一组符号轨迹，第二种情况下是一组计算轨迹。3.5.1符号属性在符号语义的情况下，如果所有有效的跟踪都是跟踪，则协议满足跟踪属性。定义3.5设A是一个协议，A是一组符号迹。 然后，将满足条件的函数表示为|=f，if Traces（迹）.认证性质，如存活性、弱一致性、非内射一致性，是典型的迹性质。另一个被广泛研究的痕迹属性是不可扣除性。定义3.6设m为符号信息。让它成为一个协议。 我们用Secret（m）表示符号迹的集合m1，···，mn，使得{m1，···，mn}/m，我们说满足Secret（m），如果|=fSecret（m）.3.5.2计算性能计算迹属性是一组计算迹，其是一组位串序列。如果对于任何攻击者，130R. Janvier等人理论计算机科学电子笔记186（2007）121A、IK、R获得不满足该特性的轨迹的概率是可以忽略的。更正式地说，我们有以下内容：定义3.7设k =（R，IK）是一个协议，φ是一组计算迹。然后，满足φ，记为|= cφ，如果对于每个对手A，Pr[θ←Init（θ）;Exec（A，IK，R，θ）/∈φ]作为η的函数可以忽略。请注意，概率是在用于计算θ的掷硬币、A的掷硬币和CL中算法的掷硬币上取的。我们现在定义另一个对应于随机数SecNonce强保密性的性质[12]。这个属性表明，对手很难区分协议执行中使用的nonce和随机nonce。在SecNonceb实验中，在执行协议之后，对手被给予两个随机数值bs0和bs1，并且必须决定在执行中使用哪一个。SecNonceb（A，IK，R，θ，N）：Rηbs0← {0， 1}bs1←R {0， 1}ηθ←θ[bsb/N]（tc，θJ，mem）←RR执行（A，IK，R，θ）d← A（tc，bs0，bs1，n）定义3.8设k是一个协议（R，IK），N是k的随机数对于任何对手来说A，我们将A的SecNonce-优势定义如下：高级SecN一次，NR RA，IK，R（η）= 2Pr [θ←Init（η）;b← { 0， 1};d←R SecNonceb（A，IK，R，θ，N）：d=b]−1如果AdvSecNonce，N（η）可忽略，则协议满足SecNonce（N），对于任何ad-A.4密码原语安全定义是使用安全标准和相关的安全游戏（实验）引入的。安全标准定义了一个涉及对手的游戏。实验如下进行。首先随机产生一些参数θ。 对手被执行，并可以使用依赖于θ的oracleF。 最后，对手必须回答一串由一个R. Janvier等人理论计算机科学电子笔记186（2007）121131一一算法V也使用θ（例如θ包括比特b，对手必须输出b的值）。定义4.1安全准则γ是三元组（Θ;F;V），其中• Θ是PPTM，给定安全值η，随机生成一些挑战θ(for例如比特B和一对密钥（pk，sk））。• F是PPTM，其将位串s和询问θ作为参数，并输出新的位串。F代表对手可以调用以解决其挑战的神谕。• V是一个PPTM，它接受一串比特s和一个挑战θ作为参数，并输出真或假。它代表了对对手计算结果的验证答案是真的（Rep）。假）意味着对手解决了（相应地，没有解决）的挑战。注4.2注意，Θ可以生成任意数量的参数，F可以表示任意数量的预言机。因此，可以用多个Θ和F来定义准则。PPTMA对γ的优势是γ。γγΣAdvA（η）= 2Pr [GA（η）=true] −PrRand其中G是图灵机，定义为：博弈Gγ（η）：θ←Θ（η）d←A（η）/λs.F（s，θ）返回V（d，θ）PrRandγ是对手能够解决挑战的最佳概率不使用OracleF。 形式上，PrRandγγJ是Pr[GA（η）=其中A在任何可能的PPTM范围内，γJ是标准（Θ;θ;V）。我们还考虑具有多个验证者的准则，表示为γ =（Θ; F; V1，.，Vn）。那么对手A的优势定义为：γ。（Θ;F;Vi）Adv（η）=最大值1≤i≤nAdvA（η）如果任何对手对γ的优势可以忽略不计，则标准γ被称为4.1非对称加密对于非对称加密方案，我们使用与经典的IND-CCA准则等价的N-IND-CCA准则[5]。定义4.3[N-IND-CCA]设AE=（KG，E，D）为非对称加密方案。然后，由γN表示的与AE相关联的N-IND-CCA准则由（Θ;F;V）给出，其中：132R. Janvier等人理论计算机科学电子笔记186（2007）121(i) 0使用KG和比特b随机地生成N对密钥（pk1，sk1）至（pkN，skN(ii) V验证对手输出了b位的正确值;(iii) F为1到N之间的每个i提供对三个预言机的访问：(a) - 左右加密预言机，其将两个相等长度的位串（bs0，bs1）作为自变量，并输出具有pki的bsb的加密;(b) 解密预言器，其对不是由前一加密预言器产生的任何消息进行解码;(c) 一个只提供公钥的预言机。非对称加密方案AE称N-IND-CCA i ∈γN是安全的。4.2散列函数哈希函数通常用于减小消息的大小：哈希函数的所有可能输出都具有相同的大小。此外，由于散列算法是确定性的，所以可以测试散列结果和位串对应。然而，散列消息可以用于对比特串进行承诺，因此很难找到两个具有相同散列的消息，这被称为冲突。它还应该从散列消息中分离出来，以恢复底层的位串。以前的可证明密码学工作已经为哈希函数引入了许多安全要求[20]。在这些要求中，最常用的三个标准是：• 原像抵抗（Pre-image resistance，Pre）：给定散列Y和所使用的密钥K，除非具有不可忽略的概率，否则应该不可能找到一个比特串MJ，使得H（K，MJ）=Y。也就是说，对于任何对手A和给定的多项式p，以下概率在η中必须是可忽略的：Pr[K<${0， 1}η;M<${ 0， 1}p（η）;Y← H（K，M）;MJ← A（K，Y）：H（K，MJ）=Y]• 第二原像电阻（Sec）：给定一个位串M和一个密钥K，除非有不可忽略的概率，否则不可能找到一个不同的比特串MJ，使得H（K，M）=H（K，MJ）。也就是说，对于任何对手A和给定的多项式p，以下概率在η中必须是可忽略的：Pr[K<${0， 1}η;M<${ 0， 1}p（η）;MJ← A（K，M）：M MJ<$H（K，M）=H（K，MJ）]• 抗碰撞性：（Col）除非有不可忽略的概率，给定密钥K，否则不可能找到两个不同的位串M和MJ，使得H（K，M）=H（K，MJ）。也就是说，对于任何对手A，以下概率在η中必须是可忽略的：Pr[K<${0， 1}η;（M，MJ）<$A（K）：M/=MJ <$H（K，M）=H（K，MJ）]在前面的三个标准之间有一些众所周知的含义[20]：标准Pre由标准Sec暗示，而Sec本身由Col暗示。R. Janvier等人理论计算机科学电子笔记186（2007）121133由于在符号设置中没有冲突，因此在证明计算可靠性时要求无冲突是很自然的。在符号设置中，对手不能从散列消息h（m）推断出底层消息m。在计算环境中，我们必须确保对手无法从其散列值中推断出位串的重要部分。例如，给定H（kH，bs1·bs2），如果bs1的长度取决于安全参数，则对手不应该能够以不可忽略的概率推断出bs1，或者产生包含bs1的消息的新散列 在这种情况下，Pre和Sec要求并不充分，因为它们仅规定对手不能产生bs1·bs2。另一种确保散列函数安全性的方法是使用概率散列函数citecanetti-hash。虽然citecanetti-hash中描述的安全概念确保任何哈希都保留了哈希消息的任何部分信息，但它并不能确保给定包含秘密随机数的哈希，不可能伪造包含秘密随机数的新哈希。此外，所考虑的散列函数是概率性的。因此，我们定义了一个新的哈希函数标准我们希望确保哈希函数满足某种形式的语义安全性。然而，不可能直接采用经典定义，因为哈希函数是确定性的。攻击者不能完全访问左右散列预言机。因此，我们引入了一个新的安全游戏，其中首先随机抽样一些挑战随机数。对手可以访问左右预言机，但他的查询没有直接哈希：在应用哈希函数之前，在这些查询中插入为此，左-右预言机将模式项而不是位串作为参数。模式术语定义如下。4.2.1模式模式术语是添加了新的原子常数的术语：模式变量。这些变量表示其值不为对手所知的挑战随机数。pat：：=pat，pat|BS|[一]由预言机进行的计算（求值）很容易递归地定义，只需将每个变量[i]替换为θ（i）表示的值。连接运算符仍然用·表示。v（bs，θ）= bsv（[i]，θ）= θ（i）v（p1，p2，θ）=v（p1，θ）·v（p2，θ）我们将模式pat的长度定义为v（pat，θ）的任何结果的长度，对于给定的θ。评价算法v接近于concr算法。然而，由于v的主要用途是对密钥执行操作，并且concr更一般，我们使用两种不同的算法。如果一个模式至少包含一个模式变量，则该模式是中空的定义4.4[HASH]134R. Janvier等人理论计算机科学电子笔记186（2007）121假设H是一个带密钥的哈希函数[6]。然后，由γH表示的与H相关联的HASH准则由（Θ;F;VUNF，VNC）给出，其中：(i) Θ随机生成长度为η的随机数Nh和散列密钥k。(ii) F允许访问三个预言机：• 一个散列预言机HN，它把一个以前从未给过该预言机的空心模式pat作为输入，并返回用NH完成的pat的k的散列;• 一个oracle存储器，它在存储器中保存由adversary发出的每个比特串;• 返回k的散列密钥oracle。(iii) VUNF验证一个位串bs是否已经由散列oracle产生，同时它已经在oracleStore之前给出。(iv) VNC将两个不同的模式作为输入，不一定是空心的，并验证它们是否具有相同的哈希值，并与NH一起完成。一个散列函数H被称为HASHiH是安全的。我们用HASH/UNF=（Θ;F;VUNF）表示与散列的不可伪造性相关的子标准，如果散列消息的某个部分是未知的，并且HASH/NC=（Θ;F;VNC）表示与冲突标准相关的子标准。我们注意到HASH/NC等价于准则Col，并且HASH隐含Pre。我们还注意到，在随机预言模型中，满足HASH的哈希函数是平凡的（哈希函数由随机预言机给出）。另一方面，在标准模型中，我们不知道满足HASH的实现。类似于IND-CCA，HASH可以被扩展到由N-HASH表示的等效准则，其中生成N个挑战随机数并由散列预言机使用命题4.5一个哈希函数是HASH，当且仅当它是N-HASH，对于任意给定的N >0。证据N-HASH隐含HASH的事实是显而易见的.为了证明相反的情况，让我们考虑一个对手A对抗N-HASH/UNF。我们建立一个对抗HASH/UNF的对手B。对手A必须产生一个新的哈希值，其中至少包含一个她的挑战随机数。对手B随机选择1到N之间的整数i。她通过生成N-1个随机数并将其分配给A的挑战随机数来模拟A，除了第i个挑战随机数，它与A的挑战随机数相关联。这样，每当A通过产生包含第i个挑战随机数的消息的新散列来赢得她的挑战时，B就赢得她的挑战因此AdvN − HASH/UNF（η）≤ N。AdvHASH/U NF（η）A BHASH/NC的N-HASH/NC的含义是类似的。QR. Janvier等人理论计算机科学电子笔记186（2007）121135我我一4.3密码库的安全性在这里，我们定义了嵌套密码原语的安全性。这是使用一个结合了前两个标准的标准完成的。也就是说，N个非对称密钥与散列密钥k一起生成，以及询问比特B。对手可以访问他在之前的标准中获得的预言（左右加密，非对称方案的公钥和解密，哈希函数的哈希和存储），并且可以通过推导b的值，通过找到具有相同哈希的两个不同模式或通过获得已经在商店中的哈希预言的位串来获胜。加密预言机现在在输入中接受相等长度的模式对（pat0，pat1），并输出用相应的NH完成的模式patb的加密。这些预言的模式由以下语法给出：pat：：=pat，pat|BS|[一]| {pat}bsencryption| h (pat)hashing评估算法v以直接的方式扩展以处理这些模式。设γN 为准则，包括上面详述的预言机和以下验证器：VIND ，其返回位b的真;VUNF，其返回真，如果散列预言机输出已经在存储中的位串;以及VNC，其返回真，如果给定具有相同散列的两个不同模式。定义4.6密码库（AE，H）被称为N-PAH，如果对于PPTM中的任何对手A，优势AdvγN（η）是可忽略的，并且PrR与碰撞是可以忽略的。这样的库在存在IND-CCA非对称加密方案和HASH散列函数的假设下存在。命题4.7如果密码库CL是IND-CCA和HASH，则它也N-PAH证据这个证明可以很容易地用[13]中提出的分割定理来完成。我们只提供一个证明草图。设A是N-PAH的对手.证明背后的直觉是，如果A能够战胜不可战胜性标准，那么我们可以建立一个对手B1来对抗N-IND-CCA，只要B赢得了她自己的挑战，她就赢得了她的挑战。如果A能够战胜非冲突挑战，则对手B2战胜N-HASH能够通过模拟A来战胜她的冲突挑战。其思想是，B2不必使用她的挑战随机数来模拟A，她可以生成新的随机数，因此她可以很容易地模拟加密预言机。如果A能够战胜不可伪造性标准，则我们针对N-PAH的不可伪造性构建对手B3，该对手B3使用她自己的散列预言机来模拟A这个想法是，A的任何一种行为都不受由A产生的“不正确”答案的影响136R. Janvier等人理论计算机科学电子笔记186（2007）121加密预言机，然后B3的优势是相同的，A的优势，或A的行为是不同的，在这种情况下，我们可以建立一个对手B4对N-IND-CCA，区分正常行为的A从她的行为时，她被B3模拟。因此，A的优势由B1、B2、B3和B4的优势之和所限定，这是可以忽略的。Q5符号语义学在本节中，我们证明了在所考虑的协议和密码原语的一些假设然后，我们利用这一点来展示一个保存结果，该结果表明，如果符号迹属性得到满足，那么它的计算具体化也得到满足。5.1关于协议的我们对协议的假设要么是语法的，要么是符号语义的自动可证明的。第一个假设是我们只考虑可执行的原型（见定义3.1）。其次，我们只考虑保密协议。也就是说，我们假设对于任何原子消息a∈atom（n），|= fSecret（a）或a∈IK（参见定义）3.6）。满足这些限制的协议称为良构协议。5.2计算痕迹与符号痕迹的为了陈述我们的定理，我们需要定义符号迹tf的具体化。由于我们处理的是非确定性的密码原语，因此通常存在一组tf的具体化。因此，给定符号迹tf，我们用Concr（tf，θ）表示通过应用concr（·，θJ）在tf的每个符号消息上，其中θJ是来自位串的映射与θ相容的符号信息。然后，我们可以陈述我们的主要定理如下。定理5.1设k =（R，IK）是一个使用Q-PAH安全密码库的良构协议，其中Q是k中密钥和随机数的个数之和. 假设A是一个对手。那么，以下概率作为η的函数是可忽略的：Pr[/tf∈Traces（λ）：Exec（A，IK，R，θ）∈Concr（tf，θ）]证据这个证明与[19，17，12]中的证明非常相似。 这个想法是建立一个对手对N-PAH的执行A通过模拟执行.对手B还构建了与所观察到的计算执行相对应的符号执行。只要A能够产生一个不符合有效符号执行的执行，那么B就能够战胜她的一个挑战。因此，A产生这种执行的概率受到B的优势的限制，这是可以忽略的假设。QR. Janvier等人理论计算机科学电子笔记186（2007）1211375.3符号和计算属性的回想一下，计算迹性质Pc由一组计算迹给出，符号迹性质Pf由一组符号迹给出。 我们说，Pf是一个忠实的抽象Pc的协议ESTA，如果一个具体化的符号迹在Pf是不是在Pc的概率可以忽略不计。换句话说，以下概率可以忽略不计：Pr[tf∈Traces（t）：tf∈Pf<$Exec（A，IK，R，θ）∈Concr（tf）<$Exec（A，IK，R，θ）/∈Pc].下面的命题是忠实迹性质的保持结果。它指出，如果符号属性是计算属性的忠实抽象，并且它在符号模型中得到满足，那么具体属性在计算模型中得到满足。它已被应用于相互认证[19]，其中也有关于符号/计算属性的更长的讨论。命题5.2设Pf和Pc分别是一个符号的、计算的、性质相同的命题. 假设TCP是一个使用Q-PAH安全库的格式良好的协议。 如果Pf是P c的一个忠实抽象，|=fPf，则|= cPc.换句话说，如果协议满足符号模型中的性质Pf，那么它满足计算模型中的Pc。证据 这个命题是定理5.1的一个推论。 我确已Pr[Exec（A，IK，R，θ）/∈Pc]=Pr[tf∈Traces（t）：tf∈Pf<$Exec（A，IK，R，θ）∈Concr（tf）]+Pr[tf∈Traces（t）：tf/∈Pf<$Exec（A，IK，R，θ）∈Concr（tf）]+Pr[/tf∈Traces（t）：Exec（A，I K，R，θ）∈ Con c r（tf）]= ν（η）+0+νJ（η）其中v和vJ可以忽略不计。Q类似的结果可以证明SecNonce [12]。定理5.3设k是一个使用Q-PAH安全库的良构协议，N是k中的随机数，A是攻击者。 如果|= fSecret（N）然后|= cSecNonce（N）。证据 这个证明与定理5.1非常相似。Q我们注意到，我们不能处理的计算秘密的nonce发送的哈希。这是因为我们没有假设我们的哈希标准，哈希函数确保不可扩展性。我们只假设一个散列不会泄漏足够的信息来获得整个散列消息。在[11]中给出了可以以散列发送的随机数的保密性的定义138R. Janvier等人理论计算机科学电子笔记186（2007）121结论本文的主要贡献如下：散列函数正确性标准的形式化定义（在随机预言模型中很容易满足）。证明Dolev-Yao模型的正确性的协议，可以结合一个非对称的计划和散列函数。我们的定理的证明使一些限制的协议，在实践中很容易满足。作为未来的工作，这将是有趣的调查是否Dolev-Yao的正确性可以证明在较弱的假设下的密码原语。此外，将这一结果推广到其他证券性质也很有意义引用[1] M.阿巴迪和P. Rogaway。讨论密码学的两种观点（形式加密的计算可靠性）。IFIP国际理论计算机科学会议（IFIP TCS 2000）