立方时间下的π演算：对称密码与通信协议

网址：http://www.elsevier.nl/locate/entcs/volume62.html17页立方时间弗莱明·尼尔森1汉娜·里斯·尼尔森2信息学和数学建模，Richard Petersens Plads bldg.321，丹麦技术大学，DK-2800Kongens Lyngby，丹麦。Helmut Seidl3FBIV-Informatik，Universi t a üt T r ier，D-54286 T r ier，Germany.摘要π演算是多元π演算的一个变体，它允许对称密码学，并允许以精确但仍然抽象的方式表达通信协议。本文表明，上下文无关的控制流分析可以在立方时间内计算，尽管事实上，spi演算在一个无限的值域上运行。我们的方法是基于HornClauses with Sharing，我们开发了从无限到有限的转换，并处理输入和输出的多元性质。 我们证明了这个表面用于获得立方时间实现，而无需牺牲精度，也无需对密钥的性质进行简化假设1介绍多元π-演算[9]已被广泛用于描述通信协议。spi-calculus [1，2]是一种扩展，用于描述和分析基于对称密码的通信协议。更具体地说，spi-calculus（见第2节）包含一个显式的加密操作（将明文转换为密文），而解密（将密文转换为明文）则通过匹配操作进行更隐式的处理。这意味着语法强制区分明文和明文，因为解密只有在应用于密文时才成功，这与实现对称加密的低级原语的情况不同。1电子邮件：nielson@imm.dtu.dk。这项工作得到了丹麦自然科学研究委员会的部分支持。2 电子邮件地址：riis@imm.dtu.dk3电子邮件地址：seidl@uni-trier.de·c2002年由ElsevierScienceB出版。 诉 操作访问根据C CB Y-NC-N D许可证进行。2通过：spi演算认为加密和解密是完美的。一方面，当密钥K用于解密时，解密用密钥K加密的消息M总是成功的，并且给出正确的消息M。另一方面，当尝试使用不同于K的密钥K·时，解密不会成功;特别地，它不会错误地“成功”。尽管我给了你一个 明确 的信 息。本文考虑了文献[4，6]中提出它（在第2节中）被指定为流逻辑[10]，并在值的无限空间上操作。这使得它更难实现的分析比π演算的情况下，它是仿照[5]。事实上，这是不是一个先验清楚的分析可以实现没有损失的精度和立方时间。作为第一步，我们（在第3节中）展示了如何将分析从在无限宇宙上操作转变为在有限宇宙上操作。我们明确地执行这一步骤，因为我们发现一般逻辑公式，特别是我们证明（在命题3.1中），这种变换不仅是正确的，而且也不缺乏精确性。作为第二步，我们展示（在第4节）如何通过使用固定元关系编码多元关系来处理输入和输出的多元性质。我们再一次证明（在命题4.1中），这种变换不仅是正确的，而且也不缺乏精确性。最后的分析已经转化为Horn子句与共享（见第5节），并使用我们的简洁求解器实现。其运行时的理论评估表明，它在立方时间（见命题5.2）和经验测量表明，它在实践中表现得很好2Spi演算spi演算简介。多元π演算[1，2]扩展了π演算的加密和解密原语，这有助于以一种相当直接的方式表达密码协议。给出了表达式（E ∈ E）、项（M，N ∈ M）和过程（P，Q ∈ P）的语法4.讨论这一假设是否适用，超出了本文件的范围。是现实的，以及概率推理是否可以用于相同的效果。 作为因此，除非密钥是已知的，否则即使通过暴力攻击也不能解密加密的消息。3···我的天···我的天∈L∈ B∈ CB →⊆♩1KE：：=MlM，N：：= n|X|（E1，E2）|0|中文（简体）|{E1，···，E k}EP，Q：：= 0|EE1，···，E k.P|E（x β1，···，x βk）.P|P1|P2|（νn χ）P|[E1是E2] P|！P|设（x βx，y βy）= E在P中|ββ1βk0的情况E：P（x）：Q| P中{x1，···，xk}EJ的情形Eπ演算用数和对来扩展π演算，并区分名称和变量;项{E1，···，Ek}E表示在对称密钥E下加密 E1，···， Ek 所获得的密文。如果E是（V1，V2），则过程（忽略上标注释）let（x，y）= E在P中表现为P [V1/x，V2/y];如果E是0，则过程E为0：P <$（x）：Q表现为sP，如果E是<$（V），则过程Q为sQ[V/x]i;如果E是0，则过程E为0：P <$（x）：Q表现为sP。x1，，xkEJ尝试用key Ej对E进行解密：如果E对于mV1具有e，，VkV和若E·的值为V，则概率为P[V1/x1，Vk/xk];其他-明智的是，上述所有进程都被卡住（即无法执行），完美密码学的假设我们参考[1，2，4，6]以获得spi演算的形式语义。控制流分析。控制流程分析的公式化是通过注释流程的相关对象来实现的。这是通过as-signing为了指示程序点，通过分配“变量类型”（范围为y β，β·）对输入动作的可变性的绑定事件的发生;并通过分配“通道类型）到绑定在限制范围内出现的名称这些注释不会更改α转换。进程P是相对于类型环境me（将名称和变量映射到它们的通道和变量类型）进行分析的。到状态分析结果的功能性，我们使用集合的幂集函数（V al）抽象值的无限集合V al，其范围为w，v，归纳地定义为：.V al=C { 0}{0}×V al- 是的{pair}×V al ×V al- 是的Σ{enc} ×Val+预期分析估计值为三重（R，K，C），其中：• R：R（V al）是一个抽象环境，它将变量类型映射到它们可以绑定的抽象值集合。[5]我们使用标签l来指代术语Ml;其他作者更喜欢省去标签，而是使用如下符号： M指的是术语M;选择在很大程度上是一个问题， 的偏好。4∧我i=1β1βki=1（R、K、C）|= men li <${me（n）}<$C（l）（R、K、C） |= me x liff R (me (x)) ⊆C (l)（）= （ll）l（R、K、C）|=meM l1（R，K，C）|=meM l2R、K、C| me M1，M2i1212PAIR（C（l1），C（l2））C（l）（R、K、C）|= me0 li{0} C（l）（R、K、C）|= me（M l0）l i（R，K，C）|= meM l0 SUC（C（l0））C（l）ki=1 （R、K、C）|=meM li（R、K、C）|={Ml1，···，M lk}li（R，K，C）|=N leme1kNle我ENC{C（ll），·· ·， C（lk）}C（le）C（l）（R、K、C）|= me0i true（R、K、C）|= meM l（）=卢卢克1K（R、K、C）|=meN liR、K、C|me Ml⟨N 1 , ··· ,N k ⟩.P iffi=1iC（l）/= N（R，K，C）|= meP<$x ∈ C（l）：C（l1）× ··· × C（lk）<$K（x）（R，K，C）|=meM l（R、K、C）|= me M l (x β1 , ··· , xβk ).P iff1KC（l）/=N（R，K，C）|=me[x<$$>→β<$]P<$nx∈C（l）：n（w1，·· ·，wk'）∈K（x）：k=k′k {wi}R（βi）（R、K、C）|= meP1|P2i（R，K，C）|= meP1（R，K，C）|= meP2（R、K、C）|=me（vnx）Pi（R，K，C）|=me[n <$→χ]P（R、K、C）|我！Pi（R，K，C）|=我P（）=[l（R，K，C）|=meM l1（R，K，C）|=meM l2R、K、C| me M1是M2Pi1212C（l1）<$C（l2）/=<$C（R，K，C） |= meP（R、K、C）|= meM l（）下一页|let（xβx，yβy）=M lC（l）/=Ml C（R，K，C）|=me[x<$→β，y<$→β]PR、K、C=me P中我是n∈r（w1，w2）∈C（l）：（R、K、C）|= me情况Ml，0：P（xβ）：Qi{w1}<$R（βx）<${w2}<$R（βy）（R、K、C）|= meM l0 ∈C（l）<$（R，K，C）|= meP（n（w）：n（w）∈C（l））n（R，K，C）|=me[x<$→β]Q<$r（w）∈C（l）：{w}<$R（β）（R、K、C）|= meM l（R，K，C）|= meN ld（R、K、C）|= me情况Ml，{x，···，x}l ii i（n∈ c{w1，·· ·，wk'}we∈C（l）：k=k′ <$w e∈ C（l d））<$（R，K，C）|=P1P中kNd设c{w1，·· ·，wk'}we∈C（1）：（k=k′kme[x→β]{wi}R（βi）5表1spi演算的流逻辑（改编自[4，6]）。6C →L →−−···H{||}• K：C（V alC）是抽象通道环境，它将通道类型映射到可以通过它们进行通信的抽象值元组集。• C：C（V al）是抽象缓存，它将标记项映射到该项可以评估的抽象值集合。估计值（R，K，C）的可接受性由以下判断定义：|= meP和（R，K，C）|=我M表达式和过程的分析在表1中给出，并使用以下简称：• （w）为（|};• pair（w1，w2）for（pair，w1，w2），andPAIR（W1，W2）for {pair（w1，w2）|w1∈ W1，w2∈ W2};• enc {w1，···，wk} w0 对于（enc，（w1，···，wk，w0）），以及对于{ enc{w1，···，W k } W 0，ENC{W1，···，W k}W0 |w0∈ W0，···，wk∈ Wk}.验证复合术语或流程的所有规则都要求验证组件（除非很明显它们不可访问）。表达式Ml的规则要求C（l）包含与M相关联的所有抽象值。此外，输出规则要求k的集合与每个组件关联的抽象值元组可以在与主题相关联的每个通道上传递对象的值。对称地，输入规则要求对于沿着主题传递的抽象值的每个k元组，对应的分量包括在x 1的值中，，xk. 最后三条规则要求对于每一个抽象值，则其子组件为包含在x1，···，xk中。上述分析改编自[4，6]，其中可以找到语义正确性的进一步解释和证明他们还确定，{（R，K，C）|（R、K、C）|= meP} 是摩尔家族这意味着它在最大下界下是封闭的;因此它的最小元素（R，K，C）（R，K，C）=meP本身满足可接受性判断。该分析最接近于[4]中的介绍，因为它避免了[6]中研究的无历史密码学的概念。由于我们不处理动态语义，我们已经免除了语义中使用的句法扩展7|003从无限到有限如何实现表1中的分析并不是立即的，因为它在无限大小的值集合上操作;因此，我们显式地修改规范以获得仅在有限宇宙上操作的表2。这里执行的开发背后的动机是观察到基于语法或基于树自动机的方法通过有限表示来描述有限值集，在模型检查[8]和集合约束[3]的情况下有效本质上，我们证明了表1可以被看作是定义了一个有限树文法，其非终结符形式为R（β）、K（κ）和C（l），尽管使用了集合的交集因此，我们不使用抽象值的集合V al，而是使用.DV al=C { 0}Σ{}×L.Σ{pair}×L×L.Σ{enc}× L+只记录术语的“顶层”结构的值的描述;然后R：B → B（DV al），K：C→ B（DV al）和C：L → B（DV al）。新分析的具体内容见表2|=·me P对于（R，K，C）=·me P到一个ve空间。我们还写了[[C]（l）对于三种语言，由非终端C（l）生成d，并且使k=k·是隐式的（通过考虑k等于k的可能性）。为了便于理解，我们稍后将R、K和C与表2相关地写为R、K和C（除非没有混淆的风险）。为了准备建立表1和表2中规格之间的关系，以及正式定义表2中使用的符号，我们定义了三个辅助操作。首先，定义函数G#[[χ]]={χ}G#[[0]]={0}G#[[G（10）]]=SUC（G（10））G#[[pair（11，12）]]=PAIR（G（11），G（12））G#[[enc{ll，·· ·，lk}l]]=ENC（{G（ll），·· ·，G（lk）}G（l））其次，G#：DVal→DVal（Val）到来自DVal的元素序列的逐点扩张被表示为G#：DVal→D Val（Val），并且dd被定义为：G#[[（w1，·· ·，wk）]]=G#[[w1]]×·· ·×G#[[wk]]第三，定义一个函数的逐点扩张H<$：（DV al）→（V al）H：DV al→Δ V（V al），如下所示：H†（W）=H（w）w∈W8K›→Kβ1βki=1L →L →1212Ne1212|=′men li <${me（n）}<$C（l）|=′mex l i<$R（me（x））<$C（l）|=′me M l1 |=′me M l2 <${ pair（l 1，l 2）}<$C（l）|=′me M l2 ∧ {pair(l1,l2)} ⊆ C(l)|=′me0li {0} C（l）|=′me（M l0）l i |=′me M l0 <${（l0）}<$C（l）=′l我1L勒日克K|=′M li |=′Nle|{M , ··· ,M}lii=1我我{enc{l1，···，lk}le}{C（l）}|=′me0i true=′l l1K|=′MLk|=′Nli [C]（l）/=100|=′P）|meM l N1，···，Nk.P imei=1我我<$x∈C（l）：C（l1） × ··· ×C（lk）<$K（x）=′l（β1β）|=′me M l∧([[[C]]](l)∅⇒|=′P）|me Mx1，···，xk .Pi我[x]β]<$χ∈C（l）：<$（w1，·· ·，wk）∈K（χ）：<$i=1{wi}R（βi）|=′meP1|P2I协议|=′meP1|=′meP2|=′me [ n <$→ χ ] P|=′me[n›→χ]P|=′me! Pi |= ′me P|=′meM l1|=′meM l2（[ C ]（l 1）[C ]（l 2）/=|=′meP）|=′meP)=′let（xβx，yβy）=M l|=me′ M l（[C]（l）/=|=me′[x<$→β，y<$→β]P）|我是你的|=′P中情况Ml，n对（l1，l2）∈C（l）：（C（l1）<$R（βx）<$C（l2）<$R（βy））|=′me M l<$（0 ∈ C（l）<$|=′me P）i <$（（<$$>（l）：<$（l）∈ C（l）<$[[C]（l）/=<$）<$|=′Q) ∧me0：P（xβ）：Q000me[x<$→β]R（l0）∈C（l）：C（l0）<$R（β）|=′meN ld|=′meNld∧|=′me情况Ml，{x，···，x}l ii i（（k{l1，···，lk}le∈C（l）：[C]（le）k[C]（l i）/=|=′P）1P中kNdi=1{l1，···，lk}le∈C（l）：（[C]（le）<$[C]（ld）=lme[x<$→β]）C（li）βR（βi）表2流逻辑在有限宇宙中的spi演算。给定一个函数C：（DV al），我们现在准备正式定义表2中使用的函数[[C]]：（V al），并在上面非正式指定它由以下等式归纳定义：1K9[C]=[C]#†C这相当于设置[[C]（l）=w∈C（l）[C]#（w）foralll∈L. In换句话说，[[C]]直观上是由树文法生成的语言10C →C× × →∈≤ ≤···C. 最后，我们定义一个具体化函数γ，γ（R，K，C）=（[C]]#<$R，[C]]#<$K，[C]]#<$C）=（[C]#<$R，[C]#<$K，[C]）并使用它来说明表1中的分析计算的最小解与表2中的最小解相同提案3.1.ΣγH{（R·，K·，C·）|（R·，K·，C·）|=·me P}=H{（R，K，C）|（R、K、C）|= meP}证据 证明见附录A。✷4摆脱多边形假设多元运算（即加密和解密以及输入和输出）的arity由某个常数限制，可以证明表2的公式可以在多项式时间内实现，通过使用第5节的技术将其转换为具有共享的线性Horn子句[12]。为了得到一个有保证的立方时间算法，我们首先仔细研究如何处理输入和输出的多adicity。对于他的位置，更换了一个缓冲通道，然后K·：（DVal）第3节的一个组件• K··：NN（DVal ）suchthatv其 中 v是k-元组在K ·（x）中的第i个余元。（如前所述，当不可能出现混淆时，我们有时会把K写成K··在形式上，抽象信道能量的两个概念之间的关系可以通过具体化函数γ来捕获，该函数由：γ·（R，K··，C）=（R，K·，C）其中K·（x）={（v1，·· ·，vk）|（x，i，k）}由于它的点态定义，它导出一个抽象函数α·，使得（α·，γ·）是一个伽罗瓦联络。当α·（γ·（R，K··，C））=（R，K··，C）时，我们可以形成三元组（R，K··，C）;这仅仅意味着K··（χ，i，k）对于1是不成立的我k不等于K（x，l，k），，K··（χ，k，k）是，并且K··（χ，i，k）是对于i>k的估计。要做到这一点，我们需要改变分析输入和输出的条款;结果是一个新的具体化|=··thatdiersfromm|=·asfollows11中文（简体）≤≤H{||}联系我们我H{||}1K我我我我（写作KforrK··）：|=··KMlN l1，·· ·， N lk.Pi |=··Ml|=··Nli [C]（l）/=100|=··P）（kC（li） ）i=1Ki=1<$χ∈C（l）：C（li） <$K（χ，i，k）|=··M l（xβ1，·· ·，xβk）.Pi |=·· M l（[C]（l）/=|=··P）me1kmeKme[x<$$> →β<$]i=1<$χ∈C（l）：K（χ，i，k） <$R（βi）现在可以说明这两种分析之间的正式关系提案4.1.Σγ·H{（R，K··，C）|（R，K··，C）|=·m·eP}=H{（R，K·，C）|（R，K·，C）|=·me P}证据证明分为四个部分。首先，这是一个关于P和M的简单的结构归纳，以证明：（R，K··，C）|=·m·eP惠（γ·（R，K··，C））|=·me P（R，K··，C）|=·m·eM惠（γ·（R，K··，C））|=·me M当ver（R，K··，C）是well-formed时。第二，我们建立了（R，K··，C）（R，K，C）=·m·eP是完全成形的。这是一个矛盾。Sosuppos set（R，K··，C）满足|=·m·ePisnotwell-formed.一种可能性是存在χ，k，i，k和j，k，使得K··（χ，i，k）=但K··（χ，j，k）=. 通过（R，K··，C）的选择，可以看出，约束K··（χ，j，k）是一个非空的力;通过对输出的形式是K（i=1C（li）/=C）Ki=1<$x∈C（l）：C（li）<$K··（x，i，k）.然而，很明显，同样K··（χ，i，k）必须是非空的，从而建立期望的矛盾。另一个可能性是，这里存在χ，k，i>k，使得K··（χ，i，k）=。因此，必须有一个约束力K··（χ，i，k）是不可能的;然而，对条款的检查表明这是不可能的。第三，为了证明γ·（H{（R，K··，C）|（R，K··，C）|=·m·eP}）|=·me Pasfollowwsbecause{（R，K··，C）|（R，K··，C）|由于（R，K··，i=112C）（R，K··，C）=·m·eP是一个M族，且由于“如果"和”只有在13U≥···第四，要证明γ·（α·（H{（R，K·，C）|（R，K·，C）|=·me P}））=H{（R，K·，C）|（R，K·，C）|=·me P}α·（H{（R，K·，C）|（R，K·，C）|=·me P}）|=·m·eP因为{（R，K·，C）|（R，K·，C）|α ·（H{（R，K ·，C））=·me P}是Mor族，|（R，K·，C）|=·me P}是一个很好的形式，因为“惠”是在上面建立的。✷命题4.1的直观内容是，表2中输出的5带共享的Horn Clauses with Sharing的评论在[12]中引入了具有共享的Horn子句集，作为在我们的简洁求解器中实现的无交替最小不动点逻辑的有用子集。带有共享的Horn子句可以被看作是通过更强大的前提条件和结论扩展Horn子句;它们由语法生成的非终结子子句pre：：=R（x1，···，x k）|前1页前2页|前1页前2页|*x：前子句 ：：=R（x1，···，x k）|1|第1条第2条|前置条款|x：子句其中R是k元关系符号，k1，x，x1，表示任意变量，1是常真子句.给定一个原子值和关系符号和自由变量的解释ρ和σ的宇宙，我们定义满足关系（ρ，σ）|= t（t一个先决条件或条款）如下：（ρ，σ）|= 1itrue（ρ，σ）|= R（x1，···，x k） i <$（σ x1，···，σ x k）∈ρR（ρ，σ）|= x：prei（ρ，σ {x <$→ a}）|= prefor a ∈ U（ρ，σ）|= x：ti（ρ，σ {x <$→ a}）|= tfor all a∈ U（ρ，σ）|= t1<$t2i <$（ρ，σ）|= t1和（ρ，σ）|= t2（ρ，σ）|= pre1<$pre2 i <$（ρ，σ）|= pre1 或（ρ，σ）|=前2（ρ，σ）|=前条款i（ρ，σ）|=子句whenever （ρ，σ）|=前我们把有共享的Horn子句中的自由变量看作是来自论域U的常数符14号。因此，给定常数的解释σ，15Lii=1我[[]]12121KNLE我i=1我 我1K1Ki=1我i=11212箱M的1K Le1K LeeD1Ki=1me[x→β]H[[nl]]me=C（me（n），l）H[[xl]]me= <$u：R（u，me（x））<$C（u，l）H[[（Ml1，Ml2）l]]me=H[[Ml1]]meH[[Ml2]]me=C（pair（l1，l2），l）H[[0l]]me=C（0，l）H[[M（10）1]]me= H[[M10]]me =C（M（10），1）H[[{Ml1，·· ·， M lk}l ]]=mkH[[M]][Nle]]C（enc（{l，···，l} （l）H[[0]]me=1H[[Ml]]mekH[[Nli]]me（NC（l）H[[P]]me）H[[M l<$Nl1，···，Nlk <$·P]]me =（（NkNC（l）v：（C（v）ui：C（ui，li）H[[Ml]]me[[x] →β]（NC（l）H[[P]]me[x]→β]）H [[M 1（xβ1，···，xβk）.P]]me = kv：（C（v）i=1<$ui：K（ui， v，i，k）<$R（ui，βi））H[[P1|P2]]me=H[[P1]]meH[[P2]]meH[[（νnχ）P]]me=H[[P]]me[n<$→χ]H [[！P]]me=H[[P]]meH[M11是M12]P]]me=H[[M11]]me= H[[M12]]me = H[[ M 11]] me= H [[ M 12]]me=（NCC（11，12）me= H[[P]]me）H[[Ml]]me[x <$→ β，y <$→ β]（NC（l）<$H[[P]]me[x<$→β，y<$→β]）设（xβx，yβy）=MlP中的HLme=X yn对（l1，l2）：（C（pair（l1，l2），l）n（u：C（u，l1）<$R（u，βx））<$（u：C（u，l2）<$R（u，βy）H[[Ml]]me（C（0，l） <$H[[P]]me）H[[0：P（xβ）：Q]]me=（（β-N（l0）：C（β-N（l0），l）β-NC（l0））β-H[[Q]]me[x<$→β]）∀suc(l0):C(suc(l0), l)⇒(∀u:C(u, l0)⇒R(u, β))H[[Ml]]meH[[Nld]]me情况Ml，（（{l，···，l}：C（enc{1，···，1}，1）H[[{xβ1，···，xβk}]]我=克NC（li））N[[P]]N）NP中{l1，...，lk}le：（C（enc（{l1，...，lk}le），l）|NCC（le，ld））ki=1 u：C（u，li）<$R（u，βi）表3spi演算的Horn子句⇒ ∧我LeNld16符号，在子句子句中，我们称关系符号R的解释ρ为所提供的解（ρ，σ）|=子句。带共享的Horn子句的转换 表3包含对应于表2的约束生成函数。使用一个额外的泛量化器将集合包含扩展为集合成员，并使用二元谓词写出形式为u∈R（v17CC联系我们l1，l2：（11，12：（C（0，11）l1，l2：（C（n（u1），l1）<$C（n（u2），l2）<$NCC（u1，u2））<$NCC（l1，l2）ll1，l2：（ll lr（u11，u12），pair（u21，u22）：C（pair（u11，u12），l1）<$C（pair（u21，u22），l2）<$NCC（u11，u21）<$NCC（u12，u22））<$NCC（l1，l2）l1，l2：（nc{u11，·· ·，u1k}u1，nc{u21，·· ·，u2k}u2：C（enc{u11，···，u1k}u1，l1）<$C（enc{u21，···，u2k}u2，l2）<$NCC（u11，u21）<$··<$NCC（u1k，u2k）<$NCC（u1，u2））<$NCC（l1，l2）表4 NCC的公理化。形式为R（u，v）。此外，我们现在明确了x等变量，这些变量只应该在中的通道上变化。(The假设谓词是预定义的;或者，它可以在引入新通道的限制子句中更新为了可读性，以及为了便于复杂性估计，我们保留了使用函数符号，如pair;这可以通过以下方式避免：（i）使用额外的三元关系Rpair，（ii）定义Rpair（l1，l2，pair（l1，l2））（iii）通过对所有的l1，l2，l对进行量化来提取C（·，l）中所有对的分量，使得C（l对，l）等于R对（l1，l2，l对）。最后，我们不得不使用允许的原语来编码测试[[C]（l）=和[C]（le）[C]（l d）=。因此，我们引入辅助谓词NC（l）和NCC（le，ld），并通过考虑DV al中五种不同的值形式中的每一种来归纳公理化它们;这种编码是全局的，不应该对每个句法成分重复。NCC的公理化可以在表4中找到;NC的公理化可以通过仅仅删除NCC的第二个参数中出现的变量来获得。提案5.1H {（R，K··，C）|（R，K··，C）|=·m·eP}=H {（R，K··，C）|（R，K··，C）全氢[[P]]me}证据 这似乎证明，（R，K··，C）|=·m·eP⇔（R，K··，C）fulfillsH[[P]]me（R，K··，C）⇔（R，K··，C）18|=·m·efulfillsH[[M]]me19HO{····}H{|H}通过P和M中的归纳;为此，我们使用[[C]（l）/=等价于NC（l）和[C]（le）|[C]（ld）|=||等于NCC（le，ld）。✷理论复杂性。复杂度估计是基于Horn Clauses with Sharing [12]。为此，我们认为分析不是在变量序列（如l1，···，lk，le）上广泛量化，而是仅在事件上量化对于Enc11，，lk·当它们在程序中发生时，因为这里有非线性地多个这样的候选。此外，我们需要修改表4中谓词NCC的公理化，以避免量化器嵌套到深度4。事实证明，[12]中提出的平铺概念对此很有用;更具体地说，表5的公理化是通过应用[12]中提出的平铺的第二种变体获得的。显然，它们的最小解定义了相同的谓词NCC。建议5.2（R，K··，C）（R，K··，C）完全填充[[P]]m可以立方时间计算。证据子句[[P]] me对于大小为n的过程具有size（n），量化器的嵌套深度至多为2。NC和NCC的全局公理化的大小为O（1），嵌套深度最多为3（如表5所示公理化时）。对于一个大小为O（n）的论域，根据[12]的命题2，所得到的约束可以在O（n3）的时间✷实证验证。使用我们的简洁解算器实现了稍微优化的分析版本[13]。为了解释主要的修改，请注意NCC的计算是不必要的昂贵，因为它计算整个关系，即使通常只需要一小部分。我们使用类似于Prolog的魔集转换的一般转换来处理这个问题：每当NCC（x，y）在一个precondition中需要时（在pre成功传递后可到达），我们将其替换为NCC！（x，y），我们在NCC之前添加子句。（x，y），我们修改的公理化NCC产生的公理化NCC！只计算NCC设置的值的结果？.我们已经在[1]中描述的宽口青蛙通信协议实证测量表明，良好的实际性能。事实上，一个由15个生产者和15个消费者组成的系统可以在大约一分钟内进行分析6结论我们已经证明了Horn子句的多功能性，用于在立方时间内实现上下文无关的控制流两个关键的转变使这一点得以实现：（一）一个20→l1，l2， u：C（u）<$C（u，l1）<$C（u，l2）<$NCC（l1，l2）C（0，l1）C（0，l2）NCC（l1，l2）l1，l2，suc（u1）：C（suc（u1），l1）<$NCC·（suc（u1），l2）<$NCC（l1，l2）l2，suc（u1），suc（u2）：C（suc（u2），l2）<$NCC（u1，u2）<$NCC·（suc（u1），l2）l1，l2，pair（u11，u12）：C（pairr（u11，u12），l1）NCC·（pairr（u11，u12），l2）NCC（l1，l2）l2，pair（u11，u12），pair（u21，u22）：C（pair（u21，u22），l2）<$NCC（u11，u21）<$NCC（u12，u22）NCC·（pairr（u11，u12），l2）{u11，·· ·，u1k}u1：C（enc{u11，...，u1k}u1，l1）<$NCC·（enc{u11，...，u1k}u1，l2）<$NCC（l1，l2）{u1 12，enc{u11，·· ·，u1k}u1，enc{u21，·· ·，u2k}u2：C（enc{u21，···，u2k}u2，l2）<$NCC（u11，u21）<$··<$NCC（u1k，u2k）<$NCC（u1，u2）NCC·（enc{u11，·· ·，u1k}u1，l2）表5NCC的平铺公理化明确的具体化函数连接无限宇宙的有限宇宙的树文法（从而适应治疗的集合约束，以更一般的逻辑公式在这里使用），和（ii）一个明确的伽罗瓦连接编码明显的这些变换也适用于在无限宇宙中运行的多元演算的其他分析。命题3.1.ΣγH{（R·，K·，C·）|（R·，K·，C·）|=·me P}=H{（R，K，C）|（R、K、C）|= meP}证据第1部分：““持有。为此，它表明表1中的分析近似于表2中的分析，这意味着的（R·，K·，C·）|=·me P（γ（R·，K·，C·））|=meP（R·，K·，C·）|=·me M（γ（R·，K·，C·））|=meM并且可以通过P和M中的结构归纳来证明。 (We注意，由于Val中的值在