12理论计算机科学电子笔记173（2007）139-157www.elsevier.com/locate/entcs静态等价的逻辑刻画HansHüttel1和MichaelD.Pedersen2，b丹麦奥尔堡大学计算机科学系b苏格兰爱丁堡大学信息学院LFCS摘要Abadi和Fournet的工作引入了框架的概念来描述密码协议环境的知识。框架是项的列表;在静态等价的概念下，如果两个框架满足相同的项方程，则它们是不可区分的。我们提出了一个一阶逻辑的框架与量化的环境知识，在某些一般条件下，characterizes静态等价，是适合于建设的特征公式。该逻辑可用于推理环境知识，并可通过定义合适的签名和相关的方程理论来适应特定的应用。 该逻辑可以进一步扩展模态以产生模态逻辑，例如应用Pi演算。关键词：框架，静态等价，逻辑，密码协议，应用PI1介绍安全协议的设计和分析的形式化方法通常依赖于环境知识的概念。继Abadi和Fournet之后，[3]，框架是具有名称限制的替换，表示通信协议中任何给定状态下主体通信的消息例如，考虑框架Δ1=Δ（vk）{enc（b，k+）/x，k−/x}其表示在协议状态下的环境知识，其中两个消息已经在某个开放信道上发送：1电子邮件：hans@cs.aau.dk2电子邮件：m.d. sms.ed.ac.uk。这项工作得到了微软研究院通过欧洲博士奖学金计划提供的部分支持。1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.02.032140H. Hüttel，医学博士Pedersen/Electronic Notes in Theoretical Computer Science 173（2007）11密钥k+和相应的私钥k-。种子k应该是秘密的这一直觉可以通过对k的限制（νk）得到。单个术语可以通过其各自的变量引用，这提供了一种对术语进行排序的方法。任意项可以从框架中的名称和变量构建，项之间的相等性由适当的等式理论=E在每个应用程序的基础上定义。在依赖于公共密钥加密的帧E11中，因此可以预期例如dec（x1，x2）=Eb。两个框架是静态等价的，如果它们不能通过测试由框架中的变量和自由名称构建的任意项之间的相等性来区分。以两个额外的帧为例，其中h是单向散列函数：J=Δ（νk）{enc（b，h（k）+）/x，h（k）−/x}<$JJ=Δ（vk）{enc（h（b），k+）/x，k−/x}11 211 2这两个帧仅在应用于键的散列函数中与第一帧不同和明文B。然后我们有了这个α1和αJ被静态等价，因为相同的等式在两个帧中成立;特别地，等式dec（x1，x2）=Eb成立。另一方面，这个等式在DJJJ中不成立，所以JJ既不静态等价于1 1除了作为知识的自包含表示之外，框架和静态等价在过程演算（如应用π演算）中起着核心作用[3]和Spi演算[4，6]，因为过程上的观测等价是使用标准互模拟条件和过程产生的框架上的静态等价条件然而，静态等价的标准定义在对术语进行泛量化的情况下确实是多余的，这引起了可判定性问题，并使逻辑表征复杂化。事实上，它已被证明，静态等价是不可判定的一些方程理论，但一类理论的静态等价是可判定的也是已知的[1，2，7]。本文的主要贡献是一个框架的一阶逻辑，它刻画了静态等价，并在一定的一般条件下，即当方程理论是一个独立的收敛子项理论，并允许项约简是可观测的时，给出了特征公式。该逻辑包括用于测试等式（在等式理论中）、约简和项之间的语法等式的原子命题。量化涵盖了框架的综合，直观地说，框架是环境知识的直接表示。因此，该逻辑可以用于推理环境知识，并且可以通过定义合适的函数签名和方程理论来适应特定的应用。用模态扩展逻辑[9]产生了Appliedπ的模态逻辑，它表征了过程上的观测等价性，并允许随着时间的推移对环境知识进行推理。模态逻辑也可以适用于特定的应用;例如，用私钥密码学定义一个方程理论会产生类似于Spi逻辑的逻辑[8]。为了得到逻辑刻画结果，我们首先给出了静态等价的一个精确定义，它不依赖于任意项上的泛量化结果表明，在上述一般条件下，细化定义与标准定义一致。我们的方法受到启发，H. Hüttel，医学博士Pedersen/Electronic Notes in Theoretical Computer Science 173（2007）141在[6]中引入的Spi演算的核心概念。本文件的结构如下。在第2节中，我们介绍了一些基本概念，并形式化了我们对方程理论的假设第3节发展了静态等价的一个精确定义，它不依赖于任意项的泛量化在第4节中，我们介绍了框架的逻辑，在第5节中，我们简要地展示了如何将其扩展到应用π的模态逻辑。第6节结束2基本定义2.1方面一个签名由一组有限的函数符号组成，每个符号与一个整数元相关联。设k为函数符号，N为名称的集合，范围为a，b，c，.。，k，设X是变量的集合，范围为x，y，z，设U = N <$X。然后，项T（U，U）的集合归纳地定义如下：• UT（，U）.• 对于所有k ≥ 0：f（M1，. ，Mk）∈T（n，U），如果f ∈ n（k）且M1，. ，Mk∈ T（n，U）出现在一个项M∈T（M，U）中的名称和变量的集合将分别用n（M）和v（M）表示，我们将使用缩写n（M1，M2）来定义n（M1）<$n（M2）。 C[x]是一个等式，其中r e v（C[x]）=xn（C[x]）=x。通常我们会对识别项M∈T（n，U）的某些位置处的子串感兴趣。为此目的，M的结构可以通过将其表示为解析树来说明，其中节点被标记为函数U的元素，被标记为U的节点是叶子，并且被标记为函数符号f的节点的子节点是f的参数。 一个位置则是一个有限序列w=w1，.，w nwherewi∈N。位置w标识通过从根，并且对于在级别i处的每个节点，在编号为Wi的边之后。其解析树以w为根的M的子项记为M|w（位置和子项的正式定义见[11]）。2.2等式理论在[1]之后，我们基于项重写系统来定义项之间的相等。重写规则r的形式为L > rR，其中L，R∈T（X，X）且v（R）<$v（L）。如果M1 = Lθ，M2= Rθ，则M1利用规则L > rR递归地约化为M2，记为M1> rM2。 项重写系统R则是重写规则的集合，并且我们感兴趣的是由重写系统导出的重写关系 > 。定 义M1>M2 当 且 仅 当 存 在 规 则 L>rR 使 得M1|w=LθandandM2=M1{Rθ/M1|w}对于某些子节点θ和节点w。方程理论= E现在由归约关系>的自反、对称和传递闭包给出。我们将使用加密和配对的应用程序视为一个运行示例。142H. Hüttel，医学博士Pedersen/Electronic Notes in Theoretical Computer Science 173（2007）= Σ2示例2.1对于具有对称密钥加密和配对的应用，可以采用以下不言自明的签名符号：Σsym =Δ{enc（·，·），dec（·，·），[·，·]，fst（·），snd（·）}等式理论ES是由以下规则生成的，这些规则指定了解密和投影如何工作：dec（enc（z1，z2），z2）>r1z1fst（[z1，z2]）>r2z1snd（[z1，z2]）>r3z2并且示例等式fst（dec（enc（[a，b]，k），k））=ESa则成立。示例2.2为了对公钥加密进行建模，我们简单地添加公钥/私钥生成器函数到来自示例2.1的签名，即pubΔ{·+，·−}。方程理论EP由以下规则产生：dec（enc（z1，z2+），z−）>rz1fst（[z1，z2]）>r2z1snd（[z1，z2]）>r3z2并且示例等式fst（dec（enc（[a，b]，k+），k-））=EPa成立。2.3框架和静态等效如在引言中所解释的，环境知识由form=（v nnn n）σ的矩阵隐式地表示，其中rnn n是p r i v a t e n a m的（possiyempty）列表，并且σ是form{M1/x1， . . ，Mk/xk}。 事实上，一个frameme只是一个对名称有可能限制的替换。考虑到这一点，以预期的方式应用于项，我们将M中出现的每个变量xi替换为Mi。我们假设替换是无环的，并且所有出现的项都是标准形式（即在相关项重写系统中不可约）。我们分别用dom（n）和im（n）表示n中置换的定义域和像。框架的自由名和绑定名分别用fn（n）和bn（n）表示，并按预期定义。静态等价基于帧中的项之间的相等性来表达帧的不可分割性定义2.3两项M1和M2在标架中相等，记为（M1=EM2）<$i <$n（M1，M2）<$bn（n）=n且M1<$=EM2<$.定义2.4两个标架和J在E中静态等价，记为EJ，idom（）=dom（J），（M1=EM2）所有项M1和M2的折扣（M1=EM2）j2.4约简可观测理论为了给静态等价下一个与标准定义相一致的精确定义，并随后给出一个逻辑特征，我们需要对所考虑的理论施加一些假设。1H. Hüttel，医学博士Pedersen/Electronic Notes in Theoretical Computer Science 173（2007）14322222第一个假设是可观察到的减少理论，定义如下：定义2.5由重写系统生成的T（n，U）上的方程理论ER是可观察到的减少，如果(i) 有一个常数函数符号ok ∈<$(ii) 对于每一个d∈，都有一个测试函数符号test d ∈。(iii) 对于rvery（d（C[zz]）>rR）∈R，re是一个可检验的规则（testd（C[z]，ok）>rJok）∈R.注意，任何理论E都可以用适当的测试函数和重写规则进行扩展，使其成为约简可观察的，我们一般用E+表示这种扩展。减少可观察理论基本上允许帧被区分的基础上减少除了平等。我们认为，这往往是一个合理的假设。考虑以下两个框架：Δenc（b，k+）xk−xJΔenc（b，k+）xc−x2 =（v k，b，c）{/1，/2}2=（v k，b，c）{/1，/2}第一帧包含加密名称和可用于解密的相应私钥第二帧包含相同的加密名称，但不包含用于解密的相应私钥。现在事实证明，2012年，PJ。唯一相关的尝试是dec（x1，x2）=EPb和x1=EPenc（dec（x1，x2），k+），但这些在任何一个框架中都不成立，因为b和k在bn（n2）和bn（nJ）中事实上，2012年，可能会让人有点惊讶因为我们得到了从输出加密项和相应的解密密钥的过程产生的知识在语义上等同于输出相同的加密项和不相关的解密密钥的过程！对另一方面，P =2/P =E+P=J因为等式测试dec（x1，x2）> ok在x2中成立，但不是在阿斯塔纳。这样做是否明智？加密函数的实现（例如，OpenSSL库[12]）通常不提供测试用给定解密密钥解密是否成功的手段。然而，在许多应用中，假设该信息是可用的，例如通过在加密之前将公知的令牌附加到明文;然后可以检查解密输出是否也包含该令牌。第二个假设是收敛子项理论，即由收敛重写系统R={Li>riRi}i∈I生成的理论，其中Ri是Li的子项，对于每个i∈I。静态等价已被证明是可判定的这类理论[1]。对于第三个也是最后一个假设，我们引入了析构函数上下文的概念：定义2. 6一个C_nt_x_tD[x，x_t]是一个D_nt_x_t_t_t_x（由下划线标识），如果它与某个重写规则L>r_R的左手边是统一的，则它是一个D_nt_x_t_t_x_t_t_x（由下划线标识）。144H. Hüttel，医学博士Pedersen/Electronic Notes in Theoretical Computer Science 173（2007）并且x在D[x，x∈ L]中的位置是R在L中的位置的近似。例如，snd（x）是一个析构函数上下文，而snd（[x，y]）不是;这反映了析构函数snd我们现在可以陈述第三个也是最后一个假设，即重写规则是独立的，因为它们不包含析构函数上下文作为适当的子项;即我们忽略重写规则，例如dec（enc（fst（[z1，z2]），z3）> z1这直观地表明，只有对的加密的第一分量才能被解密。然而，这个假设并不是很强，因为绝大多数具有上述形式规则的注意，如果E是独立收敛子项理论，则E+也是独立收敛子项理论。3细化静态等效在这一节中，我们给出了静态等价的一个精确定义，它不依赖于任意项上的泛量化。我们从定义帧的分析开始，直观地说，这是将帧转化为比特所产生的项的集合，例如，通过迭代解密或投影帧中的项。分析通常可能很大;因此我们也将框架的核心定义为足以“再现”分析的最小分析子集。静态等价的精确定义对核心上的上下文施加了条件：两个框架中的相应项必须在核心上相等，并且核心上的相同约简和句法等式必须在两个框架中保持。 为了限制所考虑的上下文的数量，我们进一步定义了划分上下文的概念。3.1分析对于任何方程理论，我们假设一个相关的启示关系，>S，其中M1>SM2，如果M1可以揭示基于项集合S的子项M2.定 义 3.1 设 S 是 一 组 项 。 定 义 M>SM|w 当 且 仅 当 存 在 r_c_t_D[x ， x_t] 和t_m_s_T_S_s_t_s_t_s_t_t_D[M，T_m]>r_M|W.例如，我们有enc（a，k+）>Sa，如果k∈S或k−∈S。 分析A（M，S）则是基于S中的项的M的迭代揭示;这是[10]中给出的密码协议分析的推广。重要的是，分析项可以按其父项中的位置排序，因此我们将分析A（M，S）定义为一组对（M|w，w）其中M|W是从M中揭示的术语。定义3.2设S是一个项集，M∈S。 然后对MH. Hüttel，医学博士Pedersen/Electronic Notes in Theoretical Computer Science 173（2007）145ΔT∈SΔΔ==关于S，归纳地定义如下：A0（男，女）= {（M，N）}Ai+1Δi（M，S）= A（M，S）{（M |w，w）|中文（简体）|WJ，WJ）∈ Ai（M，S）s.t. M|wJ>SAi（T，S）M |w}我们进一步定义AM∈SA（M，S）.（男，女）ΔA（M，im（）<$fn（）），对于帧和A(S)Δ当位置不重要时，它们将在下面被省略，在这种情况下，分析被简单地认为是一个多项集。3.2核心和核心作为一组已知的术语，分析通常包含冗余。出于复杂性的原因，我们只希望考虑分析的最小子集，通过应用适当的上下文，可以从该最小子集重构分析实现这一目标的第一步是对核心进行以下定义。定义3.3设M是一项，S是一组项。然后核心（M，S）={（M|w，w）|（M）|w，w）∈A（M，S）<$M|w/>A（S）}定义核心（M，N）=cores（M，im（m）<$fn（m）），cores（x，n）Δ=cores（x，），for=（νn）{Mi/xi}i∈I，岩心Δ=i∈I{（M i|w，w，i）|（M i|w，w）∈cores（M i，n）}<${（n，，）|n∈ fn（n）}请注意，我们已经定义了框架的核心，以包括框架中的所有自由名称（占位符只是表示自由名称没有索引和位置），因为这些是环境知识的重要组成部分。与分析一样，我们经常忽略位置信息，并将核心视为多项集，而不是成对或三元组。我们对核的定义是对[6]中给出的定义的概括，其中核是一个单独的术语，仅针对对称密钥加密定义。 相比之下，我们的定义适用于任何收敛的子项重写系统，导致核心是集合。然而，上述对核心的定义有时不足以捕捉这样一种想法，即可以通过将适当的上下文应用于核心来重建分析。举个简单的例子：146H. Hüttel，医学博士Pedersen/Electronic Notes in Theoretical Computer Science 173（2007）Δ12ϕ=（v k）{enc（[a，b]，k+）/x，k−/x}则cores（x1，n）={a，b}，但k+不是core。完全忽略k+会导致信息的丢失：M1=enc（[a，b]，k+）（因此对k的分析）不能H. Hüttel，医学博士Pedersen/Electronic Notes in Theoretical Computer Science 173（2007）147通过将上下文应用于核心来重建，并且等式dec（M1，k−）=E[a，b] holds丢失。 这促使我们这样定义扩展核心：定义3.4术语M|w∈ A（M，S）是关于集合S的扩展核或ecore，如果(i) （M）|w，w）∈cores（M，S）.(ii) 这是一个不连续的字符C[xx]和不连续的字符串A（S），因为M|w=C[M]。M关于S的扩展核的集合用ecores（M，S）表示，我们定义了ecores（M，S）、ecores（x，S）和ecores（S）作为核。同样，我们经常忽略ecores中的位置信息。Ex示例3.5Takefram e=Δ（νa，b，k， k）{[enc（a，k1+），enc（b，k2+）]/，k−}在理论EP。然后1 2 x11/x2cores（x1，n）= {a，enc（b，k2+）}ecores（x1，k 2）={enc（a，k1+），enc（b，k2+），a}注意im（m）中的每一项现在都可以写成ecores上的上下文，并且可以通过应用适当的函数符号来从ecores重构分析！为了比较不同框架中具有相同索引的核，我们对核施加线性排序，并将核的有序序列写成核（N）=（N）i∈J排序是基于帧中的位置和索引，但细节是无关紧要的，已被省略;它们可以在[11]中找到。3.3分区上下文为了限制静态等价的定义的复杂性，并随后给出有限特征公式的构造，我们只考虑一类有限的划分上下文是至关重要的。为此，我们首先需要定义上下文中变量的相关关系直觉上，如果y 1和y 2分别独立于C [ y 1]的整数倍，则y 1y2在一个整数倍C[y 2]中;在整数倍C（enc（y1，y2+），y3）中，y 2和y3是相关的，而y1与y2和y3既不相关。换句话说，加密密钥是相互依赖的，但它们独立于明文。以下是一般定义：定义3. 6LetL[z]>R[z]是一个新的规则，而LetC[y]是一个常数，其中与hL[z]一致。在C[Y]和Letwj和wJ中，是I j最长前缀wi，分别为w j，使得位置wJ，分别为wJ，I j存在于L[z]中。我们可以把两个wi和wj分成两部分，w i rR[z]（并且与R相似），则C [ y] Q。有了这些概念，我们现在就准备好陈述静态等价的精确定义了。定义3. 9Let=（νn）{Mi/x}anddJ=（νn）{MJ/x}两帧ii∈Iiii∈I其中，ecores（n）=（N）j∈J，ecores（nJ）=（NJ）j∈J。然后，静态地细化如果满足以下每一个条件，则等价，写作j j：(i) 对于一个chi∈I，它是一个简单的常数xtC[yj]，满足Mi=C[Nj]和MJ=C[NJ]。(ii) 对于一个连续的xtC[y]和对于所有的j∈JitholdsthatC[Nj]=Nj惠C[NJ]=NJH. Hüttel，医学博士Pedersen/Electronic Notes in Theoretical Computer Science 173（2007）1492EEE我我E(iii) 对于任何类型的零件，如果C[y]和C[y]Qihold，C[y]that1 1 1C[N]>rC[N]惠C[NJ]>rC[NJ]1 2 1 2上下文和核心的定义方式使得条件1得到了很好的定义，通过归纳很容易看出，框架中的任何项确实可以写成核心上的上下文。条件2和条件3包含上下文上的泛量化，但这里的关键点是，只有有限多个等式和约简成立，因为划分上下文中的变量必须相关，并且只有有限多个核。一阶框架逻辑中的量化器的适当语义允许我们表达所有（无限多）不成立的等式和约简，这是导出特征公式的关键。3.5符合结果定义的精确度是为了让它与而事实证明，这确实是事实。由于篇幅限制，我们只陈述主要结果，读者可参考[11，第4章]以获得完整的证明。定理3.10证明依赖于以下引理：引理3.11设和J是两个框架，其中jJ，核（）=（N）j∈J，ecores（NJ）=（NJ）j∈J. 对于任意的C1[y]和C2[y]，（i）C1[N]=C2[N]惠C1[NJ]=C2[NJ]（ii）C1[N]>rC2[N]惠C1[NJ]>rC2[NJ]（iii）C1[N]=EC2[N]惠C1[NJ]=EC2[NJ]第一个结果是矛盾的。第二个结果依赖于分区-i g c ontexts：一个yc o n te xt C [ y n t]，其中该yc o n te x tC[y nt]与一个可重写的给定的LHS {Cn[yn t]}i ∈ I的子集是一致的（其中该yc o n te x t C [ y n t] } i ∈I被称为基因分区）。分级上下文），每个都在变量的等价类上（在相关性下）。我们使用C[ N]表示对于所有i∈ I，C[N]表示。第二个结果使用了前两个结果，并且对于收敛重写，系统，M1=EM2 iM1>EM3和M2>EM3对于某些和M3。定理3.10现在相当直接地从引理3.11向前推出，它给出了BEE的定义，以及每个不包含有界名称的项都可以写成核上的上下文。定理3.12该证明依赖于以下引理来建立核上的上下文和框架项上的上下文之间的关系：150H. Hüttel，医学博士Pedersen/Electronic Notes in Theoretical Computer Science 173（2007）我112233引理a3.13Let=（νn）{Mi/x}，J=（νnJ）{MJ/x}，其中h为你好然后ii∈Ii ii∈IEForachMi|w∈A（Mi，M j）anddMJ|w∈A（MJ，n，J）是一个连续的R[x，j]，可计算为n我我分析配方，并且a k∈N使得R[M]>kMi|w/>R[MJ]>kMJ|联系我们引理是通过构造来证明的，即给出了分析配方的归纳定义，并证明其具有所需的性质。这个论点依赖于理论是可观测的约化的假设，这就直接给出了一个项在静态等价框架中可以以完全相同的步骤约化。引理3.13可以用于定理3.12的证明，如果出现以下情况，则对C_J进行简化：如果出现以下情况，则A_j和C_j[N_j ]>rC_j[N_j]，E12对于某些情况，nC[R[M]]>lC[N]>rC[N]，以及所有C[R]拉 吉1 1 21[M]]>C1[N]。减少服务器数量可使C[NJ]mu i vt e red ecib ede 在C[y]中的一个sumpt是partitionig，C[y]或C[y]Q，并且重新编写的系统是1 1 1在这种情况下，使用最后一次重新评估方法是可行，即，C[NJ]>rC[NJ]asdesired. 第二部分是一个简单的例子。最后一个结果告诉我们什么时候可观测理论的简化假设是多余的：定理3.14若cores（n）= cores（n），则E= E + E+E。证明的一个方向当然是直接的。对于另一个方向，我们使用当ecores（）=cores（）时，任何不是core的分析项都可以写为ecores上的非平凡上下文（即不是变量的上下文）。这一点，连同推论，可以用来要了解这是如何工作的，请考虑对应于R12和R1j的密钥第2.4节：ϕ3Δenc（b，k）xkx JΔenc（b，k）xcx=（v k，b，c）{/1，/2}3=（νk，b，c）{{\fn黑体\fs19\bord1\shad1\1cHD8AFAF\4cHC08000\b0}我们又有了那个3/ES+J因为test dec（x1，x2）>ok在x13中成立，但在x2 3中不成立，在尼日利亚。 但突然间我们也有了那个“03/03/03”因为下面的等式3 3可以用来表示上述的减少在K3中成立，但在KJ中不成立：x1=Eenc（dec（x1，x2），x2）这个等式是可能的，因为enc（b，k）可以写为核心b和k上的非平凡上下H. Hüttel，医学博士Pedersen/Electronic Notes in Theoretical Computer Science 173（2007）151文，这通常意味着核心和核心一致。相比之下，这对于公钥版本中的enc（b，k+）项是不可能的，因为k+不是ecore。152H. Hüttel，医学博士Pedersen/Electronic Notes in Theoretical Computer Science 173（2007）（）={C[N]|N=e（n）andC[y]isacontext}4框架逻辑在本节中，我们将介绍框架的一阶逻辑LF，它刻画了静态等价并产生特征公式。4.1语法LF的语法定义如下，其中Mi在项上的范围和x在变量上的范围：A：：= M1= EM2|M1> M2|M1= M2|A1A2|€A1|（A1）|A1（A1）逻辑连接词的全部集合以通常的方式由<$、和定义4.2语义所有三个原子命题的共同点是要求被测试的术语不包含私有名称，因为公式不应该能够区分基于私有名称的框架因此，命题逻辑的满足关系定义如下：如果n（M1，M2）bn（）=，则M1 = EM2;如果n（M1，M2）bn（）=，则M1=EM2;如果n（M1，M2）bn（）=，则M1> M2;如果n（M1，M2）bn（）=，则M1> M2;如果n（M1，M2）bn（）=，则M1 = M2;如果n（M1，M2）bn（）=，则M1=M2;ϕ►¬Aifϕ A量化应该允许对框架所表示的知识进行推理，我们正式定义为综合S（S）（Paulson在[10]中引入的相应综合概念的推广定义4.1SΔ满足的定义现在可以用存在量化公式的情况来完成<$$> x（A1）如果<${M/x}<$A1，对某项M∈S（A）观察量化变量的绑定是如何通过用额外的替换扩展框架以自然的方式表示的。在x∈dom（n）的情况下，我们假设x到某个xJ/∈dom（n）的alpha转换，因为否则量化可能会覆盖n中的现有项。例4.2考虑框架ϕ4Δenc（b，k+）x[c，k]xJΔenc（enc（b，k+），k+）x[c，k]x=（v k，b）{/1，/2}4=（νk，b）{/1，/2}H. Hüttel，医学博士Pedersen/Electronic Notes in Theoretical Computer Science 173（2007）1534EEECΔ=公式y1y2（dec（x1，y1）> y2y3y4（dec（y2，y3）> y4））则表示x1可以使用某个已知密钥解密，并且所得项不能进一步解密。此属性对2004有效，但对200j无效。4.3结果第一个主要结果是LF刻画了静态等价。定理4.3（LF刻画φJ）设ThLF（）Δ{A∈LF|{\fnSimHei\bord1\shad1\pos（200，288）}它然后认为， Thj惠ThLF（）= ThLF（J）。证明是通过公式结构的归纳法，存在量化的归纳法依赖于以下引理：引理4. 4（ExtensionLemma）Letn=（νnn n）{Mi/xi}i∈Iandd nJ=（νn）{MJ/x}是具有hj的矩阵的W，并且令ecores（N）=（N）和iii∈IEj∈Jecores（NJ）=（NJ）j∈J. 对于一个C[y]i，它不保持等于{C[N]/x}nJJ{C[N（其中s是任何具有s/∈ I的索引）。sEs第二个主要结果断言特征公式的存在。定理4.5（特征公式）对于任何框架，存在有限特征公式C，使得对于任何满足dom（）=dom（J）的框架J，它成立那是什么意思？本小节的其余部分致力于构造对于一个framemi=（νn）{Mi/xi}i∈I的多个C的特征。为了证明这种结构确实有效，我们提出了[11]。C的形式如下=0.00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000ecore−1（y1）154H. Hüttel，医学博士Pedersen/Electronic Notes in Theoretical Computer Science 173（2007）EE第二次-2a第二次-2b第二次-2c第二次-3a第二次-3b第二次-3c）每个ecore由一个存在量化变量yi表示，公式ecore−i（y i）表明y i实际上是一个ecore。条件1−3是然后编码在我们下面详细说明的其余合取词首先要注意的是，在条件3中，在ecores上有无限多的上下文。J，则不存在减少的情况。例如，要表达的是，到y1和y2不是相关的公钥/私钥对，特征公式应该断言，dec（enc（n，y1），y2）>，dec（enc（n，y1+），y2）>，dec（enc（n，h（y1）+），y2），...这将导致无限的连接。相反，我们只是选择第一个≈H. Hüttel，医学博士Pedersen/Electronic Notes in Theoretical Computer Science 173（2007）155E并使用存在量化来表达，<$z.dec（enc（，z），y2）>在y2不是任何其他合成项的私钥对应物的 在y2是不同于y1的其他合成项的私钥对应项的情况下，我们自动得到y2也不是y1的私钥对应项。这个论点的推广依赖于所讨论的上下文是分区的，因此z是2。上述选择的背景就是我们所说的最小化背景：第四章. 6一个最小的最小的常数xtC[y_n，z_n]是一个与txth有关的常数C[y，z]и. Eachy∈如果您选择的是一个简单的函数，z˜∗is旨在表示任意合成项。请注意，只有有限个最小化的上下文，这对于下面构造有限个特征公式至关重要。编码Ecore首先，我们这样编码启示：M>Δ你好z，z[]> T）T =D [y，z]，...，[z]1秒1秒1s是一个最小化的析构函数上下文当R j [M] > k j N j时，L et Rj[xj]是Nj的一个特例，且L et k j ∈N b e。然后，ecore谓词编码如下：ecore−j jΔ1k j1 2 3k−1j（y） =z.. . zj（R[x> z ···> y）[zkj（yj>zkj）f（z1，.，zs）∈ S（s）1，.，z s，i，j=f（z1，.，zs））]编码条件1E achMicannb e writtenasaconttextooververer e- le C i [ y n] b e n y s u c hcont t e x t.条件1inJ则用以下公式表示：第二个-1Δ=i∈Ixi=Ci[yi]156H. Hüttel，医学博士Pedersen/Electronic Notes in Theoretical Computer Science 173（2007）2={j|如果C [ N ] =N，则C[y]不连续}21编码条件2编码依赖于以下集合：S2A =Δ{（i，j）|Ni=Nj}S2a =Δ{（i，j）|N i/=N j}S2B =Δ{（C[y]，j）|C[N]=Nj}S2c Δj第二次-2aΔ=（i，j）∈S2aΔyi=yjYIYJ（i，j）∈S<$2a第二个b=（C[y≠j]）∈S2bC[y]=yjΔ第二次-2c=一号... z k（<$f（z1，...，z k）= y j）j∈ S2 c f（z1，.，zk）∈k编码条件3编码依赖于以下集合：S3aΔ1⊥˜⊥˜⊥˜={（C1[y]，C2[y]）|C[y]ispartioning<$C1[N]<$C1[N]>C2[N]}S¯Δ ⊥ ⊥⊥˜⊥˜⊥˜3a={（C1[y]，C2[y]）|C1[N]是一个连续的函数，它是C1[N]>C2[N]}S3bΔ1⊥˜⊥˜⊥˜={（C1[y]，C2[y]）|C[y]isparting<$C1[N]Q<$C1[N]>C2[N]}S3C=Δ{C=[y]，z=1 ， . . ，zs]|C[y，z，.. . ，z是一个最小值，111秒第一， .. . . ，Ts∈S（N）.C1[N∈ N，Ts，. . ，Ts]>}ψΔ⊥ ⊥ ⊥ ⊥第二代a =（C[y]，C[y]）∈S3aC1[y]>C2[y]（C[y]，C[y]）∈S<$3a<$C1[y]>C2[y]1 2ψΔ⊥ ⊥第二次-3b=（C[y]，C[y]）∈S3bC1[y]>C2[y]ψΔ∗ ∗⊥ ∗ ∗第三代c =C[y，z，.. . ，z<$]∈S3c1. . zs. ，zs]>z）11秒5应用π1H. Hüttel，医学博士Pedersen/Electronic Notes in Theoretical Computer Science 173（
我的内容管理
展开
