基于标签的符号模型在概率加密中的应用

理论计算机科学电子笔记186（2007）49-65www.elsevier.com/locate/entcs在对概率加密1建模时，不需要显式随机性V'eroniqueCortierHeinrich？H？ordegenBogdanWarinschiLoria/CNRSUMR7503INRIALoraineprojetCassissUniversit′eHenri-Poincar′eINPLLorraine，France{cortier，hordegen，warinsch}@ loria.fr摘要安全分析中使用的最流行的抽象之一是使用抽象的符号术语来对通过网络发送的位串。然而，高度的抽象模糊了在这些模型中进行的证明对于实际执行的重要性。特别是，虽然好的加密函数是随机的，大多数现有的符号模型的安全性不明确捕获的随机化密文。另一方面，将符号模型与密码学模型相关联的最近结果要求其中密文的随机化被显式地捕获（通过使用附加的标签）的符号模型到符号密文）。由于几乎没有工具支持生成的基于标签的模型，似乎有必要将决策程序和现有工具的实现从简单的模型扩展到使用标签的模型。在本文中，我们提出了一个更实际的替代方案。我们表明，对于一个大类的安全属性（包括相当标准的配方的保密性和真实性），安全的协议相对于简单的模型意味着安全的模型，使用标签。结合[4]的计算可靠性结果，我们的定理使得在不使用标号的符号模型中获得的安全性结果能够转化为标准计算安全性。基于这些结果，我们最近实现了一个AVISPA模块，用于验证标准密码模型中的安全属性保留字：概率加密，安全模型，协议验证，保密性，认证。1引言计算系统数学模型的设计者需要在两个看似矛盾的要求之间找到适当的权衡。自动验证（以及可用性）通常需要高度的抽象，而预测准确性则需要高度的细节。从这个角度来看，使用符号模型进行安全分析是特别微妙的，因为似乎这种模型操作的固有的高抽象级别无法来捕捉与安全相关的所有方面。本文研究1部分由ACI Jeunes chercheurs和ARA SSIA FormaCrypt支持的工作1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.11.04450诉Cortier等人理论计算机科学电子笔记186（2007）49ek（B）ek（B）ek（B）一个特别的方面，即在密码系统的构造中使用随机化[5]。基于复杂性的计算模型的一个核心特征是能够明确地捕捉和推理随机性的使用。此外，随机性对于实现加密的任何有意义的安全概念是必不可少的相反，符号模型很少直接表示随机性。例如，在实体B的公钥下加密消息m的典型表示是项{m}ek（B）。请注意，符号表示并没有捕获对用于生成此密文的随机性的依赖性。虽然这种抽象在某些设置[11]中可能足够准确，但在其他一些设置中则不足够。考虑下面一些玩具协议中的流程A→B：{m}ek（B），{{m}ek（B）}ek（B）为了实现该流程，{m}ek（B）的每次出现都被映射到密文。但是，注意，图片说明没有说明两次出现的{m}ek（B）是相等的（以相同的随机性创建）或不同的（以不同的随机性创建）。在足够丰富的协议规范语言中，消除上述结构的歧义可以很容易地完成。例如，在具有显式赋值的语言中，协议的第一条消息的两个不同解释可以如下获得：x：={m}ek（B）; send（x，{x}ek（B））和send（{m}ek（B），{{m}ek（B）}ek（B））。在这里，{m}ek（B）的每个不同的出现被解释为具有不同的随机性。其他方法采用更直接的解决方案，并表示所使用的随机性对于加密显式[6，1，10，4]。 如果我们写{m}l对于M在具有随机性l的B的公钥下，对该序列的两种不同的解释是：发送（{m}l1L1ek（B）L2ek（B））并发送（{m}l1L2ek（B）L3ek（B）最近，一种采用标签来捕获密文（和签名）中使用的随机性的模型已被用于建立符号分析相对于计算模型的可靠性[4]。他们的结果是基于一个仿真引理：对于协议执行，每个计算轨迹都可以映射到一个有效的符号轨迹。然后使用该映射转换安全属性，从符号模型到计算机模拟。请注意，即使在没有明确重复密文的情况下，标签的使用也是必要的，以区分例如代理生成的加密消息与对手生成的加密消息。使可靠性结果与实践相关的下一步是使用符号模型的一些（半）自动化工具进行安全性证明。然而，据我们所知，没有一个流行的工具（ProVerif[3]，，{{m}}，{{m}}）诉Cortier等人理论计算机科学电子笔记186（2007）495111CASPER [8]，Athena [13]，AVISPA [2]），或在使用标签的模型中自动推理的能力这个问题至少有两种解决办法。一种可能性是增强作为现有工具基础的符号模型。不幸的是，这样的修改可能需要大量的工作，包括调整现有的决策程序，证明其正确性，以及验证和修改数千行代码。在本文中，我们提出并澄清了一个替代的解决方案，在[4]中隐含使用。我们的想法是保持现有的工具不变，使用它们的底层（未标记的）模型来证明安全属性，然后证明结果实际上对带有标记的模型是有意义的。本文的主要结果是证明，对于一个大类的安全属性，我们提出的方法确实是可行的。结果我们考虑[4]中定义的协议规范语言和执行模型。该语言适用于使用随机数、公钥加密和数字签名的协议，并使用标签来模拟这些原语使用的随机性。对于每个带有标签的协议栈，我们自然地将擦除所有标签后得到的协议栈关联起来，并将转换扩展到执行轨迹。对于每个轨迹树，我们关联一个轨迹树，通过擦除标签获得，我们将此映射扩展到轨迹集。本文的第一个贡献是证明了变换是合理的。更精确地说，我们证明了，如果tr是一个有效的迹的（获得Dolev-Yao操作），那么tr是一个有效的迹的。重要的是，这个结果依赖于这样一个事实，即我们所考虑的特定语言不允许密文之间的相等性测试。我们相信，对于大多数（如果不是全部）满足上述条件的协议规范语言，类似的结果也是成立的。用于指定协议（带标签和不带标签）的语言以及它们相关的执行模型之间的关系在第2节中。在第3节中，我们给出了两个逻辑，L1和L1，我们用来表达安全属性-分别用于有标签和无标签的协议。非正式地，L1的公式通过从L1的公式中移除标签而获得。这两种逻辑都很有表现力。例如，它可以用来表达保密性和真实性属性的标准公式。接下来，我们将关注两个模型之间的安全属性转换。首先，请注意，带标签和不带标签的模型之间的映射是不忠实的，因为它丢失了关于密文不等式的信息。为了形式化这种直觉，我们给出了一个协议和一个公式，使得协议满足φ（在没有标签的模型中对应于φ的公式），但是协议不满足φ。我们的例子表明，问题的根源在于φ可能包含密文之间的相等性测试，而这些测试可能不会被忠实地翻译。反例在第4节。本文的主要结果是一个可靠性定理。我们表明，对于一个大类的安全属性，它是可以进行的证明在模型中更准确地说，我们52诉Cortier等人理论计算机科学电子笔记186（2007）492122一标识符L1L2是L1的片段和L1，因此，定理成立。考虑L1中的任意协议和公式φ。设φ为公式，L2通过擦除出现在φ中的标记而获得。因此，法院认为：逻辑L1Π |= φ = φ |= φ和L2仍然有足够的表现力来包含秘密和授权，计算公式 定理及其证明在第4节。基于我们的结果，我们实现了一个AVISPA模块[2]，用于获得计算可靠的自动证明，并使用它来验证AVISPA库中的我们的实验结果在第5节中描述。2议定书在本节中，我们提供了带标签的协议的语法。本文改编自[4]。规范语言类似于Casrul [12];它允许各方使用公钥加密和数字签名交换由身份和随机生成的随机数构建的消息。不使用标签的协议是直接获得的。2.1语法考虑一个代数签名，它有以下几种类型。代理身份的排序ID，对分别包含用于签名、验证、加密和解密的密钥的SKey、VKey、EKey、DKey进行排序代数签名还包含随机数、标签、密文、签名和对的排序，分别用于随机数、标签、密文、 排序标签用于加密和签名，以区分相同明文的不同加密/签名。SortTerm是一个包含所有其他排序的超级排序，除了SKey和DKey。有九个操作：四个操作ek，dk，sk，vk是在排序ID上定义的，并返回与输入身份相关联的加密密钥，解密密钥，签名密钥和验证密钥。ag和adv这两个操作定义在自然数和返回标签上。正如引言中所解释的，标签用于区分由诚实代理或对手创建的相同明文的不同签名（和签名）。我们区分代理和对手的标签，因为它们不使用相同的随机性。我们考虑的其他操作是配对、公钥加密和签名。我们还考虑了排序变量的集合X=X.n<$X.a<$X.c<$X.s和Xl=X <$X.l。这里，X.n、X.a、X.c、X.s、X.l分别是排序随机数、代理、密文、签名和标签的变量的集合。变量X.a和X.n的集合如下。如果k∈N是代表协议参与者数量的某个固定常数w.l.o.g. 我们将代理变量的集合固定为X。a ={A1，A2，. ，Ak}，并通过生成随机数变量的一方来划分随机数变量的集合。形式：X.n=A∈X.aXn（A）且Xn（A）={Xj| j ∈ N}. 此分区避免以后指定，诉Cortier等人理论计算机科学电子笔记186（2007）4953ek（a）| [T]MM每个角色，哪些变量代表生成的随机数，哪些变量代表预期的随机数。由参与者发送的标记消息使用TlL * = X. 1|ag（i）|adv（i）T1：：= X|一|ek（a）|dk（a）|sk（a）|vk（a）|n（a，j，s）|{T l } L|{T l}LLlsk（a）其中i，j，s∈N，a∈ID。未标记的消息被类似地指定为代数T中的项，T：：= X|一|ek（a）|dk（a）|sk（a）|vk（a）|⟨ T , T ⟩ |{T } ek（a）|[T ] sk（a）|[T] sk(a)其中j，s∈N，a∈ID。从标记项到未标记项的映射·：Tl→T通过移除标签：{k}l={k}m，[k]l=[k] m，f（t1，. ，tn）= f（t1，. ，tn），否则。的映射函数扩展到预期的术语集。每个协议参与者的个人行为由描述消息接收/传输序列的角色定义。一个k方协议由k个这样的角色给出.定义2.1[标记的角色和协议]标记的协议参与者 的 角 色 集 合Roles l定义为Rolesl=（（{init}<$Tl）×（Tl<${stop}））<$。一个k方标记协议是一个映射：[k]→角色l，其中[k]表示{1，2，. ，k}。未标记的角色和协议的定义非常相似。映射函数从标记协议扩展到未标记协议。我们假设一个协议规范是这样的，即，使得f（j）=（（lj，rj），（lj，rj），. . ），1122第j个每个序列（（l1，r1），（l2，r2），. . ）∈Rolesl指定执行角色的一方要发送/接收的消息：在步骤i，该方希望接收消息并返回消息ri。我们希望强调，术语lj、rj是我我不是实际的消息，而是指定接收的消息和输出应该是这样的。例2.2Needham-Schroeder-Lowe协议[7]的具体描述如下：有两个角色分别对应于发送者和接收者的角色，分别是R1（1）和R2（2）A→B：{Na，A}ek（B）B→A：{Na，Nb，B}ek（A）54诉Cortier等人理论计算机科学电子笔记186（2007）49A→B：{Nb}ek（B）诉Cortier等人理论计算机科学电子笔记186（2007）4955的1的1，X一个2的1的1，X一个2• （SId，f，H）1l一个2−−−−−−−−−→一个2int（1）=（init，{X1中文（简体）ek（A2）），（{X11Lek（A1），{X1中文（简体）ek（A2）（2）=（{X1L1ek（A2），{X11中文（简体）ek（A1）），（{X1L2ek（A2），停止）显然，并非所有使用上述语法编写的协议都是有意义的。特别是，某些协议可能无法执行。这实际上与我们的结果无关（我们的定理也适用于不可执行的协议）。2.2执行模型我们只为标记协议定义执行模型。然后，未标记协议的执行模型的定义是简单的。如果A是排序代理的变量或常数，我们将其知识定义为kn（A）={dk（A），sk（A）}<$X.n（A），即 代理知道它的秘密解密和签名密钥以及它在执行期间生成的随机数。形式执行模型是一个状态转换系统。系统的全局状态由（SId，f，H）给出，其中H是表示在网络上发送的消息的T1的项的集合，并且f维护所有会话idSId的本地状态。 我们将会话ID表示为形式为（n，j，（a1，a2，. ，ak））∈（N × N × IDk），其中n ∈ N标识会话，a1，a2，. k是会话中涉及的各方的身份，j是在该会话中执行的角色的索引。在数学上，f是函数f：SId→（[X→Tl]× N× N），其中f（sid）=（σ，i，p）是会话sid的局部状态。函数σ是在角色n（i）中出现的变量的部分实例化，p∈N是程序的控制点。允许三种过渡。corrupt（a，.，a）、−→（SId，f，<$1≤j≤lkn（aj）<$H）. 这位设计师已经做好了准备通过输出一组身份来识别各方。作为回报，他收到了与身份相对应的密钥。它只在执行开始时发生一次。我们专注于静态腐败，因为[4]中使用显式标签的可靠性结果只考虑这种腐败。然而，在我们的正式背景下，我们的减少结果应该很容易扩展到自适应腐败的情况下（当代理在执行过程中的任何时候都被损坏），因为我们可以映射的痕迹与动态腐败的痕迹，所有腐败的代理都是这样的开始。• 对手可以发起新的会话：（SId，f，H）new（i，a1，.，（a、k）（SIdJ，fJ，HJ）其中HJ、fJ和SIdJ定义如下。设s=|Sid|+1，是新会话的会话标识符，其中，A1}，A2}}，A1}，A2}}）56诉Cortier等人理论计算机科学电子笔记186（2007）49|Sid| 表 示 SId 的 基 数 。 HJ 定 义 为 HJ=H 和 SIdJ=SId{ （ s ， i ， （ a1 ， . ，ak））}。函数fJ定义如下。·fJ（sid）=f（sid），对于每个sid∈SId。诉Cortier等人理论计算机科学电子笔记186（2007）4957S{m}S{m}S[m]一一ppS<$lmm∈SSlm1Slm2S∈lb，ek（b），vk（b）b∈X.aSlm1，m2初始知识配对和非-Slm1，m2Slmii∈ {1，2}配对Slek（b）Slmadv（i）i∈NL lek（b）Sldk（b）加密和Lek（b）Slsk（b）SlmSlmSl[m]l解密ladv（i）sk（b）i∈Nsk（b）Slm签名Fig. 1. 扣除规则。·FJ（s，i，（ai，. 其中σ是部分函数σ：X → T1，并且：⎧σ（Aj）=aj1≤j≤kσ（Xj我）=n（ai，j，s）j∈N我们记得，执行角色的主体由Ai表示，因此，在这个角色，每个Xj形式的变量我 表示由Ai生成的随机数。send（sid，m）• 攻击者可以发送消息：（SId，f，H）−→（SId，fJ，HJ），其中sid∈SId，m∈Tl，HJ和fJ定义如下。 我们定义fJ（sidJ）=f（sidJ），每一个sidJ sid。 我们表示k（j）=（（lj，rj），.，（lj，rj））。 f（sid）=（σ，j，p），11一些σ，j，p。有两种情况。kj kj· 或者存在m和l的最一般的单位元θjσ。则fJ（sid）=（σ<$θ，j，p+1）和HJ=H<${rjσθ}。· 或者我们定义fJ（sid）=f（sid）和HJ=H（状态保持不变）。如果我们用SID=N×N×IDk表示所有会话id的集合，符号exe的集合cution traces是SymbTrl=（SID×（SID→（[X→Tl]×N×N））×2Tl）。一套corre-响应未标记的符号执行轨迹由SymbTr表示。映射函数·被扩展如下：如果tr =（SId0，f0，H0），. ，（SIdn，fn，Hn）是SymbTr 1的迹，tr =（SId0，f0，H0），. ，（SIdn，fn，Hn）∈ SymbTr其中SIdi简单等于SIdi且fi：SID→（[X → T]×N×N））且fi（sid）=（σ，i，p），58诉Cortier等人理论计算机科学电子笔记186（2007）49如果fi（sid）=（σ，i，p）且σ（X）= σ（X）.对手拦截诚实参与者之间的消息，并使用图1中定义的演绎关系计算新消息。直觉上，Slm意味着对手能够从消息集合中计算出消息mS.所有的演绎规则都是相当标准的，除了最后一条规则：最后一条规则规定对手可以从给定的签名中恢复相应的消息。本规则所考虑的功能与数字签名的标准计算安全定义不矛盾，诉Cortier等人理论计算机科学电子笔记186（2007）4959ek（a2）ek（a1）一个2的1对计算对手来说是重要的，对[4]的可靠性结果很重要。接下来，我们为未标记的协议绘制执行模型。如上所述，执行是基于捕获对抗能力的演绎关系的。从图1中可以得到如下的演绎规则，这些规则定义了一个新的概念。初始知识和配对与取消配对的规则集保持不变（当然，用“”替换“1 对于加密和签名，我们在加密函数{ }和签名函数[ ]中抑制标签adv（i）和l，用于规则加密和解密以及规则签名。也就是说，加密的规则是：Sek（b）SmS{m}ek（b）签名的是：S{m}ek（b）Sdk（b）森姆Ssk（b）SmS[m]sk（b）S[m]sk（b）森姆我们使用演绎关系来描述有效的执行轨迹集。我们说迹（Sid1，f1，H1），.，（SIdn，fn，Hn）是有效的，如果对手发送的消息可以通过Dolev-Yao运算计算。更准确地说，我们send（s，m）要求在有效迹中，每当（SIdi，fi，Hi）−→（SIdi+1，fi+1，Hi+1），我们有海姆。 给定一个协议栈，表示为Exec（执行）。在没有标签的模型中，执行跟踪的集合Exec（Exec）也有类似的定义。因此，我们要求每个发送的消息mJ满足Hijiamu J.例2.3使用例2.2中描述的Needham-Schroeder-Lowe协议，对手可以破坏代理a3，为代理a 3启动新的会话，第二个角色，玩家a1，a2并发送消息{n（a3，1， 1），a1}adv（1）到扮演第二个角色。 相应的有效跟踪执行为：corrupt（a3）new（2，a1，a2）（n，f1，n）−−→（n，f1，kn（a3））−→send（sid1，{n3，a1}adv（1））（{sid}，f，kn（a））ek（a2）123. −−−−−−−−−−−−−−−→Σ{sid1}，f3，kn（a3）<${{n3，n2，a2}ag（1）}，其中，sid1=（1， 2，（a1，a2）），n2=n（a2，1， 1），n3=n（a3，1，1），并且f2，f3定义如下：f2（sid1）=（σ1，2， 1），f3（sid1）=（σ2，2，2）其中，σ1（A1）=a1，σ1（A2）=a2，σ1（X1）=n2，且σ2将σ1扩张σ2（X1σ2（L1）=adv（1）。2.3标签和非标签执行模型的关联下面的引理（可以很容易地通过结构归纳证明）指出，只要一个消息是可演60诉Cortier等人理论计算机科学电子笔记186（2007）49绎的，相应的未标记的消息也是诉Cortier等人理论计算机科学电子笔记186（2007）4961子MM引理2.4SlmSm基于上述性质，我们表明，每当一个跟踪对应于一个协议的执行，相应的未标记的跟踪也对应于相应的未标记的协议的执行。外稃2.5tr∈Exec（）<$tr∈ Exec（）.关键论点是，只有模式匹配在协议中执行，当一个带有标签的术语匹配某个模式时，未标记的术语匹配相应的未标记模式。证明是通过归纳法对迹的长度进行的。 完整详情见附录A。Q3安全属性在本节中，我们定义一个用于指定安全属性的逻辑。然后，我们表明，逻辑是相当有表现力的，特别是，它可以用来指定，而标准的保密性和真实性属性。3.1初步定义我们在步骤p定义角色i的迹tr的局部状态集LSi，p（tr），LSi，p（（SIdk，fk，Hk）1≤k≤n）={（σ，i，p）|s∈ SIdk，s.t. fk（s）=（σ，i，p），1≤k≤n}.我们假设一个无穷集Sub的元变量的替代。我们的逻辑包含变量替换为变量替换的项之间的测试。更正式地说，让Tl代数定义为：L：：= L（xl）|ag（i）|adv（j）L子* =（x）|一|ek（a）|dk（a）|sk（a）|vk（a）|n（a，j，s）| T l，T1⟩ |{T l}L| [T l ] L子子分项ek（a）子项sk（a）其中xl∈X.l，n∈Sub，i，j∈N，x∈X，a∈ID。无标号代数TSub也相应地被定义。两个代数之间的映射函数定义为：（x）=={k}m，[k]l=[k] m，f（t1，. ，tn）= f（t1，. ，tn），否则。3.2安全逻辑在本节中，我们将描述安全属性的逻辑。除了标准的命题连接器，逻辑有一不62诉Cortier等人理论计算机科学电子笔记186（2007）49个谓词来指定诚实的代理人，项之间的相等性诉Cortier等人理论计算机科学电子笔记186（2007）496311⎧1 if t∈ ID和t不会出现在cor-i中。⎪破坏行为，即tr=e1，e2，.，n和[[NC（tr，t）]]=⎪你好，，a，s.t. ecorrupt（a1，.，（a、k）e，t a，1k1−→2 i⎪0.00否则⎧if∈（θ，i，p）∈ LSi，p（tr），我们有[[θ LSi，p（tr）. θ F（tr）]]=[[F（tr）[θ/θ]= 1，⎪000元，否则⎧如果ε1（θ，i，p）∈ LSi，p（tr），s. [F（tr）[θ/θ]]=1，[[LSi，p（tr）. F（tr）]]=0否则。图二. 解读。定义3.1逻辑L1通过归纳定义如下：F（tr）：：= NC（tr，t1）|（t1= t2）|€F（tr）|F（tr）F（tr）|F（tr）F（tr）|LSi，p（tr）.| ∃LSi,p (tr).ς F (tr)其中tr是公式的参数，i，p∈N，n∈Sub，t1和t2是下式的项：L子 . 请注意，公式由跟踪树参数化。像往常一样，我们可以使用φ1→φ2作为<$φ1<$φ2的捷径。我们类似地定义了相应的未标记逻辑L1：测试（t1=t2）是在Tsub上的未标记项t1，t2之间。映射函数·如预期的那样被扩展具体地，NC（tr，t）=NC（tr，t），（t1=t2）=（t1=t2），=LSi，p（tr）. F（tr）和LSi，p（tr）. F（tr）=LSi，p（tr）. F（tr）。这里，元数2的谓词NC（tr，t）用于指定未损坏的代理。数量函数LSi，p（tr）.和LSi，p（tr）.是在迹tr中步骤p处的主体i的局部状态上。我们的逻辑的语义被定义为封闭公式如下：标准的命题连接符和否定被解释为通常。平等是语法平等。量化器和同品种NC的解释如图2所示。接下来，我们定义一个协议何时满足公式φ∈ Ll。直接给出了无标记执行模型的定义非正式地说，如果φ（tr）对所有的迹都为真，则协议满足φ（tr形式上：定义3.2设φ（tr）是一个公式，φ（tr）是一个协议。 我们说满足安全性质φ，并写为|= φ如果对任意迹tr ∈ Exec（n），[φ（tr）]= 1。不64诉Cortier等人理论计算机科学电子笔记186（2007）49滥用符号，我们偶尔会将集合{tr| [[φ（tr）]]= 1}。 然后，|= φ精确地当Exec（执行）φ。诉Cortier等人理论计算机科学电子笔记186（2007）4965一一一个3一个2一的1的13.3安全属性的示例在本节中，我们通过指定保密性和认证性来说明逻辑的使用。3.3.1一个秘密财产设f（1）和f（2）是两方协议中发送方和接收方的角色。为了指定我们的保密属性，我们使用标准编码。也就是说，我们加上三分之一对于协议的作用，n（3）=（X13，停止），这可以被看作是某种见证。非正式地，保密属性Ps的定义指出，对于两个非损坏的代理a1和a2，其中a1扮演角色（1），a2扮演角色（2），第三个代理扮演角色的agent（3）不能获得关于nonceX1的1 由角色发送（1）（由A1扮演），当A1是诚实的，正在和一个诚实的代理人A2交谈时。φs（tr）=φ LS1， 1（tr）.φ LS3， 2（tr）. φJ[NC（tr，（A1））<$NC（tr，（A2））→<$（J（X1）=（X1））]3.3.2身份验证属性考虑一个两个角色的协议，角色1在n步后完成执行，角色2在p步后完成执行。对于这类协议，我们给出了周协议性质的一个变体[9]。非正式地说，这个属性表明，每当角色2的实例化完成时，存在角色1的实例化已经完成，并且它们同意某个变量的某个值，并且它们具有的确，他们互相交谈过在我们的例子中，我们选择这个变量为X1。1请注意，我们捕捉到一些代理已经完成了其执行量化适当地超过该代理的本地状态。更准确地说，我们只量化了它确实完成执行的州φa（tr）=<$LS2，p（tr）.<$$> LS1，n（tr）.<$J[NC（tr，<$（A1））<$NC（tr，<$J（A2））→（（X1 ）=J（X1））<$（<$（A2）=<$J（A2））<$（<$（A1）=<$J（A1））]请注意，尽管在当前版本中，我们的逻辑还不足以指定更强版本的一致性（如单射或双射一致性），但它可以适当扩展以处理这种更复杂的身份验证形式。4主要结果回想一下，我们的目标是证明|= φ = φ |= φ。然而，如在引言中所解释的，该下面的例子揭示了导致期望的隐含失败的原因66诉Cortier等人理论计算机科学电子笔记186（2007）49例4.1考虑某个协议的第一步，其中A向B发送一条消息，其中某个部分是要给某个第三方代理的。A→B：{Na，{Na}ek（C），{Na}ek（C）}ek（B）诉Cortier等人理论计算机科学电子笔记186（2007）4967一一一一一一一一的1的1一个2一个22一一与第一步相对应的A和B的角色的具体说明如下：以下为C1的定义2 和c22 是排序密文的变量）。int（1）=（init，{intX11，{X11中文（简体）ek（A3），{X11中文（简体）ek（A3）中文（简体）ek（A2）（2）=（{1，C12、C22Lek（A2），停止）我们假设A生成两倍的消息{Na}ek（C）。 请注意，我们在B收到第一条消息后停止执行B，因为这对我们的目的来说是足够的，但它的执行可能会继续，以形成一个更现实的例子。考虑安全属性φ1，它声明如果A和B在随机数1，那么B应该收到两次相同的密文。1φ1（tr）=φ LS1， 2（tr）.φ LS2，2（tr）. φJNC（tr，（A1））NC（tr，（A2））（（X1 ）=J（X1））→（C1）=J（C2））这个性质显然不适用于任何正常执行的标签协议，因为A总是发送带有不同标签的密文。因此，|= φ1。另一方面，我们可以证明，|在无标签执行模型中= φ 1。直觉上，这是成立的，因为如果A和B是诚实的代理人，1，则B接收到的消息已经由A发出，因此应该包含1相同的密文（在移除它们的标签之后）。4.1逻辑L1上面的反例依赖于这样的事实，即在没有标签的模型中相等的两个密文可能是从带标签的模型 因此，可能的情况是，尽管t1/=t2<$t1t2，反正蕴涵t1=t2t1=t2不成立，这又意味着包含密文之间的相等性测试的公式在没有标签的模型中可能为真，但在有标签的模型中为假在本节中，我们确定L1的一个片段，我们称之为L1这些测试是被禁止的。 形式上，我们1 2通过禁止任意否定来避免任意项之间的相等性测试公式和允许相等测试之间的简单条款。定义4.2一项t称为简单项，如果t=n（x），其中x∈X.a<$X.n且n∈Sub，或对于}}⟩⟩}⟩⟩}XX）68诉Cortier等人理论计算机科学电子笔记186（2007）492某个a∈ID，t=a，或对于某个a ∈ID，j，s∈N，t=n（a，j，s一个重要的观察是，对于任何单式项t，t=t成立。定义4.3逻辑L1定义如下：F（tr）：：= NC（tr，t1）|<$NC（tr，t1）|F（tr）F（tr）|F（tr）F（tr）|（t1/= t2）|LSi，p（tr）. |LSi，p（tr）.| ∃LSi,p (tr).ς F (tr),