理论计算机科学电子笔记126（2005）53-75www.elsevier.com/locate/entcs安全协议的语义推理Arjen Hommersom1奈梅亨信息与计算科学研究所荷兰奈梅亨拉德布大学约翰-朱尔斯·迈耶荷兰乌得勒支大学信息与计算机科学研究所埃里克·德·温克荷兰埃因霍温理工大学数学与计算机科学系荷兰莱顿大学Leiden Institute of AdvancedComputer Science摘要我们提出了一个模型理论的方法推理安全协议，应用动态认知逻辑的 这使我们能够准确地描述随后的认知状态的代理参与的协议，使用Kripke模型和它们之间的转换的基础上，年龄的不确定性的状态与时间的关系在该协议中的时间间隔。在某些情况下，您将考虑SRA三次通过协议。关键词：模态逻辑，信念修正，语义更新，安全协议，动态认知逻辑1通讯作者：arjenh@cs.ru.nl1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.11.01354A. Hommersom等人理论计算机科学电子笔记126（2005）531介绍在当今安全协议的设计是困难和容易出错的[20，2]，这使得（自动）验证协议至关重要。自80年代后期以来，在其他研究中，推理安全协议的一条研究路线是基于Burrows，Abadi和Needham在[5]中提出的所谓BAN逻辑的使用。这是一种认知逻辑，通过与安全推理相关的构造来增强，例如具有加密密钥的处置以能够解码消息并因此知道其内容的属性。虽然已经报道了许多有用的结果（例如，[16，1，21]），由于它们的复杂性和它们的语义基础，使用BAN逻辑来证明安全协议的正确性的成功是有限的（cf.[3、6、22、19]）。在本文中，我们将应用Gerbrandy [13，14]，Baltag和Moss [8，4，7]，Van Dit- marsch [10，11]和Kooi [17]最近发展的动态认知逻辑的见解。此外，与传统的BAN逻辑方法相反，我们的方法是语义或模型理论的。我们使用Kripke模型来表示协议中所涉及的代理的认知状态，类似于Van Ditmarsch的S5保持方法来分析某些类型的涉及知识的游戏。从Baltag和Moss为此，我们还需要运营商展开模型，这反过来又启发了Gerbrandy不同之处在于，在我们的方法中，只需要部分展开。此外，我们提出了一种语言来表达的信念更新的背景下，安全协议以及这些更新的属性，并给出了语义，这种语言中提到的模型和他们的操作。由于我们的方法是模型论的，我们相信它可以作为工具支持的安全协议验证的起点作为一个案例研究，说明我们的方法，我们将考虑所谓的SRA三遍协议，并证明它的属性。这不是我们的目的，以证明该协议是完全安全的（因为它是不是在充分的一般性），但我们将证明，如果代理参与协议是诚实的，那么入侵者观察通信不学习任何关于纯文本消息在一个单一的运行。此外，我们展示了入侵者能够了解参与的代理A. Hommersom等人理论计算机科学电子笔记126（2005）53552预赛在本节中，我们简要讨论了一些关于我们将处理的更新和我们将使用的认知模型的知识和背景首先，我们定义了客观公式的概念和o序列性的概念定义2.1确定命题变量的集合P，也称为原子。目标公式类是最小类，使得• 所有命题变量p∈ P都是客观的;• 如果φ是客观的，那么<$φ是客观的;• 如果φ1和φ2是客观，则φ1<$φ2是客观。因此，客观公式不涉及信念。就我们的目的而言，重要的是每个主体都用相同的“客观”信息来区分世界。这导致了O系列模型的概念定义2.2克里普克模型M = S，π，R1，...， Rm∈ R m是o-序列i ∈ R，对所有i，1 ≤i≤m，且w∈S，存在v∈S使得（w，v）∈Ri，且对所有目标公式φ，（M，w）成立|= φ（M，v）|= φ。我们使用a、b、c等作为典型的代理，取自A类。我们使用符号{x}ka来表示用代理a的密码密钥ka加密的消息x。此外，B被用作doxastic模态算子。例如，Baφ应读作我们解释了标准Kripke模型（M，s）=（S，π，R1，…，Rm，s），其中（M，s）|= Biφ iRi（s，t）→（M，t）|= φ。这个状态被称为现实世界。我们要求关系Ri是O-序列的、传递的和欧几里德的。 这就产生了一类我们称之为Kt45的模型，它是著名的doxastic逻辑KD45模型类的一个真子集。小写字母t指的是公理(t)Biφφ，对于每个目标φ系统Kt 45相对于o-序列、传递和欧几里得模型类是合理的[15]。我们将证明我们引入的关键在于，在Kt 45模型的世界中，对于一个客观公式φ，我们不能同时拥有Biφ和Bi<$φ。这是合理的，因为我们假设代理人对协议是有意识的。因此，他们不会推断客观矛盾。这种客观性是在每个州本地捕获的因此，我们引入的操作可以在不破坏客观信息的情况下限制状态集对于下面的安全协议的分析，我们假设我们对协议的不同运行中的变量的值为56A. Hommersom等人理论计算机科学电子笔记126（2005）53例如，协议运行中的程序变量p具有值[p]]。 在现实世界中，显然，p=[[p]总是正确的。然而，在我们下面使用的Kripke结构的操作中，跟踪真实世界是很麻烦的。因此，我们假设给出了一个解释[·]]，它在需要时提供程序变量的“真实”值。在某种状态下，p=[[p]的情况很可能是这样的。 从现在开始，我们将把p=[[p]]转换为p。(Thus转换程序表达式变成命题变量 ） 。 类 似 地 ， <$p 是 p=[[p]] 的 缩 写 。 例 如 ， 智 能 体 a 学 习 到Bbp<$Bb<$p，知道智能体b已经给程序变量p赋值。我们考虑的更新类型是（i）变量的公开声明(ii)一个变量的私人学习和（iii）关于其他代理的知识的私人学习。第一种类型的更新通常运行如下：在开放网络中，代理a向代理b发送消息。从安全的角度来看，可以假设Dolev-Yao框架[12]，其中网络中的所有代理也可以读取此消息。然而，在开放的网络中，也可以进行第二种类型的更新，即私人学习。例如，代理b从代理a接收消息{x}k。这里，{x}k表示具有用（对称）密钥k加密的内容x的消息。如果b拥有密钥k，则b私下学习消息内容x（假设密钥k在a和b之间共享）。最后一种更新，学习他人的知识，可能是最有趣的。假设所有代理都知道协议运行中的步骤是现实的。因此，观察一个代理接收消息将增加其他代理的知识。例如，如果代理a向代理b发送消息{x}k，则代理c获知b已经获知消息{x}k中包含的信息，但是通常，如果c不拥有密钥k，则c不获知x。我们在这里不考虑更强类型的更新例如，我们不会更新诚实代理的信念，使其了解入侵者已经了解了其他人。在本文中，我们限制自己更新信念的目标公式和信念的目标公式。3更新结构在本节中，我们将详细介绍各种类型的更新。我们将从定义3.1小节中命题的更新开始。在3.2小节中，我们将定义一个信念更新，用于了解他人信念的代理。我们以两种稍微不同的方式来实现这一点，即通过改变描述代理方效应的函数。A. Hommersom等人理论计算机科学电子笔记126（2005）5357我我一B3.1目标更新我们将使用的目标公式的信念更新基于[18，8]。构造工作如下：我们将复制模型的状态，使得old（S）中的旧世界对应于原始模型中的信息，new（S）中的新世界对应于新信息。定义3.1设世界（M，w）=（S，π，R1，.，Rm，w），一组代理人B，并给出一个目标公式φ，使得（M，w）|= φ。然后UPDATE（φ，B）（M，w）=（φSJ，πJ，RJ，.，RJ（D）1m哪里• SJ=old（S）{new（s）|（男，女）|= φ}• wJ=new（w）• πJ（old（u））（p）=πJ（new（u））（p）=π（u）（p）对所有p∈ P• 对于1≤i≤m，SJ上的关系RJ是极小的，使得RJ（old（u），old（v））惠Ri（u，v）RJ（new（u），new（v））惠Ra（u，v）若a∈ BRJ（new（u），old（v））惠Rb（u，v）ifb∈/B注意，φ在新部分的每个状态下都成立。下面的示例显示了这在具体模型上的工作原理。例3.2考虑图1a中的模型（M，s），其中π（s）（p）=真，π（t）（p）=假。我们执行的操作是b学习p，即UPDATE（p，b）。这导致图1b中的模型（M，u），其中new（s）=u，old（s）=v，old（t）=w，π（u）（p）=π（v）（p）=真，π（w）（p）=假。新世界（t）从现实世界中是无法到达的，因此在图中被省略了。(In事实上，在本文的所有图表中，我们将省略不可到达的世界。我们可以看到，主体a的信念没有改变：它仍然认为它的旧世界是可能的。然而，代理人b的信念发生了变化。它现在只考虑p成立的状态u，因此b相信p。更新更新（φ，B）基于公式φ和一组代理B。Roorda等人。 [18]已经给出了通过使用单个学习代理的这种操作来改变的公式的特征。在这里，我们扩展了多智能体的定义。58A. Hommersom等人理论计算机科学电子笔记126（2005）53v甲乙丙Wa aua，b a，ba，b a，bs a，b tBa.（M，s）b.（M，u）图1.一、定义3.3更新函数（·）[φ，B]被称为真函数，如果（M，w）[φ，B]|= p⇔（男、女）|= p（M，w）[φ，B]|=αβ⇔（M，w）[φ，B]|= α和（M，w）[φ，B]|= β（M，w）[φ，B]|=<$α⇔（M，w）[φ，B]$α（M，w）[φ，B]|=B a α⇔（男、女）|=Ba α ifa∈/B（M，w）[φ，B]|= Bb α⇔B b（w，u）（M，u）|= φ）意味着（M，u）[φ，B]|= α） 如果b∈ B根据Roorda等人的观点，我们得到更新 （ φ ， B ）是适当的。此外，UPDATE（φ，B）由定义3.3唯一地刻画，直到初等等价，即如果（·）[φ，B]是一个真的更新函数，则（M，w）[φ，B]和UPDATE（φ，B）是初等等价的。我们收集UPDATE（φ，B）的以下性质。引理3.4(a) 对于所有的公式φ，（M，w）成立|= φUPDATE（φ，B）（M，w）|= BBφ。(b) 如果一个模型（M，w）满足Kt45性质，并且φ是客观的，那么模型更新（φ，B）（M，w）也满足Kt45性质。(c) 模型UPDATE（φ，B）（M，w））和UPDATE（φ，B）（UPDATE（φ，C）（M，w））是双向相似的。注意，在引理3.4中，aφ的范围是任意公式，包括非客观公式.然而，对于一个非客观的公式，比如说Biφ，可能会发生这样的情况：一个代理人A. Hommersom等人理论计算机科学电子笔记126（2005）5359无意中增加了公式φ所包含的客观知识。下一个例子说明了这一点。60A. Hommersom等人理论计算机科学电子笔记126（2005）53甲乙丙a，ba，b甲乙丙a，b a，bsatbua.（M，s）b.（MJ，v）图二、例3.5假设我们感兴趣的是智能体a学习公式Bbp<$Bb <$p，而不是p本身。考虑图2a中的Kripke模型（M，s），其中π（s）（p）=π（u）（p）=真，π（t）（p）=假。这个模型表明b知道p是真的。代理a不知道p或<$p，也不知道b是否知道p。如果我们应用更新操作的定义，它会导致图2b中的模型（M，v），其中π（v）（p）=π（s）（p）=π（u）（p）=true和π（t）（p）=false。它变成这样的原因，是因为Bbp <$Bb<$p成立的唯一状态，是状态s。因此，所有其他状态都没有从新点v可到达的对应新状态。图2b说明了a已经学习了Bbp<$Bb <$p，但也说明了a已经学习了p本身。在下一小节中，我们将定义一个侧效应函数，使得a在上述情况下将学习其他函数，但本身不学习任何客观公式。3.2侧射在例3.5中，更新代理a的Bbp <$Bb <$p失败的主要原因是它实际上删除了错误的箭头。更新操作删除a的箭头以获得满足更新公式的状态。这不是我们的本意我们希望a保持它认为可能的所有状态，但同时我们希望更新a的所有可能状态，使得公式Bbp<$Bb <$p在这些状态下成立。此外，我们不想改变其他代理人的知识。在本节中，我们定义了实现这些要求的功能。一个技术障碍是状态可以在代理之间共享。很明显，如果我们改变一个状态的意图是改变一个主体的信念，那么其他认为这种状态可能的主体的信念也会改变。因此，首先要做的是将学习代理的状态与不学习的代理的状态分开。这个过程将被称为展开。 函数newB和orig是新的和旧的，但函数orig只定义了S一B不Buv一A. Hommersom等人理论计算机科学电子笔记126（2005）5361我我我在模型中，即真实的世界定义3.6给定一个模型（M，w），其中M= S，π，R1，.，Rm，一个代理集合A的分割X，我们定义运算展开X（M，w）=（SJ，πJ，RJ，.， Rj，wJ），其中1m• SJ=（B∈XnewB（S））-numerorig（w）• wJ=orig（w）• πJ（newB（v））（p）=π（v）（p），πJ（wJ）（p）=true对所有p∈P，B ∈ X• SJ上关系RJ，1≤i≤m，是极小的，使得RJ（newB（u），newC（v））惠Ri（u，v）（B=C）RJ（orig（w），newB（u））惠Ri（w，u）<$i∈ B其中B、C的范围超过X。因此，对于每一组主体B，都有原始状态的副本（即，对于每个s∈S，都有新的B（s））。 这个操作确实保留了我们的Kt45属性，并且它模拟了相同的知识，这可以通过以下引理来捕获62A. Hommersom等人理论计算机科学电子笔记126（2005）53我a，b a，b a，b甲乙丙a，b a，bSJA一TJBUJASsatbusJJbJJ不uJJ甲乙丙a Ba，b a，ba.（M，s）b.（MJ，s）引理3.7图3.第三章。(a) 如果（M，w）是Kt 45模型，X是ma的一个划分，则展开X（M，w）也是KT45型号(b) 对于A的每个模型（M，w）和划分X，它认为模型（M，w）和展开X（M，w）是双相似的。例3.8考虑图3.a中的克里普克模型（M，s），其中π（s）（p）=π（u）（p）=真，π（t）（p）=假。所以，B知道P是真的，而A不知道。此外，a不知道b是否知道p。现在我们执行的操作是展开{{a} ，{b}}（M，s），这将导致图3b中的模型（MJ，s）（估值与预期一致）。所以我们把A和B的知识分开。状态s是原始状态，启动状态模型a因此，模型的上半部分代表a的知识，下半部分代表b的知识。 请注意，没有状态是共享的，特别是因为模型的点不是可反射的。接下来，我们给出一些预备性的定义，这些定义引出定义3.14中的边射运算的概念。首先，我们定义子模型的概念。定义3.9模型M = S，π，R1，.， Rm是M j 的子模型=SJ，πJ，RJ，.，RJ<$，记作M±MJ，i <$S<$SJ，π（s）（p）=πJ（s）（p），1m所有的s∈S，p∈ P和Ri<$RJ。接下来，我们构建一个子模型，它代表了代理a的知识。定义3.10给定一个模型（M，w）=（πS，π，R1，.， Rmj，w）和A的一个部分{ {a}，B }使得（M，w）=展开{{a}，B}（MJ，wJ）使得{{a}，B}对于某个模型（MJ，wJ），M的a-子模型子a（M）为由（M J，wJ）=<$SJ，πJ，RJ，.给出， RJ其中1mA. Hommersom等人理论计算机科学电子笔记126（2005）5363我我a-子模型甲乙丙SJA一a，b a，bTJBUJASsJJbtJJuJJ甲乙丙剩余模型a Ba，b a，b见图4。a-子模型轮廓• s∈SJ惠新a（s）• πJ（newa（s））（p）=πJ（orig（s））（s）=π（s）（p）对所有p∈ P• RJ（s，t）惠Ri（s，t）≠ s，t ∈ SJ.显然，a-子模型是定义3.9意义上的子模型。剩余模型是模型的一部分，它在可访问性关系方面补充子模型。定义3.11给定一个模型（M，w）= S，π，R1，. Rm∞和一个子模型N = SJJ，πJJ，RJJ，...，RJJ ∈ M，M的剩余模型剩余N（M）关于1m到N由剩余N（M）=<$SJ，πJ，RJ，.给出，RJ在哪里1m• s∈SJ惠s∈S（u，v）∈RJ：u=sv=s• πJ（s）（p）=π（s）（p）对所有p∈ P• RJ（s，t）惠Ri（s，t）惠RJJ（s，t）我我通过使用例3 - 8的模型并应用上面的定义，我们可以看到a-submodel和restmodel的定义。参见图4。这正好对应于两个子模型的想法，代表不同的代理人的知识。现在我们想更新一些代理人的信念。为此，我们希望用一个新的模型来替换代表他们信念的子模型。为此，我们引入了替换操作。定义3.12给定一个模型N = S，π，R1，. Rm，一个模型M，一个子模型N J使得N ± N J± M，其中剩余NJ（M）=<$SJ，πJ，RJ，.，RJ我们，1m定义替换NJ（N，M）= SJJ，πJJ，RJJ，.，RJJ在哪里1m• s∈SJJ惠s∈ Ss ∈SJ• πJJ（s）（p）=π（s）（p）fors∈SJJ for allp∈ P64A. Hommersom等人理论计算机科学电子笔记126（2005）53我B甲乙丙SJA一甲乙丙TJASsJJbtJJuJJ甲乙丙a Ba，b a，b图五、（MJJ，s）• RJJ（s，t）惠（s，t）∈Ri惠（s，t）∈RJ.我我我们的想法是，一旦信念被完全分离，我们不仅可以安全地改变某个代理的信念，而且还可以保持Kt45属性。特别地，我们局部地改变代理a的知识，例如，关于另一个代理B关于一个提议P的不确定性。下面的操作ATOMSPLIT（p，b）删除了对p有不同赋值的状态之间的b的箭头。定义3.13给定模型M = S，π，R1，. 在这里，我们定义一个函数，ATOMSPLIT（p，b）（M）= ΣSJ，πJ，RJ，.，RJ具体如下：1m• s∈SJ惠s∈S• πJ（s）（p）=π（s）（p）对所有p∈ P• RJ（s，t）惠Ri（s，t）（i b）• RJ（s，t）惠Rb（s，t）<$π（s）（p）= π（t）（p）.最后，我们可以定义将这些东西联系在一起的实际边效应函数。定义3.14对于模型（M，w），put（MJ，wJ）=UNFOLD{{a}，A\{a}}（M，w）且N=SUBa（MJ）。模型副效应（p，a，b）（M，w），即学习b已知p的副效应，由下式给出：副作用（p，a，b）（M，w）=（替换N（原子分裂p，b（N），M J），wJ）。例3.15我们继续例3.8。对于M的a-子模型，我们现在应用原子分裂p，b，这导致图5中的模型（MJJ，s）。 的箭头（tJ，uJ）消失了，因为π（tJ）（p）π（uJ）（p）。 因此，uJ不是从现实世界中可以到达，并且可以被丢弃。 注意到一张相信Bbp<$Bb<$p，而a对p本身一无所知。我们有以下结果。A. Hommersom等人理论计算机科学电子笔记126（2005）5365引理3.16(a) 如果（M，w）是Kt45模型，则副作用（p，a，b）（M，w）也是Kt45模型。(b) 给定一个模型（M，w），主体a，b，c，d，两个命题p，q∈ P，它认为，副作用（p，c，d）（副作用（q，a，b）（M，w））和是双向相似的。副作用（q，a，b）（副作用（p，c，d）（M，w））(c) 给定一个模型（M，w），主体a，b，c，命题p∈ P和目标公式φ，认为模型副作用（p，c，d）（更新（φ，a）（M，w））和是双向相似的。UPDATE（φ，a）（副作用（p，c，d）（M，w））接下来，我们考虑如何通过侧射函数改变公式我们将通过提出一些在所得模型中成立的有趣公式来部分回答这个问题。我们将研究多组代理，而不是单个代理：(i) 学习其他智能体的智能体组，范围由a表示;(ii) 被学习的代理的组，由b排列;(iii) 其他药剂，由C.很明显，a型智能体是唯一会学习的智能体。其他智能体认为他们的旧世界是可能的;他们的信念没有改变。考虑到这一点，我们提出了侧射函数的一些性质。引理3.17设a，b和c是三个不同的施事。 给定一个模型（M，w）模型（MJ，WJ）=副作用（p，a，b）（M，w），它认为(a) （MJ，wJ）|= Ba（Bbp <$B b<$p）(b) （MJ，wJ）|= Baφ i（M，w）|= Baφ （对于φ物镜）(c) （MJ，wJ）|= BaCabc（Bbp <$B b<$p）(d) （MJ，wJ）|= Biφ i（M，w）|对于i/= a，66A. Hommersom等人理论计算机科学电子笔记126（2005）53我上述引理的（a）部分陈述了主体a获得派生知识代理人B。（b）部分指出，没有对象知识被学习。部分（c）短语，代理a认为其余的代理是聪明的。最后，部分（d）捕捉到其他代理不学习。性质（c）是a关于其他代理人的合理假设，开放通信网络的背景（如第4和第5节的设置）。如果一个代理人相信另一个代理人知道p的值，那么可以合理地假设另一个代理人也会相信同样的事情。另一方面，常识可能过于强大而无法假设。我们展示了如何通过区分被认为具有平等学习设施的代理和不具有平等学习设施的代理来改进上述方法。也就是说，我们将前一组其他智能体分为通常学习的智能体和将保持无知的智能体我们通过将a对其他智能体的信念与原始（未修改的）状态联系起来来表示这一点我们现在区分四种不同类型的代理人组。(i) 学习其他代理的代理组A，由a排列;(ii) 被学习的代理B组，由b排列;(iii) C组代理人，其中代理人a认为他们通常已经了解了b组代理人，范围为c;(iv) A中的智能体认为他们对其中的智能体一无所知的智能体组D，其范围为d。为了表示的简单性，我们假设在每个组中恰好存在1个代理，即A={a，b，c，d}。我们定义了新的侧边检验操作0-展开（其中0表示零知识）。注意，0-展开操作取决于代理A的特定partinioning。由于操作的侧效应将取决于展开操作，侧效应函数也相对于代理集合的某些选择的划分而被采用定义3.18给定一个模型（M，w），使得M =S，π，Ra，.， Rd，我们定义一个函数0-UNFOLD（M，w）=（SJ，πJ，RJ，.， Rj，wJ），其中一个d• SJ=newa（S）newbcd（S）orig（w）• wJ=orig（w）• 对于所有p∈ P，B ∈ {{a}，{bcd}}，πJ（newB（v））（p）=π（v）（p）和πJ（orig（w））（p）=π（w）（p• RJ在SJ上，i∈ {a，b，c，d}，是极小的，使得A. Hommersom等人理论计算机科学电子笔记126（2005）5367D我我一我一我RJ（newa（u），newbcd（v））惠Rd（u，v）RJ（newa（u），newa（v））惠Ri（u，v）（i/=d）RJ（newbcd（u），newbcd（v））惠Ri（u，v）RJ（orig（w），newa（v））惠Ra（w，v）RJ（orig（w），newbcd（v））惠Ri（w，v）<$i=b，c，d因此，我们不是将代理a的知识与其他代理完全分离，而是将代理a关于d的知识与其他代理共享。由于其他智能体没有学到任何东西，所以a没有获得关于d的知识。我们提出一个类似于引理3.7的引理。引理3.19(a) 如果（M，w）是Kt 45模型，那么0-UNFOLD（M，w）也是。(b) 对于每个模型（M，w），它认为模型 （M，w）和0-UNFOLD（M，w）是双相似的。由于上述定义3.18中对RJ（orig（w），newB（v））的情况区分，它认为a关于b的知识与其他主体关于b或b本身的知识无关。所以，和前面一样，我们可以从a的信念中“切出”包含b箭头的子模型：定义3.20给定一个模型（MJ，wJ）=<$SJ，πJ，RJ，.，RJ，使得一个d（MJ，wJ）=0-UNFOLD（M，w），对于某些（M，w），定义B-SUB（MJ）= SJJ，πJJ，RJJ，.，Rjj一个d哪里•SJ={newa（s）|s ∈ S}• πJJ（s）（p）惠π（s）（p），对所有p∈ P• RJJ（s，t）惠RJ（s，t），其中s，t∈SJJB b• RJJ=（i/= b）。操作0-副作用p则由下式给出：0-副作用p（M，w）=（替换N（ATOMSPLIT（p，b）（N），MJ），WJ）其中N = b-sub（MJ）.同样，操作尊重Kt45特性。引理3.21如果（M，w）是Kt 45-模型，则模型也是0-副作用p（M，w）。68A. Hommersom等人理论计算机科学电子笔记126（2005）53a，b，ca，b，c素八sJtJa，b，c，da，b，c，d a，b，c，daad sdCJJb，c，dJJ JJsa，ctbus t ua、c、ba，b，c，d a，b，c，d a，b，c，da.（M，s）b.（MJ，s）图六、类似于引理3.16和引理3.17，我们有以下结果。引理3.22(a) 如果（M，w）是Kt 45-模型，则0-副作用p（M，w）也是.(b) 给定一个模型（M，w）和模型（MJ，wJ）=0-副作用p（M，w），它认为，(i) （MJ，wJ）|= Ba（Bbp <$B b<$p）(ii) （MJ，wJ）|= Baφi（M，w）|= Baφ（对于φ物镜）(iii) （MJ，wJ）|= BaCabc（Bbp <$B b<$p）(iv) （MJ，wJ）|= Biφ i（M，w）|= Biφ for i/= a(v) （MJ，wJ）|= BaBdφ i（M，w）|= BaBdφ第（i）到（iv）部分与引理3.17给出的性质相比较。第（v）部分指出，代理人a关于代理人d的知识没有改变，完全按照预期。例3.23回想例3.8中的模型（M，s）（图3.a）。我们现在在图6.a中展示这个模型，其中有四个代理{a，b，c，d}，使得π（s）（p）=π（u）（p）=真，π（t）（p）=假。现在，我们应用0-副作用p（M，w），并从图6.b中获得模型（MJ，s），使得π（s）（p）=π（sJ）（p）=π（sJJ）（p）=π（uJJ）（p）=真，π（tJ）（p）=π（tJJ）（p）=假。注意，在后一个模型中，与引理3.22b的（v）条一致，a仍然和以前一样知道d4安全协议的逻辑语言在这一节中，我们将利用上一节的思想，用逻辑语言来推理安全协议。扩展和副作用操作用于其语义.该语言的用法说明为A. Hommersom等人理论计算机科学电子笔记126（2005）5369SRA三次通过协议的情况。我们描述了协议的各个步骤如何改变所涉及的代理的初始知识以及最终获得的Kripke结构。定义4.1确定一组命题P，其范围为p，和一组m个元素的主体A，其范围为a。语言LC由下式给出：φ：：= p| ¬φ|φ1∧φ2|Biφ|[σ] φσ：：= Priv（i→j，p）|Pub（i，p）|σ; σJσ符号表示一个（可能是合成的）通信动作。动作Priv（i→j，p）是从i到j的私有或对等消息p;动作Pub（i，p）意味着i关于p的公开声明或广播。在后者中，网络上的每个代理都学习p，而在前者中，只有j学习p。括号运算符[σ]φ的解释是，在执行通信操作后，φ保持不变。LC中的下标指的是一组所谓的过渡规则C。转换规则捕获更新，即更新和副作用，解释构造Priv（i→j，p）和Pub（i，p）所必需的。转换规则强制保持命题之间的一致性。例如，如果代理相信消息m的值是[m]并且拥有密钥k（a），则它必须相信m的加密Ek（a）（m）的值具有与[m]对应的值。一个转移规则有Bip<$β或Hip<$β的形式。Bip和Hip是条件，分别表示代理i必须相信p或p已被传递给代理i。转换规则的主体β是动作序列α1;. ;αn.行动有两种形式，即LBp和Si，jp。这里，动作LBp表示p是在集合B中的代理之间学习的，并且对应于信念更新，而动作Sa，bp表示代理a已经学习到代理b现在知道p的副效应。例如，当代理a和b共享密钥k并且a向b发送消息{x}k时，我们将具有转换规则Bb{x}k<$Lab{x}k。Hipβ转换规则的典型应用 在上述情况下，代理a向代理b发送消息x，代理b返回消息{x}k。 由于它是共享的，{x}k本身，所以{x}k的传递并没有教a任何关于这个值的东西。但是，由于它必须来自b，代理a确实知道b有共享密钥，并向a认证b。在这种情况下，转换规则是Ha{x}k<$Sa，bk，说明代理a在观察{x}k时，了解到代理b知道70A. Hommersom等人理论计算机科学电子笔记126（2005）53关键字k的正确值。在下一个定义中提供的语言LC的语义遵循[8，10]定义4.2设C是一组转移规则。对于σ∈ LC，关于A在P上的模型的关系[[σ]]由下式给出：• （M，w）[[Priv（i→j，p）]]（MJ，wJ）优惠（M，w）|= Bip（EXPANDp，j（M，w）dp（M J，wJ））（M，w）[[Pub（i，p）]]（MJ，wJ）优惠（M，w）|= Bip（EXPANDp，A（M，w）dp（M J，wJ））（M，w）[[σ;σJ]]（MJ，wJ）对于某个模型（MJJ，wJJ），惠（M，w）[[σ]]（MJJ，wJJ）[[σJ]]（MJ，wJ）• （M，w）dp（MJ，wJ）若（x<$β）∈Mod（M，w，p）则对于某个（M jj，wJJ），（M，w）<$β<$（MJJ，wJJ）dp（MJ，wJ）else（M，w）=（MJ，wJ）• （M，w）（MJ，wJ）惠（M，w）=（MJ，wJ）（M，w）<$LBp;β<$（MJ，wJ）惠展开（p，B）（M，w）<$β<$（MJ，wJ）（M，w）<$Si，jp;β<$（MJ，wJ）惠副作用（p，i，j）（M，w）<$β<$（MJ，wJ）• （男、女）|= p惠π（w）（p）= true（M，w）|=<$φ惠（M，w）$φ（男、女）|= φ（M，w）|= φ和（M，w）|=A. Hommersom等人理论计算机科学电子笔记126（2005）5371（男、女）|= Biφ（M，v）|= φ对于所有v使得wRiv（男、女）|=[σ] φ f（M J，wJ）|= φ if（M，w）[[σ]]（M J，wJ）72A. Hommersom等人理论计算机科学电子笔记126（2005）53我• Mod（M，w，p）={Bip ∈ C|（M，w）<$β<$（M J，wJ），（M J，wJ）|= φ Participate（M，w）|= φ，（M，w）|= Bip}{Hip ∈ C|（M，w）<$β<$（M J，wJ），（MJ，wJ）|= φ参与（男、女）|= φ}操作dp在执行通信动作之后应用多个转换规则。对于Bipβ类型的转移规则，检查前提条件Bip是否成立。选择Mod（M，w）以这样的方式组织，即没有过渡规则被反复应用。因此，d的递归定义是明确的，因为如果没有新的转换规则可以应用，它就会停止。 在在Mod的定义中，检查代理人的信念是否在转移规则下发生变化，以防止dp的无限重写链。请注意，由于上一节的结果，应用这些转换规则的顺序并不重要。5SRA三次通过协议在这一节中，我们将讨论上面开发的机制如何适用于一个具体的例子。为此，为了使模型保持在合理的大小范围内，我们采用了两个有用的技巧。第一个是忽视任何代理人都不知道的命题。因此，如果一个命题不是模型的一部分，那么解释就是没有代理人对它有任何知识，我们接下来必须指定的是我们如何将该命题添加到模型中。我们通过制作原始状态的两个副本来实现这一点。其中一个我们指定为“积极”，另一个为“消极”。在肯定的状态下，命题将为真，而在否定的状态下，命题将为假。定义5.1给定一个模型（M，w）= S，π，R1，. Rmm m e we define the func-对加法运算p，使得（M J，wJ）=加法运算p（M，w）= πSJ，πJ，RJ，.，Rj1m哪里• SJ=pos（S）负向（S）• πJ（pos（s））（q）= ifp =q thentrue elseπ（s）（q）• πJ（neg（s））（q）= ifp =q thenfalse elseπ（s）（q）• Ri（s，t），α，β=pos，neg• wJ=pos（w）我们有以下财产。
我的内容管理
展开
