基本协议逻辑完备性及反例生成的一阶谓词逻辑证明方法及应用

理论计算机科学电子笔记147（2006）73-92www.elsevier.com/locate/entcs基本协议逻辑的完备性和反例生成（扩展摘要）长谷部浩二1、2和Mitsuhiro Okada冈田光弘1，3庆应义塾大学哲学系邮编108-8345东京都港区三田2-15-45摘要本文给出了一个一阶谓词逻辑中的公理系统，用于证明安全性命题的正确性。 我们的公理和推理规则导出了协议逻辑文献中显式或隐式使用的基本推理规则，因此我们称我们的公理系统为基本协议逻辑（Basic Protocol Logic，简称BPL）。 我们给出了BPL的形式语义，并证明了完备性定理，使得对于任何给定的查询（表示正确性属性），是可证明的，它对任何模型都是真的。此外，作为我们的完整性证明的推论，BPL中的可证明性的可判定性对于任何给定的查询都成立。 在我们的形式语义中，我们考虑“跟踪”任何种类的原始动作序列、反模型（其从不可证明的查询生成）不能立即被视为可实现的跟踪（即，在所讨论的协议上被攻击的进程）。然而，借助Comon-Treinen算法的入侵者演绎问题，我们可以确定是否存在一个可实现的痕迹之间的正式反模型，如果有的话，所产生的证明搜索方法（用于我们的完整性证明）。我们还证明了我们的方法是有用的证明建设和使用一个简单的例子，通过分析。关键词：安全协议分析，一阶谓词逻辑，协议性质，证明搜索方法。1这项工作得到了文部科学省科学研究补助金、文部科学省人文科学卓越中心（庆应义塾大学）和Oogata-kenkyu-jyosei补助金（庆应义塾大学）的部分支持第一作者还获得了日本科学促进会的日本青年科学家奖学金2电子邮件地址：hasebe@abelard.flet.keio.ac.jp3电子邮件地址：mitsu@abelard.flet.keio.ac.jp1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.06.03874K. 长谷部，M.Okada/Electronic Notes in Theoretical Computer Science 147（2006）731引言对于安全协议的形式化分析，有两种典型的方法：一种是强调语法方法，如BAN逻辑[2]和[9，7，16]的协议逻辑（cf.也[1]用于协议组合逻辑项目概述），另一种强调语义方法，如串空间方法[18]和MSR [4]。前一种方法旨在证明一个保证协议在某个逻辑推理系统方面正确的属性，而后一种方法旨在检测协议中的错误（即，对协议的具体攻击）。在本文中，我们采取前一种方法。也就是说，本文的主要目的是给出[9，7，16]的协议逻辑的核心部分的简单公式，以证明协议是正确的。我们还旨在将这种正式的方法连接到一种用于检测的方法中。特别是，我们集中在[20，14]意义上的几种类型的协议属性，并研究在一阶谓词逻辑中，人们可以在多大程度上制定协议逻辑的基本部分，这足以证明我们的目标属性。(Thus在本文中，我们不讨论关于随机数或会话密钥的保密性。这种性质对于安全性分析也是一个重要的问题，因为某些协议的一致性依赖于它们的保密性。此外，我们还给出了一个完整的BPL的形式化语义，并提出了如何应用我们的框架来证明安全协议的正确性和检测非法性。为此，我们首先给出一个一阶谓词逻辑的公理系统来证明协议性质。在这个系统中，我们将关于随机数和密码学假设的一些性质形式化为具有等式的一阶谓词逻辑中的非逻辑公理，并给出了一种特殊形式的公式，称为查询形式，它表示限制于数据项数量的协议性质（即，在所讨论的协议中。然后，基本推理规则，显式或隐式地用于证明协议逻辑[9，7，16]中的一致性，是我们系统的派生规则。因此，我们的公式被称为基本协议逻辑（或简称BPL接下来，我们给出了BPL的一个形式语义，并证明了该定理的完备性，使得对于任何给定的查询，该查询在BPL中是可证明的，并且对于任何模型都是真的。这个定理是通过调整一阶谓词逻辑的通常证明搜索方法到我们的框架中来证明的（参见。[17]）。作为完整性定理的直接推论，我们的完整性证明的证明搜索方法提供了一个反例生成，如果给定的查询是不可证明的。此外，作为我们完备性证明的一个推论，BPL中可证明性的判定性也适用于任何查询。(In本文仅简略地给出完备性定理及其推论的证明的K. 长谷部，M.Okada/Electronic Notes in Theoretical Computer Science 147（2006）7375详细的证明将出现在本文的完整版本中。在我们的形式语义中，我们认为“跟踪”是任何类型的原始动作序列，因此反例（从不可证明的查询生成）不能立即被视为可实现的在所讨论的协议上的受攻击进程）。然而，借助于Comon-Treinen的因此，我们的完整性证明和Comon-Treinen的算法相结合由于我们的证明构造过程直接是一个反例生成，这项工作将有助于弥合安全协议分析的两个不同方向之间的差距，即证明正确性和发现攻击。最后，我们还证明了一个简单的例子，我们的方法是有用的证明结构和反求检测。本文件的组织。在第2节中，我们引入了一个公理系统，称为一阶谓词逻辑中的基本协议逻辑，并将我们的目标正确性属性形式化为一种特殊形式的公式，称为查询形式。在第三节中，我们给出了一个基于迹的形式语义，并证明了查询形式的可靠性定理。在第四节中，我们给出了查询形式的完备性定理和可证明性的判定性，并说明了如何利用证明搜索方法和Comon-Treinen算法为给定的查询构造证明/攻击过程。最后，在第5节中，我们提出了结论，并概述了本研究的一些进一步的方向。2基本协议逻辑我们首先将我们的语言固定在具有相等性的一阶谓词逻辑中，并给出一个公理系统，称为基本协议逻辑。在这个系统中，我们的目标的正确性属性被描述为一个特殊形式的公式，称为查询形式。2.1语言分类和术语。我们的语言是顺序排序的，它由排序名称，随机数和消息组成。A ，B，...，A1，A2，. （P，Q，...， P1，P2，.. . ，分别） 是常量（变量，分别）的排序名称（表示主体名称），以及N，NJ，.，N1，N2，. . . （n，nJ，...， n1，n2，.. . ，分别） 是常量（变量，分别）随机数所有的排序术语name和nonce都是排序消息的术语。76K. 长谷部，M.Okada/Electronic Notes in Theoretical Computer Science 147（2006）73- -±/±≥1≤≤K符号m，mJ，...，m1，m2，. 用于表示排序消息的变量。排序信息的复合项由函数from1，...，m n，{m}P和mP −1，表示消息的n元组串联，加密分别为P的公钥和私钥我们还使用元符号s，sJ，...，t，tJ，. 来表示排序消息的任何术语。4公式。我们引入五个二元谓词符号：P生成n，P接收m，P发送m，m=mJ和m mJ，表示作为随机数的新值n “前三个叫做行动谓词，Meta表达式acts用于表示动作之一谓词：生成、接收和发送。原子公式是如下表达式：P1作用于1m1;P2作用于2m2;···;Pk作用于kmk（其中k1和Pi（mi，resp.）可以与Pj（mj，resp.）对于任意i=j），m=mJ且m mJ。第一个是所谓的跟踪公式。这种类型的原子公式用于表示例如，原子消息mJ 我们还使用以下符号作为Meta表达式。αP，βP，...，αP，αP，.（或者简单地说，α，β，...，α1，α2，... . ）用于表示轨迹1 2对于形式为P作用于m，αP1;· · ·;αPk的m（或简称α→）用于表示P1act s1m1;· · ·;Pkact skmk（其中k表示α→的长度）。特别地，当每个P1对于Ik与P相同时（即，由单个主体P执行的一系列动作），我们也用α→P来表示这样的动作。追踪穆拉F或α→（α1;· · ·;αm）和β→（β1;·· ·;βn），其中β→包括α→（记为yα→β→），如果α→和β→满足以下条件：在β→中，对所有i（1≤i≤m），且f或anyαi<$βj和αk<$βl，如果ik则jl对于n，y1≤i，k≤m。（粗略地说，α→β→意味着所有的动作都是在α→中的谓词在β→中出现，并保持α →的顺序。）公式（用X，X，. . ）由以下语法构成。：：=α→|m=mJ|m±mJ|¬ϕ|ϕ∧ϕ|ϕ∨ϕ|ϕ→ϕ|x|x我们使用Meta表达式m[m→]来表示m→中的项列表。替换用这种符号表示发生最后，我们引入了迹的（严格）保序归并的概念公式α→而β→，则定义如下。4为了使我们的讨论更简单，在本文中，我们不考虑对称密码学，也不考虑共享会话密钥的协议，但是我们的形式化可以很容易扩展，以便包括这些概念。K. 长谷部，M.Okada/Electronic Notes in Theoretical Computer Science 147（2006）7377定义2.1（保序合并）α→（α1;·· ·;αl）和β→（αβ1;· · ·;βm）是μla→δ（αδ1;· · ·;δn）的过程，是由以下规则制定的。（作为特殊情况，如果α→，我们分别考虑l = 0和n = 0。）(i) δ1<$α1或β1。且β→是empty，则(ii) 对于每个i（1 ≤i≤n），如果α1;···; αj<$δ1;···; δi和β1;···; βk<$δ1;···;δi（对于某些0 ≤j≤l和0 ≤k≤m），则δi+1<$αj+1或βk+1。(iii) 如果→δ<$δ1;· · ·;δi;δi+1;· · ·;δn是α→和β→的保序归并，δi<$δi+1，则→δJ<$δ1;· · ·;δi−1;δi+1;· · ·;δn也是保序的α→和β→的合并。我们还介绍了另一种类型的保序合并，根据规则（i）和（ii），称它为严格或保留α→和β→。例如，α1;α2;α2;α3和α2;α1;α3;α2和α1;α2;α3是α1; α2和α2; α3的保序合并，而最后一个不是严格的保序合并。角色描述一个协议是一组角色，每个主体（比如P）的角色被描述为一个形式为α→P<$Pact s1m1;· · ·;Pact skmk的轨迹。作为一个例子，这里我们考虑Needham-Schroeder公钥协议[15]，其非正式描述如下。1. P→Q：{n1，P}Q2. Q→P：{n1，n2}P3. P→Q：{n2}QNeedham-Schroeder公钥协议的发起者例2.2（Needham-Schroeder协议的作用）初始化NS[P，Q，n1，n2]P生成n1;P发送{n1，P}Q;P接收{n1，n2}P;P发送{n2}Q响应NS[P，Q，n1，n2]Q接收{n1，P}Q;Q生成n2;Q发送{n1，n2}P;Q接收{n2}Qα→P作用的公式是由P，Q→n，其中一些类似的术语。例如，InitNS[A/P，B/Q，N1/n1，N2/n2]78K. 长谷部，M.Okada/Electronic Notes in Theoretical Computer Science 147（2006）73±和RespNS[A/P，B/Q，N1/n1，N2/n2]分别是InitNS和RespNS的运行，我们称这样一组实例为A，B，N1，N2数据项。角色α → P的游程的严格保序合并称为α→P的多重游程。2.2基本协议逻辑我们通过添加以下公理（I）、（II）和（III）来扩展通常的一阶谓词逻辑。这个公理系统被称为基本协议逻辑。(I) 项上的泛句公理 我们假定下列公理为=和±。 当一个有限的文字集{t1=tJ1， . ，tn=tJn，s1±sJ1， .. . sj±sJj，u1 uJ1， . ，uk uJk，v1/±v1J， . ，vl/±vlJ}在以下情况下不可满足：我们的语言的自由项代数（其中=和±是自由t代数中的单位项和子项关系），则<$m →<$（t1=TJ1< $···< $tn=tjnS1sJ1sjsJju1=uJ1uk=uJkv1v1JvlvlJ）是一个公理。请注意，满意度问题在自由项代数（cf. [19]），因此类型1的公理集是递归的。(II) 跟踪公式的规则。 我们引入以下公理（1）和（2）对于m的迹，其中γ→i的α→和β→。（1）β→→α→（对于α→β→）（2）γ→1π···πγ→n参与α→πβ→(III) 属性之间关系的公理。我们引入下面的一组公式作为非逻辑公理。这些公理代表了关于随机数和密码学假设的一些性质。(1) 订购1：PQnm（P生成n→ <$（Q发送/接收m;P生成n））(2) 订购2：PQmmJ（P发送/接收vesm→mJJ（Q发送mJJ;P发送/接收vesm{mJ}Q−1±mJJ））(3) 随机数验证1：PQn1m2m5m6（P生成n1，P发送m2，n1±m2，P接收m5n1±m6<${m6}Q−1±m5m7（P发送m7→m3m4（P发送m2;Q接收m3;Q发送m4;P接收m5<$n1±m3<${m6}Q−1±m4））K. 长谷部，M.Okada/Electronic Notes in Theoretical Computer Science 147（2006）7379−≤≤Q→n（i）[P，Q，→n]<$Only（α→（i）[P，Q，→n]）(4) 随机数验证2：PQn1m2m5m6（P生成n1，P发送m2，n1±m2，P接收m5{m6}Q/±m5m7（P发送m7∧ ∀m8(n1±m8∧m8±m2→m8± {m6}Q)→m3m4（P发送m2;Q接收m3;Q发送m4;P接收m5{m6}Q±m3<$n1±m4））(5) 随机数验证3：PQn1m4m5m6m9（P生成n1，P发送m2，n1±m2，P接收m5{m6}Q/±m5m7（P发送m7∧ ∀m8(n1±m8∧m8±m2→m8± {m6}Q)REQ发送 {m4}Pn1±m4m10（Q发送m10<$n1±m10→m10={m9}P）→ {m9}P=m5）这里，表达式排序1和2分别表示与随机数和加密消息相关的动作的排序。随机数验证1和3在很大程度上依赖于[10]引入的基于串空间方法的认证测试的思想：随机数验证1是传入测试的形式化，随机数验证2和3是传出测试的形式化。2.3查询表单和正确性属性我们的目标的正确性属性描述在一个特殊形式的公式，称为查询形式。查询形式包括主体的诚实性的形式化（表示为y H o n es t（α → P）），其定义如下。第2.3节（诚实的原则Honest（α→P[P，Q→，→n]）def→P→P→这里，α→P[P，Q→，→n]是形式Pacts1m1;Pacts2m2;· · ·;Pactskmk的角色，其中每个动作i（1 i k）是发送、接收和生成中的一个，并且α→P（i）[P，Q→，→n]表示α→P[P，Q→，→n]的以Pact simi（对于0≤i≤k）结束的n个初始段，即， α→P（i）[P，Q→，→n]→Pacts1m1;· · ·Pactsimi. （特别是在这种情况下，α→P（0）表示T。）Only（α→P（i））表示如下的模，其其含义是i∈ {j|mj∈Sends（α→P[P，Q→，→n]）}<${k}α→80K. 长谷部，M.Okada/Electronic Notes in Theoretical Computer Science 147（2006）73∧∧∈∈∈{|}≡···0@0@0BAgeneratesn1;Asends{n1，A}Q;Areceives{n1，n2}A;Asends{n2}Q1C1C∧∀m4(Asendsm 4→⊥)A@m5（A接收m 5）∨∧∀3 3→ 31@m 5（A接收m 5m 5 =n1，n2A）Only（α→P（i））nn1（P基因速率n1→n1∈基因速率（α→P（i）n∈m2（P发送m2→m2∈Sends（α→P（i）n∈m3（P∈m3→m3∈R∈ves（α→P（i）这里，Sends（α→P（i））表示集合mj P发送mjα→P（i）。（Receives（α→P（i））和基因速率（α→P（i））相似。设置理论符号，例如ch为mSends（α→P（i））（以及mReces（α→P（i））和mGenerates（α→P（i）是析取形式的缩写：例如，如果Sends（α→P（i））={mJ1， . ，MJ}，则m∈Sends（α→P（i））表示mula（m=MJ1）<$（m=MJ2）<$··<$（m=MJ）. （作为特殊情况，如果Sends（α→P（i））是empt y，则m∈Sends（α→P（i））表示n。）因此，每个ch析取α→P（i）Honest（α→P）中的Only（α →P（i））表示P在其运行的每一步中的动作的Pacts1m1;P作用于 i表示P在这一步的作用，O n l y（α → P（i））表示P只作用于α → P（i）。在特殊情况下，α→P（0）Only（α→P（0））表示P不作作用。因此，Honest（α→P[P，Q→，→n]）表示α→P的作用，并使用相同的数据项Q→并且→n，f或each chrun”。作为一个例子，我们给出了下面的Needham-Schroeder协议的发起者（比如A）的诚实性示例2.4（NS协议的发起者诚实（初始化NS[A/P，Q，n1，n2]）第1页第2页n3（A生成n3→ n）1∧∀m5(Areceivesm5→⊥)0BA基因速率n1;A发送{n1，A}Q1C∨∧∀3 3→ 31n（A生成nn=n）m4（A发送m 4→m 4={n 1，A}Q）∧∀ → ⊥n（A生成nn=n）m4（A发送m 4→m 4={n 1，A}Q∧∀→{}请注意，我们对诚实的形式化比通常意义上的更强。也就是说，我们对诚实的定义仅限于用于诚实主体运行的单个数据项集然而，通过将一定数量的相同角色的严格保序合并视为单个角色，我们可以表示关于用于所有可能的角色的任何有限数量的数据项集合的诚实性。一AAK. 长谷部，M.Okada/Electronic Notes in Theoretical Computer Science 147（2006）7381联系QQn1n2n1n∧∀m4(Asendsm4 → ⊥)∧∀m5(Areceivesm5 →⊥)A发送{n1，A}Q;A接收{n1，n2}A;A发送{n2}Q→m4={n1，A}Qm4={n2}Qm4={n1，A}Q'm4={n2}Q'）A接收m5→m5= {n1，n2}A接收m5={n1，n2}A⎟⎠由诚实的校长管理作为一个例子，我们给出了Needham-Schroeder协议的发起者（比如A）诚实的情况′等位基因n3（A基因ratesn3→n）突变A基因发送n1;A发送{n1，A}Q∨⎜⎝nn3（A生成n3→n3=n1）m4（A发送m4→m4= {n1，A}Q）∧∀m5(Areceivesm5→⊥)∨⎜⎝nn3（A生成n3→n3=n1）m4（A发送m4→m4={n1，A}Qm5（A接收m5→m5= {n1，n2}A）A基因速率n1;A发送{n1，A}Q∨⎜⎝n=n3（A基因速率n3→n3=n1<$n3=n′1）′m4（A发送m4→m4={n1，A}Q∧∀m5(Areceivesm5 →⊥)A发送{n1，A}Q;A接收{n1，n2}A;A发送{n2}QA基因发送n′1;A发送{n1，A}Q′⎜′⎟∨⎜⎝nn3（A生成n3→n3=n1<$n3=n1）′⎟⎠∧∀m4(Asendsm4→m4={n1,A}Q∨m4={n2}Q∨m4={n1,A}Q')m5（A接收m5→m5= {n1，n2}A）基因A发送n1;A发送{n1，A}Q;A接收{n1，n2′}A;A发送{n2}Q⎞⎟⎞⎟A基因发送n′1;A发送{n′1，A}Q′;A接收s{n1，n′2}A;A发送{n2}Q′∨⎜⎝n=3（A基因速率n3→n3=n1<$n3=n′1）A发送m4′′⎟⎠⎟⎠′′正确性性质的一阶形式化我们引入了一种通用形式的公式，称为查询形式，来表示我们的目标正确性属性。为了使讨论更简单，我们只考虑两方认证协议的情况，然而我们的查询形式可以很容易地扩展，以便表示相对于其他类型的协议，其中包括两个以上的主体的正确性属性。定义2.5（查询形式）查询形式是以下形式的公式。Honest（α→P）→Q→Only（β→Q）→→γ我们的目标的正确性属性被描述为一个特殊的情况下的查询形式。例如，质子的非注入一致性={α→P[P，⎟⎠82K. 长谷部，M.Okada/Electronic Notes in Theoretical Computer Science 147（2006）73}Q，→n]，β→Q[P，Q，→n]从响应者（S a y，B s）的观点可以描述为以下公式。Honest（α→P[A/P，Q，→n]）Hβ→Q[A/P，B/Q，N→/→n]nnly（β→Q[A/P，B/Q，N→/→n]）→α→P[A/P，B/Q，N→/→n]用协议定义的α→P[A/P，B/ Q，N → / → n ]和β→Q[A/P，B/Q，N→/→n]的严格保序归并其中α→P[A/P，B/Q，N→/→n]分别为0nly（α→P[A/P，B/Q，N→/→n]）。实际上，我们对协议性质的形式化比通常意义上的弱，因为我们的诚实假设比通常意义上的强。然而，正如我们在诚实的定义（定义2.3）中所解释的那样，我们的查询形式可以扩展，以便诚实的主体可以使用有限数量的数据项集用于他/她的运行。BPL与其他协议逻辑的比较在结束本章时，我们想指出BPL和其他协议逻辑。其中一个主要的困难是关于诚实的推理的形式化。在[9，7，16]的协议逻辑中，诚实的概念被形式化为一个原子公式，并通过一个特殊的推理规则得出关于诚实的推论。另一方面，在BPL中，诚实的概念被形式化为非原子公式，并且所有关于诚实的推论都是由逻辑推理规则得出的，并且在[9，7，16]中基本上使用的关于诚实的推论是BPL中的派生规则。更确切地说，为了证明协议的正确性，[9，7，16]的协议逻辑隐式或显式地使用了三种类型的推理：我们将这些推理作为附录A中的诚实规则至于非逻辑公理，我们提出的非逻辑公理（1）-（5）(III)第2.2节中介绍的方法基本上不依赖于我们的框架。特别是，正如我们将在第4节中展示的那样，我们的完备性和可判定性论证并不受非逻辑公理的选择的影响。本文中所选用的非逻辑公理是证明我们所要的正确性的最简单的形式化方法之一。 协议逻辑中的基本推理规则实质上是BPL的派生规则。在这里，我们强调BPL是在一阶谓词逻辑中形式化的，没有任何时间模态运算符，也没有在[9，7]的协议逻辑中使用的Floor-Hoare风格的动态运算符：这就是为什么我们称我们的系统为“基本”的原因K. 长谷部，M.Okada/Electronic Notes in Theoretical Computer Science 147（2006）7383⟨ ⟩ ⟨⟩联系我们∈⊆∈ ∈ ⟨ ⟩ ⟨⟩3形式语义与合理性在本节中，我们给出了我们的系统的语义一个t ra cemodeldel（或modeldel）是M=（DP，DN，α→，Φ）其中DP是一个集合，称为名字域，DN是一个集合，称为随机数域，DM是自由代数域（即，一阶项的集合）由DP和DN以及项构造规则确定，、，K（，）和K−1（，），（其中、是有序对函数符号，K（，）和K−1（，）是密钥加密和解密函数symbols），并且α→是迹。（注意，我们经常使用缩写，sayn1，n2A，n3B−1for K−1（B，n1，K（A，n2），n3）.）在本文中，且A基因为n，其中A∈DP，m∈DM.迹α→的形式为（原始）动作αi的有限序列α1;···;αn。Φ（A）∈DP，名称排序的常数符号A，以及随机数排序的常数符号N的Φ（N）DN。我们将Φ推广到变量的求值，使得Φ（P）DP和Φ（n）N，像往常一样。Φ（t1，t2）= Φ（t1），Φ（t2），Φ（K（A，t））=K（Φ（A），Φ（t）），Φ（K−1（A，t））=K−1（Φ（A），Φ（t））。任何动作谓词α（A，m），Φ（α（A，m））=α（Φ（A），Φ（m））. 为了追踪-形式为α1;···; α n，Φ（α1;···; α n）=Φ（α1）;···; Φ（α n）的公式。对于模型M=（DP，DN，α→，Φ），m1±m2在Mi中成立，其中Φ（m1）是Φ（m2）的子项，m1= m2在Mi中成立，其中Φ（m1）和Φ（m2）是相同的项. β→在Mi∈Φ（β→）中成立α→。所有一阶逻辑连接都是一个以标准的方式解释。定理3.1（合理性）如果查询形式的闭公式Honest（α→P）→Q→Only（β→Q）→→γ在BPL中成立，则在任意模型M=（DP，DN，α→，Φ）中成立。这个定理是由一个标准归纳法证明的关于长度的证明.4完备性、可判定性及其在反例生成中的应用在本节中，我们首先通过证明搜索方法来证明查询形式的完备性定理。此外，作为完备性证明的一个推论，我们还证明了对于任何给定查询的可证明性的可判定性。（实际上，在这份初步报告中，我们只是概述了这些证据。详细的证明将出现在本文的完整版本中。）接下来，作为这些结果的应用，我们展示了如何找到对所讨论的协议的攻击。作为主要结果，借助于Comon-Treinen算法，84K. 长谷部，M.Okada/Electronic Notes in Theoretical Computer Science 147（2006）73−TT►对于入侵者推断问题[6]，对于任何给定的查询，只要我们对数据项的数量设置任何上限，我们就可以确定是否存在对所讨论的协议的攻击。在本节的最后，我们还展示了一个证明构造/反例生成的具体示例。4.1查询表单我们的完整性陈述如下。定理4.1（完备性）如果查询形式的闭公式Honest（α→P）→Q→Only（β→Q）→→γ若M=（DP，DN，→δ，Φ）模型成立，则该公式在BPL中成立。为了证明完备性定理，我们使用证明搜索方法（本质上与Beth的tableau方法相同特别是，我们遵循Takeuti [17]第1.8节中描述的方法和几个术语（如阶段，分支和可用术语）。为了将我们的查询形式固定为微积分风格的证明搜索方法，我们首先将我们的查询形式稍微修改为以下的“”，称为查询“”。Honest（α→P），β→Q，Only（β→Q），Axioms（1）-（5）α→γ这里，公理（1）-（5）表示在2.2节中介绍的（III）的非逻辑公理（1）-（5）的集合。我们把这些公式作为查询的假设。现在，我们回顾一下证明施工过程，并注意到在我们的设置中需要稍微修改的地方。证明施工过程。 对于任何查询S，我们将定义S的证明构造树（用（S）表示）。 （S）是一个（可能是无限的）树，它是在轮中构造的：证明构造过程从第0轮开始，在那里我们在树的底部写入查询S，然后转到第1轮。 然后每个回合i（对于i = 1，2，.. . ）由阶段组成（k = 0，1，2，...，14）由案件定义：情况I：每个最上面的顶点，其形式为Γ满足一个人如果满足以下条件（C1）（C3），则验证构造过程终止。我们把这种封闭的管道称为“封闭的管道”。(C1)r和r包括一个共同的公式（C2）t1=tJ1， . ，tn=tJn，s1±sJ1， . . sm±sJm∈Γ且u1=u1J， . ，uk=uJk，v1±v1J， . ，vl±vlJ∈n，并且文字{t1=tJ1， . ，tn=tJn，s1±K. 长谷部，M.Okada/Electronic Notes in Theoretical Computer Science 147（2006）7385⊆►►►−−►→ ∀∃¬ ∧∨--∧ → ∨· ··∨不sJ1， .. . sm±sJm，u1uJ1， . ，ukuJk，v1/±v1J， . ，vl/±vlJ}不满足于我们语言中的自由项代数这个条件本质上是一样的如第2.2节中的公理（I）。（C3）Γ包含mulaα→并且m包括mulaβ→的迹线与β→α→。这个条件基本上与2.2节中f（II）的公理（1）情况II：不是情况I。 然后，根据k = 0，1，2，.，13，14，其中情况k= 0，1，2，...，11和14与[17]相同，即，k= 0和1涉及符号，k= 2和3涉及符号，k= 4和5涉及符号，k= 6和7涉及符号，k= 8和9涉及符号，k=10和11涉及符号。除了上面的阶段，我们插入以下规则作为k= 12和13。• k= 12（等式规则）：令Γ[t][t]是树的任何最高层，由阶段k1定义。然后写下Γ[t]<$[t]，s=t和s=t， Γ[t]， Γ[s/t]<$[t]，<$[s/t]上面的Γ [t][t]，对于所有项s和t，它们由所有可用的排序项name和nonce与函数符号组成。我们引入这个阶段，而不是无限方案<$x<$y（x=y<$F（x）→F（y））作为查询中的假设• k=13（迹公式的规则）：设Γ是由k阶数定义的树的任何最高阶数1，且α→1， …，α→j是出现在Γ中的迹公式。然后写下形式的所有序列→γi，Γj其中→γi是α→1， . 的 保 序 归 并 。 ，α→j，且ΓJ是Γα→1， . ，α→j.这一阶段是第二节中公理（II）（2）的if-部分的组合2.2（即， →γ1α···β→γn→α→αβ→）和n-左约化。 注意，我们不需要考虑公式（ II ） （ 2 ） 的 唯 一 假 设 部 分 （ 即 ， α→β→→γ1→γn），因为在我们的证明-构造过程中，不存在一个形式为α→β→β的方程出现在我们的假设中。在应用了第14阶段的规则之后，如果最上面的一个节点没有闭合，那么我们进入第i+1轮，重复上面的过程。完备性定理的证明简图。从现在开始，我们展示我们的完备性证明，这是通过使用以下引理证明的。主引理 如果存在分支S0，...，S3×14在（S0）中，其中S3×14是第三轮结束时的一个非闭的子，则存在对S0的一个反模delM=（DP，DN，→δ，Φ）.在这里，我们勾勒出如何从S3×14构造这样一个反模型M。86K. 长谷部，M.Okada/Electronic Notes in Theoretical Computer Science 147（2006）73∈∈2±∈¬∨假设θ→是在的左手侧中的模拉ap的迹线，S3×14。(Note在每一轮结束时，该图的左手侧总是仅包括单个迹公式。）我们通过以下步骤固定DP和DN：我们首先取S3×14中出现的所有文字的集合并解决这些文字的满足问题，然后分解由复合项组成的每个文字{N1，A}B={n1，P}Q分解为N1=n1，A=P和B=Q），然后取DP和DN作为它们分解的文字我们通过对项的长度的归纳来定义项的赋值Φ如下。作为基本情况，排序名称或随机数的每个常量和变量由其代表（即，Φ（N）= N（D N），（1）n=0（D N）其中N和n是等价的代表类，分别为N和n，对排序名的解释是相似。）排序消息的每个变量（比如m），既不是排序名也不是随机数，都由m的等价类的代表来解释。项的归纳步骤和每个公式的求值定义由第3节中的Φ的定义来遵循。最后，当y→δ时，我们称e→δ=Φ（θ→）。从现在开始，我们证明M是S0的反模型。证明这一事实的基本思想是利用以下事实：（1）每一个非逻辑公理在M中是可满足的;（2）关于迹公式的公理在M中是可满足的;（3）关于=和的公理在M中是可满足的。至于事实（1），对于证明构造树中的任何分支，如果一个本征变量（比如m）出现在该分支中，那么这样的本征变量总是出现在形式为A作用于m的公式中。另一方面，作为诚实假设的后代，Aactsm m=t总是出现在分支中，其中t是在这一阶段出现的项因此，如果T是第3轮中的项的集合，对于出现在第3轮之上的特征变量m，具有某个t T的方程m=t总是出现在左侧，则搜索域在第3轮之上不会增加至于事实（2）和（3），它们分别直接从逻辑公理（I）（在2.2节中介绍）和终止条件（C2）的对应关系，以及逻辑公理（II）（在2.2节中介绍）和终止条件（C3）的对应关系导出。通过这个主引理，我们的完备性定理的证明如下。对于任何给定的查询形式，如果约简树的每个分支直到Round3终止，那么我们可以很容易地写一个证明这个查询。然后通过对位，对于任何不可证明的查询，存在一个分支，该分支包括在第3轮结束时，一个非封闭的节点（例如，S3×14）。利用主引理，我们从S3×14的信息中得到了一个反模型.然后通过对比，证明了完备性定理成立.Q这个主引理不仅保证了我们的完备性成立，K. 长谷部，M.Okada/Electronic Notes in Theoretical Computer Science 147（2006）7387∀∃此外，我们只需要制作一个直到第三轮的证明构造树来找到一个反模型。因此，如果我们为- 左，- 右和等式规则，下面的可判定性直接从主引理导出。推论4.2（可判定性）对于任何给定的查询形式，查询在BPL中的可证明性是可判定的。此外，以下定理成立。定理4.3（有限数量的最小反模型）对于任何不可证明的查询形式，从查询的证明构造树直到第三轮结束所获得的反模型的数量是有限的。4.2构建受攻击的进程通过前一小节中提出的证明搜索方法，对于任何给定的查询，如果查询成立，我们就得到一个证明否则，我们获得查询的反模型.然而，从这些反模型中获得的痕迹不能立即被认为是被攻击的过程，因为在我们的语义学中，我们认为是一个为了找到一个被攻击的进程，我们引入了可实现的跟踪的概念，通过Comon-Treinen可变现迹线的定义如下。定义4.4（可实现的t族）设→δe是一个函数序列，P1表示m1，. ，Pk表示mk是→ δ中所有接收动作的列表，而→δ（i）是f→δ的初始段，它与Pk表示mi。→δ是可实现的，如果它满足-证明了如下条件：对任意P i接收m i（1 ≤i≤k），m i可从[ 6 ]的Comon-T reinen系统中的Sends（→δ（i−1））证明（可检索）.直观地说，可实现的跟踪是一系列动作，其中每个接收消息都可以由Dolev-Yao入侵者生成[8]。显然，从一个可实现的跟踪，这是从一个反模型的查询，我们可以很容易地构建一个具体的攻击过程中的协议问题，通过插入一些合适的入侵者由于检查可实现迹的过程是可判定的（参见[6]），下面的定理立即推导。定理4.5（被攻击进程检测的可对于任何给定的查询，是否存在一个反模型M=（DP，DN，→δ，Φ）使得→δ是一个可等价的查询的问题是可判定的.88K. 长谷部，M.Okada/Electronic Notes in Theoretical Computer Science 147（2006）73关于我们正如我们在查询表单的定义中所解释的那样，我们可以表示任何数量的数据项集（由诚实主体使用）的正确性属性。因此，这种可判定性保证了我们可以确定是否存在一个攻击的痕迹，每当我们设置任何上限的数据项的数量使用的主体。这种可判定性对应于以前的作品的结果（参见。[4]）。找到对所讨论协议的攻击的合适策略是通过扩展查询形式来增加搜索域。如果我们不对搜索域设置限制，这个过程通常是无限的。然而，这个过程是最佳的，因为相同的不可判定性结果也适用于一些其他框架（cf. [4]）。4.3一个被攻击进程检测在这一小节中，我们展示了一个简单的例子，说明如何从通过对不可证明查询的证明搜索获得的反模型中找到受攻击的在这里，我们考虑Needham-Schroeder公钥协议的匹配会话（从响应者RespNS[A/P ， B/Q ， N1/n1 ， N2/n2] ， Honest （ InitNS[A ， Q ， n1 ，n2]），公理，n3（B生成n3→n3=N2），m5（B接收m5→m5={N1，A} B► A生成N1;A发送{N1，A}B;B接收{N1，A}B;B生成N2;B发送{N1，N2}A;A发送{N2}B;B接收{N2}B在这个查询的证明构造树中，在第三轮结束时有16个非闭合分支，它们具有以下形式。（这里我们使用示意性表达式：t1是N1