Ad-Hoc网络路由协议静态分析与安全属性验证

理论计算机科学电子笔记142（2006）195-213www.elsevier.com/locate/entcsAd-Hoc网络的形式化安全Sebastian Nanz1，2和Chris Hankin3英国伦敦帝国理工学院计算机系摘要在ad-hoc网络中，自治无线节点可以通过为彼此转发消息来进行通信对于这种设置中的路由协议，众所周知，恶意节点可以通过不根据规范进行行为来执行虽然路由协议的安全版本正在开发中，但很少有类似于传统安全协议领域中用于保密和认证的开发来正式化该场景。我们提出了一个广播过程演算适合描述的行为，需要一个本地内存组件的每个节点的协议。通过为消息的来源添加注释，我们能够在此上下文中正式定义一个重要的安全属性，称为存储授权。此外，我们描述了一个静态分析，检测违反此属性。对于AODV协议的模型在我们的演算中，我们可以推断出，攻击者可能会在某些网络中引入路由环路。关键词：协议分析，基于语言的安全，ad-hoc网络1介绍Ad-hoc网络是一种无线通信模式，它允许移动节点在不需要固定基础设施或集中控制组件的情况下交换消息。相反，它们通过以多跳方式转发数据来专门设计的路由协议试图以资源有效的方式确定这种行为1部分由德国学术交流服务（DAAD Doktorandensti- pendium）提供支持2电子邮件：nanz@doc.ic.ac.uk3电子邮件地址：clh@doc.ic.ac.uk1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.10.029196S. 南斯角Hankin/Electronic Notes in Theoretical Computer Science 142（2006）195直到最近，随着医疗保健部门、军事通信和其他地方的关键应用的出现，研究人员开始通过描述攻击和非正式地讨论安全要求来质疑这些路由协议的安全性[5，4]。考虑到对网络中所有节点相关的安全路由信息的需要，这些要求与经典的“点对点”安全属性（如保密和认证）非常不同，这并不奇怪，这些安全属性在密码协议领域已经正式研究了很长时间。然而，就我们所知，还没有尝试将特设网络环境在早期的工作[6]中，我们已经展示了一种在CBS过程演算[9]的变体中对ad-hoc网络的路由行为建模的方法，并开发了网络中消息流的静态分析。在这里，我们建立在这项工作的基础上，以正式确定ad-hoc网络的安全属性，在[4]中提到，我们称之为存储授权：存储有关某些节点的路由信息应该由这些节点本身授权。为了这样做，我们扩展了我们的演算与元组存储组件，私有的每一个节点，和行动的存储和检索元组。此外，我们引入注释来跟踪广播消息的来源。我们对Ad-hoc按需距离矢量（AODV）路由协议的关键片段进行了建模[8]，并表明专门设计的静态分析可以记录攻击者存在时违反商店授权属性的行为。对分析结果的解释表明，在某些条件下，可以执行路由环路攻击[5]，这会导致数据包在一个循环中遍历网络，从而耗尽网络的功率和带宽资源。为此，我们的攻击者模型只需要能够窃听网络的所有通信并伪造路由消息。本文的其余部分的结构如下：在第2节中，我们提出了CBS的变体，我们正在使用的ad-hoc网络中的路由行为描述它包括每个节点的类似存储的组件和消息来源的注释操作语义采用的注释，以防止在网络中的节点试图违反存储授权属性的派生在第3节中，我们回顾了商店授权的概念，开发了一个控制流程分析，该分析计算了违反此属性的安全近似值，并提出了一个简单的攻击者模型。在第4节中，我们描述了AODV协议的操作和我们的模型。我们应用我们的分析来找出攻击者可以执行的所有属性侵犯，并讨论这一发现对协议安全性的影响S. 南斯角Hankin/Electronic Notes in Theoretical Computer Science 142（2006）195197我2微积分在[6]中，我们提出了一个过程演算CBS [9]的变体，它使我们能够对ad-hoc网络的源路由协议的行为进行建模。演算的核心思想是通过让节点丢弃不在广播节点传输范围内的消息来表达多跳消息传递决定这种行为的网络拓扑在所谓的分配环境α中被指定。源路由协议的特征在于路由是作为节点名称列表的发送消息的一部分。距离矢量协议，我们要在这里研究，要求节点本地存储到某个目的地节点的下一跳。为了能够表达这种行为，我们扩展了我们的演算与存储类似的组件。这可以与协调语言（如KLAIM[2]）中的元组空间的思想进行比较，但是重要的区别是，商店只能在本地访问。这似乎更适合于必须在消息传输之间执行某些私有计算和存储操作的通信节点的上下文中对于安全分析，它使我们能够清楚地区分通信窃听者和捕获节点并试图直接访问存储的攻击者之间的2.1语法演算包括三个语法类别：项E、过程P和网络N，它们在表1中定义。项可以是变量x∈ X、名称n∈ N或位置l∈ L。 我们选择将位置添加到术语集合中，同时它们也用于区分节点，因为我们希望能够在消息组件中显式地声明消息的来源。像往常一样，我们将术语与此同时，例如， E代表E1， . . ，Ekfor somek. 我们一起来吧|E|对于列表中的值E，并且E=EJ表示s|E|为|埃吉|=k对于somek，并且E i= EJ，其中i = 1，.， K.流程是多元形式的，并包含了消息组件的术语匹配，如微积分LYSA[3]。从语法上讲，这是由元组表示的：在元组之前的术语必须等于消息或元组的第一个组件，这提供了一种强大的方法来区分不同格式的消息和元组。此外，我们还添加了术语来源的注释，这些注释写在方括号中。这背后的直觉是，某种因果链的发起者仍然可见。中间节点只对消息的接收做出反应，将复制原始注释并将其作为注释198S. 南斯角Hankin/Electronic Notes in Theoretical Computer Science 142（2006）195σE：：=x变量，x∈ X| nname, n ∈ N| llocation, l ∈ LP：：= 0零|EP发送|（E<$;x<$）[x] ？Preceive|E|（E;x）↑P1：P2检索ve|如果E=EJ则P1否则P2如果| Adefinition|P1|P2进程并行组合N：：=P：l，α节点|网络的N1<$N2表1微积分的基本原理造成的任何行为我们区分以下进程：0表示终止进程。 这是一个混乱的结局，它是由一个小女孩[E] 决 定 的 ！ P，其中E是消息，E是评估位置的注释项。的行动（E<$;x<$）[x] ？P表示接收混乱：E必须与第一个如果注释项E是注释项，则注释项S将被绑定到X;注释项E将绑定到X。元组E的存储由启动器E[E]、E[J]）↓P表示，其中启动器E位于授权启动器的列表E [j]中，其值为一个文件列表。一个例子是用（E_n;x_n）↑P_1：P_2从数据库中检索到一个数据组，如果您不知道如何更新组件，则会发送电子邮件boundtox. 取决于是否存在与P1或P2一致的映射元组。如果表达式常数A可以表示过程的定义 进程也可以并行执行，写成P1|P2.S. 南斯角Hankin/Electronic Notes in Theoretical Computer Science 142（2006）195199σσJσσσσσ2σ网络由定位过程P：1，α的并行组合N1<$N2组成。 位置l对于被定位的进程是唯一的，并且使得能够区分不同的节点。分配环境α：L→[0，1]为我们提供了节点的连通性信息，从而提供了网络拓扑：例如，由P j表示的消息：lJ，αJ由P节点接收：1，α为表示为αJ（l）。σ表示节点的本地元组存储。 当α或σ在某种情况下不必要时，我们可以去掉它们2.2操作语义通过两个转换M网络关系第一个N1−→pN2描述了网络N1到网络N2的概率为p，消息m.就像在哥伦比亚广播公司，是从集合{！、、怎么样？，：}，以及发送、接收和丢失消息m的动作由m！表示，m？， 和m：MESSAGES被写为<$E[E]lJ，αJ，其中E是一个无变量项列表，E是注释项，l和α表示位置和分配直接发送者的环境。第二个关系N1−→N2transs形成了一个网络，只适用于局部的、非交互式的计算。这两个关系并不相互依赖，但是这种指定方式确保了在推导中，所有节点在下一次消息交换之前都完成了本地计算M第一个跃迁关系−→p的规则在表2中给出。规则nil表示nil过程0：l，α静默地丢弃任何消息，可能性1. Rule ssend1andsend2de scri bethebeh avourofE[E] ！ P：1，α。这样的节点以概率1静默地丢弃传入消息，如规则发送2.当广播消息时，它以概率1演变为P：l，α，在规则send1中指定。此外，该消息将携带注释E。有三个规则用于接收的合成器，（E;x）[x] ？ P：1，α。rec1和rec2描述了第一个消息组件匹配用x表示，即，E=EJ 和|埃吉|为|X轴|，对于一个竞争对手来说：1 2JJ在规则c1中，没有一个选择接收一个整数E j，Ej[E]l，α与1 2概率yαJ（l），其中x的变量是与他们的各组成部分，E∈J;al so，符号项E与x相结合。另一方面，节点也可以以概率1-αJ（l）丢弃消息，这在规则rec2中描述。规则rec3表示，如果消息内容与预期消息不匹配，即第一个消息组件不匹配或消息没有正确的长度，则节点以概率1丢弃消息。定义A：l，α可以简单地扩展，如规则def所示。 规则第1款和200S. 南斯角Hankin/Electronic Notes in Theoretical Computer Science 142（2006）195σσσσσσσσ1 2Jnil0：l，α−m→：10：l，α发送1m=E[E]l，αEP：l，α−m→！1P：l，αsend d2 E[E] ！ P：l，α−m→： E[E] ！P：l，α1m= EJ，EJ[lJJ]lJ，αJE= EJ|埃吉|为|X轴|11 2 1 2（E<$;x<$）[x] ？ P：l，α−m→？JP[E<$ J/x<$，lJJ/x]：l，ασα（l）2σm= EJ，EJ[lJJ]lJ，αJE= EJ|埃吉|为|X轴|2016年10月21日（E<$;x<$）[x] ？P：l，α−m→：1−αJ（l）（E<$;x<$）[x] ？P：l，αm= EJ，EJ[lJJ]lJ，αJE/= Ej|埃吉|/= |X轴|2016年12月12日（E<$;x<$）[x] ？ P：l，α−m→：（E<$;x<$）[x] ？P：l，α1def一l，αmJl，αdef=P P：σ−→qP：σA：l，αmJl，ασ−→qP：σP：l，αm1Jl，αl，αm2Jl，αpar11σ−−→q1P1：σP2：σ−−→q2P2：σ（）1◦2⊥P | P: l,αJ Jl，α1 2σ−→q1·q2P1|P2：σM1Nm2JParr1−−→q1N1N2−−→q2N212/=N Nm（12）NJNJ1 2−−−−−→q1·q212表2操作语义学1parr用于网络的并行组合，描述了广播消息如何传播到所有进程。他们使用代数的组成1，2∈ {！、、怎么样？，：}，其在表2中示出。 像在原始CBS中一样，这些规则确保网络中的每个节点都决定接收或丢弃某个消息，并且不尝试同时广播两个消息，因为1/2/= 1/2。当组件的跃迁具有概率q 1和q 2时，跃迁的概率为q1·q2。在表3中，我们讨论了第二个过渡r −→的规则。Theruleσσ◦！ ？ ：！⊥ ！！？！ ？ ？：！ ？ ：S. 南斯角Hankin/Electronic Notes in Theoretical Computer Science 142（2006）195201σ21σ店E∈EE[E]E<$E<$ J，E<$ J<$[lJ]∈σσE=EJσJ|为|X轴|x˜|11 2 1 2（E;x）↑P1：P2：l，α−→P1[EJ/x]：l，ασ2σ$<$E<$ J，E<$ J<$[lJ] ∈σ。 E=Ej|埃吉|为|X轴|2012年12月12日（E;x）↑P1：P2：l，α−→P2：l，α如果1σ σE=EJ如果E=EJ，则n个P1elseP2：l，α−→P1：l，α如果2σ σE EJ如果E=EJ，则n个P1elseP2：l，α−→P2：l，ασ σP1：l，α−→PJ：l，αP2：l，α−→PJ：l，ασ标准杆2杆1σ1σ2σ2P1|P2：l，α−→PJ|PJ：l，ασ1 2σ1∪σ 2表3操作语义学2如果在授权发起者列表E j中找到发起者E，则s to re将s aupleEj添加到i本地序列σ，其中E∈E J。对于元数据val（E;x）^P1：P2：l，αdistinggu的两个规则是这样的：其中某个元组包含或不包含在本地存储中。在规则ret1中，如果元组的第一个组件匹配并且元组具有正确的长度，其余的电子邮件元组组成为EJg etboundtoxppP1.特别注意，在两个或更多匹配元组的情况下，是所选元组的非确定性选择;在具体应用中，可以通过E J的选择来确定。 如果没有找到匹配的元组，则过程P2将继续。if表达式的两个规则：ifE =EJ thenP1 elseP2：l，α选择P1或P2作为连续过程，取决于等式E=EJ。表达式是为了清楚起见而包括的，尽管它们可能是用检索语句最后，给出了并行组合P1的语义|P2对Ward来说是一个很好的选择。该转换规则旨在被重新定义，即， P−→P，这样只有一个分支的变化是可能的。202S. 南斯角Hankin/Electronic Notes in Theoretical Computer Science 142（2006）195σσ3安全分析分析的目标是在可能窃听和伪造任何消息的攻击者存在的情况下安全地近似违反注释演算的存储授权属性。它是由一个流程逻辑，一种方法来控制流程分析，其重点是指定，而不是计算的分析结果。然后，我们的实现是通过将一阶逻辑的规则转换为一阶逻辑的片段的项来给出的3.1商店授权表3中的规则存储指出，演算中的推导被卡住，如果E∈/E <$j，则anode<$E<$[E]<$E<$J）↓P：l，α。将所有数据记录到本地化Lj，其表示导致存储操作的因果链的发起者，例如，已经发送关于某个路由信息的更新的另一节点。因此，E j对LJ的位置列表进行了评估，指定授权触发存储操作的位置。存储授权属性用我们的微积分术语表示，即“存储操作的发起者l j（存储授权[ l j ]<$L（j）↓ P m u s t b es p i n e d i n ti本操作的授权声明”。该安全属性的重要性可以如下所示：用于多跳路由、对等覆盖网络和其他类似应用的通信协议需要各个节点存储具有协议相关信息的数据。只要所有节点都遵循协议规范，分布式数据是一致的，或者可能包含由于故障节点而导致的可容忍数量的不一致。然而，一旦恶意节点进入网络并随意改变分发的协议信息，就会出现问题。根据攻击者的意图，协议的工作可能受到严重限制，例如通过拒绝网络部分的服务。作为一个例子，我们将在第4.2节中介绍一个对ad-hoc网络的资源消耗攻击，并展示列表如何在这种情况下，授权人的职责可能会受到限制，以满足要求。3.2控制流分析我们的分析是通过判断ρ、κ、σ、ερ：l来实现的，使用了以下定义的某些类型的分析组件。这里，ρ是所有局部变量项的集合，σ是所有局部变量项的集合，V表示无变量项的集合，而星号表示S. 南斯角Hankin/Electronic Notes in Theoretical Computer Science 142（2006）1952032σ有限列表。为了关注原始注释，我们不在这里描述分配环境的分析，并参考[6]。ρl：X →N（V × L）局部变量环境ρl：X→X（L）局部注释变量κV× L×Lnt工作env铁σlV× Llocalstoreenvironmentε误差分量分量的类型揭示了原点分析的核心思想：值V∈ V与位置l∈ L配对，以表示l起源V. F或example，如果anode（E;x∈）[x] ？P：l，α接收到一个混乱的EJ，Ej[lJlσ12] ，即，源自lJ，分析将计算变量环境ρl，l（Vi，LJ）∈ρl（xi），或entsEi∈E J上的所有esVi处和尊重-i vexi∈x<$。 但是，当我的年龄被传递到网络w或k上时，它将计算<$VJ，Vj <$[lJ]lJ∈κ，即。他估计我的年龄是有限的，或者说，1 2发送者LJ和直接发送者LJ J将被记录在网络环境是的从逻辑上讲，存储容量存储元组和发起人。 注释变量环境注释变量，即始发者位置。我觉得这是一个小问题错误组件记录违反商店授权属性的情况如果一个任意的实验对E_（？）_j的e时间s L_（？）_j，引入一个随机变量E_（？）_（？）[ l_J]、E_（？）_J）↓P：l，α和l_J∈/L_（？）_j，则结果将使得（l_J，l，L_（？）_J，V_（？） ）∈ε，即. LJ可能伪装成与lj有关的权威人士之一，在L的商店里。3.2.1定义实际分析见表4 表4包含了术语的两个辅助判断的定义。ρlV×L，其中包含对（V，lJ），其中V是E可以计算的值，lJ是这个值的起源。在常量项的情况下，即名称和位置，每个位置都被假设为始发者。对于一个变量x，估计值包含变量绑定和记录在ρl（x）中的发起者。为了估计注释，需要第二个判断标准E：当估计发起人位置时，需要对注释进行估计。注意，对于表5和表6，（E，l）∈，并且类似的平均值（E1，l）∈1· · ·ε（Ek，l）∈εk，假设Ek表示E1， .. . ，Ekfor somek. Rulesnil和阿利帕尔都很直接规则说明，网络环境JJ204S. 南斯角Hankin/Electronic Notes in Theoretical Computer Science 142（2006）195σσ2σ1LLρl（x）lJ∈ L. （n，lJ）∈NlJ∈ L. （lJJ，lJ）∈特拉瓦尔ρx：用户名中文（简体）pllJJ：拉瓦瓦尔p<$l（x）pālx：什特拉洛克lJJ∈p<$llJJ：<$表4术语分析卡尼尔ρ、κ、σ、ε0：l你好中文（简体）你好 lJ∈（V<$ J，lJ）∈V<$J<$[lJ]l∈κ<$ρ，κ，σ，εP：l发送σρ，κ，σ，εE[E] ！P：l中文（简体）∀⟨V˜ J，V˜ J⟩ [lJJ] lJ∈κˆ. （VJ，lJJ）∈l/=lJ1 2 1（V<$ J，lJJ）∈ρl（x<$）<$lJJ∈ρ<$l（x）ρ，κ，σ，εP：l最大值σρ，κ，σ，ε（E;x）[x] ？P：lρ，κ，σ，εN1 ρ，κ，σ，εN2斯皮帕尔ρ，κ，σ，εN1<$N2表5工艺分析1κisupdatedwithallposblemessage sanddtheirrespectiveooriginatorand立即结束，<$V<$ J<$[lJ]l∈κ<$。 条件（V_ J，l_J）∈E_j使得l_J-起源项V_ j是从E_j的当前估计值集合中导出的。lJitself是注释项E的估计的一个元素。另一方的规则是所有的标记都是VJ，Vj [lJJlJ[12 ]中记录是的 Itischeckedthat（VJ，lJJ）∈V，即. 第一个步骤是在一个混乱的环境中完成我知道这是一个期望值，这是一个估计值。Furgent，llJS. 南斯角Hankin/Electronic Notes in Theoretical Computer Science 142（2006）195205表示发送节点不接收自己发送的消息 如果满足这些条件，则x和x的变量envi nt在ed处增加。206S. 南斯角Hankin/Electronic Notes in Theoretical Computer Science 142（2006）195σσσσσσ1σ2σ∪σ12p<$lE：<$plE：plEJ：J你好 。 lJ∈（V<$ ，lJ）∈ σ<$l<$<$V < $<$[lJ]∈σ<$l<$（lJ∈/jLJ∈J. （lJ，l，L<$ J，V< $）∈ε）ρ，κ，σ，εP：lJ公司简介σ∪⟨V⟩[l]ρ，κ，σ，εE[E]<$EJ）↓P：l中文（简体）<$$>V<$ J，V<$j <$[lJJ] ∈σ<$l。（VJ，lJJ）∈1 2 1（V<$ J，lJJ）∈ρ<$l（x<$）<$ρ，κ<$，σ<$，ε<$P1：l2σρ，κ，σ，εP2：l最大值σρ，κ，σ，ε（E;x）↑P1：P2：lρlE：ρlEJ：Jϑ∩ϑJ/=∅⇒ρ,κˆ,σˆ,ε►P1:lρ，κ，σ，εP2：l希里夫ρ，κ，σ，ε，如果E=EJ，则nP1eleseP2：l拉斯帕尔ρ，κ，σ，εP1：lρ，κ，σ，εP2：lρ，κ，σ，εP1|P2：l表6工艺分析2在表6中，规则Ruppar很简单。规则存储类似于发送：代替将消息插入到网络环境中，现在存储元组被插入到节点的本地存储器σl中，即，存储元组[lJ]∈σl。很抱歉，如果编辑器LJ不是注释L1 s t的估计值εJ的元素，则更新误差分量ε。另一方面，《规则》与《规则》相似。显然，元组现在是从本地存储中获取的，而不是从网络环境中获取的。 为了精确起见，仅在以下情况下分析延拓分支P1：当P2总是被分析时，存储检索确实可以成功这适用这类似于规则10.1.1.2中的相等检验，否则就很简单。3.2.2正确性定理3.2中的主语归约结果说明了语义正确性关于2.2节中的操作语义的流程逻辑。我们S. 南斯角Hankin/Electronic Notes in Theoretical Computer Science 142（2006）195207σσσσMBσ2首先需要一个替换引理。引理3.1（代换）如果FV（EJ）= 0，则下列陈述成立：(1) ρ l <$E：ε和（Ej，lj）∈ ρ（x）蕴含ρ l <$E [Ej/x]：ε。(2) ρ和EJ∈ρ。（3）ρ、κ、σ、εP：l（4）ρ、κ、σ、εP：l且（EJ，LJ）∈ρ（x）蕴含ρ，κ∈，σ∈，ε∈P[EJ/x]：l. 且EJ∈ρ<$（x）蕴含ρ，κ<$，σ<$，ε<$P[EJ/x]：l.通过简单的结构归纳证明。Q在定理3.2的证明中，我们必须确保只考虑有效的M推导N1−→N2，在这个意义上，用作标签的消息m确实具有被发送。 这可以通过检测消息转换与消息环境κ的关系，从而导出新的推断M系统κ<$N1−→N2如下：消息m仅在规则parr的接收分支，用于情况“1 = 2 =！";而且，规则κ<$N1−→N2，其中b∈ {？，：}得到一个新的前提m∈κ。我们可以M确保微积分中的一个导数κ<$N1−→N2符合一个判断，ρ，κ，σ，εN1b y requiringgκκ.Theorem3.2（SubjectReduction）Ifκκ以及ρ、κ、σ、εN1和κNm l1−→N2，t h enρ，κε，σεn nN2. 对于其他情况，如果σσP1：l−→P2：lJ，t∈nρ，κ∈，σ∈，ε∈P2：lJ.和ρ，κ，σ，εP1：σσ σ σM用归纳法给出了fκN1−→N2和N1−→N2的推理规则.考虑规则rec1的情况：我们从规则rec1得到，(i) m=<$E<$ J，E<$ J<$[lJJ]lJ∈κ1 2㈡E=Ej|埃吉|为|X轴|1 2此外，根据规则(iii) 中文（简体）(iv) ∀⟨V˜ J，V˜ J⟩[lJJ]lJ∈κˆ. （V<$ J，lJJ）∈ρ<$l/=lJ<$（V<$ J，lJJ）∈ρ（x<$）<$lJJ∈ρ<$（x）1 2 12l l(v) ρ，κ，σ，εP：l使用gκκ，weknowE J，Ej[lJJ]lJ∈κ与h（i）。式（ii）、（iii）和规则1 2其中，n为e，n为c，n为c，n为j，J∈L. （EJ，lJJ）∈EJ是发送1 1消息，因此是无变量的。 从微积分中可以清楚地看出，lj= LJ，并且不可能将其重新计算出来。在这里，我们有一个ve（EJ，208S. 南斯角Hankin/Electronic Notes in Theoretical Computer Science 142（2006）195lJJ）∈ρl（x<$）<$lJJ∈ρ<$l（x）withrulee（iv）. 通过应用替换引理3.1（4）和3.1（3），|埃吉|时间sto（v）给出了期望的结果ρ，κ，σ，ε，P[E，J/x，l，J/x]：l。2 2σS. 南斯角Hankin/Electronic Notes in Theoretical Computer Science 142（2006）195209不安全−→NσA规则ret1和if1可以类似地证明，而其余规则则通过假设或应用相应的推理逻辑规则和归纳假设直接证明。Q下面的定理表明，如果我们的分析，微积分中的推导不会因为违反商店授权属性而被卡住。d oesnotreport anerrorinε. 为了稳定，设N1−→N2是一个消去规则s的条件E∈E J的迭代.定理3.3如果N1不安全2 和ρ，κ，σ，εN1其中ε=ε，则N1−→N2。我们只需要考虑规则库，因为这两个推理系统在其他方面是相同的。根据不安全语义中的规则存储，我们有σJ=[E]. AsE和E是存储元组的组成部分，我们有FV（E）=且FV（E）=。因此，我将继续与我的伙伴们：ρl<$E<$：从规则中得到的结果是（E<$，E）∈<$<$. 因此，状态ntE∈/jL（E，l，L<$ J，E<$）∈ε成立。 因为eε=但tj，所以E∈J。满足了E∈E_（？）J和标准力学中规则集的条件。Q3.3攻击者模型攻击者A被简单地指定为我们的过程演算的以下项，其中A ∈N（N）是某个网络发生的事件的集合，分析ysed和xk表示变量的sak-elementlis：A=（|k∈A（;x<$k）[x] ？ 一|你好 ！A）：1A，αA这意味着A可以接收任何含有任意数量组件的消息，并以这种方式获得一些知识。然后，这在分析中表示为，对于所有混乱的重新分配，可变的e_v_m_t_p_A随着可变的绑定而增加。其他人，也许都是伪造的已经在网络中使用过的。对于这些消息，分析保持跟踪A作为始发者，因为发送被注释有1A。这遵循经典Dolev-Yao攻击者的思想，但不同之处在于不涉及密码学。这是适当的，因为我们在第4节中建模的AODV协议不使用加密原语。我们计划在未来的工作中研究协议的安全版本，然后可以像[1]中那样将密码原语添加到微积分210S. 南斯角Hankin/Electronic Notes in Theoretical Computer Science 142（2006）1954AODV协议在ad-hoc网络中，一组无线节点相互协作，以便将消息转发到发送方的直接传输范围之外的目的地。Ad-hoc按需距离矢量（AODV）路由协议[8]是一种用于这种设置的协议，其中节点仅在需要时（按需）才尝试找到到达目的地的路由。它还要求每个节点存储特定目的地的方向（下一跳）和距离（跳数）的“向量”。下面我们将描述AODV的操作，并展示如何在我们的演算中对其进行建模。然后，我们执行第3节的分析，以便在存在攻击者的情况下检测违反商店授权属性的行为。4.1AODV协议的运行和建模如果节点S（源）需要与另一个节点D（目的地）通信，而对于该节点D它没有路由信息，则S发起路由发现过程。由于协议的复杂性，我们将通过省略路由的过期时间和新鲜度信息（序列号）以及距离信息来简化描述和建模这个过程。此外，我们定义αi（l）：= 1，对于所有l∈ L和分配环境αi，即每个节点可以看到每个其他节点，并且连接图是L上的完全图。在第4.2节中，我们将详细讨论这些假设对我们的证券分析的影响。路由发现包括以下步骤：(1) S通过广播包含源、目的地和请求的转发节点的名称的路由请求rre q来发起路由发现。这是一个4元组的集合q，S，D，NJ，其中NJ是直接发送者，因此在S的情况下NJ= S。(2) 每个接收到RREq的节点N检查它本身是否是目的地即N=D。如果不是，N将存储反向路由的向量，以便能够将应答从D传播回S。 如果N接收到RREq从立即发送者NJ，因此它将存储元组NREV，S，NJ。然后，它将请求重新广播为RREq，S，D，N，将直接发送者NJ的名称替换为自己的名称。如果N=D，则节点将使用路由应答RREP进行应答，其中包含其名称（目的地）、源、应答的转发节点的名称在D从直接发送者NJ接收到rre q的情况下，它将因此发送5元组RREP，D，S，D，NJ。S. 南斯角Hankin/Electronic Notes in Theoretical Computer Science 142（2006）195211我我发送发送i=1σiP（1）=|n快来q，l i，l j，l i！Nii j=1，i/ =jP（2）=（RREq; x src，x dst，x send）[x orig]？如果li=xdst，则发送请求，发送请求！NielseREV，xsrc，xsend你好，我是问！NiP（3）=（RREP; xdst，xsrc，xsend，xaddr）[xorig]？如果li=xaddr，则（REV，xsrc;xJ）↑（FORW，xdst，xsend[xorig]<$xdst）↓如果li=xsrc，则Nielse {\displaystyle {\frac{x}{\DISPLAYSTYLE{x}{\Ni）：Ni否则NiPi=P（1）|P（2）|P（3）Nn=n我我我Pi：li，αi表7AODV协议(3) 每个接收到NRREP，D，S，NJ，NJJ的节点N检查它是否是被寻址者，即N=NJJ。 这在广播之上实现了单播，因为如果没有寻址，所有节点将丢弃消息否则，N将尝试检索S的反向路由作为元组REV，S，NJJJ。如果不正确，它将存储一个forw转发路由，以便能够传播从S到D的进一步消息。 因此，它将存储一个元组，D，N，j。如果N=S，它现在可以开始发送数据。 否则，它会重播回复如RREP，D，S，N，N JJJ。表7中所示的方案建模完全遵循该描述。 它表示n个节点的网络，其中节点通过位置l1，. ... 非正式的描述。 每个节点li尝试向所有其他节点lj在J。 作为一个盈余，我们当然有注释的起源，212S. 南斯角Hankin/Electronic Notes in Theoretical Computer Science 142（2006）195我我充分和传播例如，在P（1）中，RREq被标记为[l i]以表示关于将源11指定为该消息的发起者。 这同样适用于P（2），相应目的地的RREP否则，在接收到消息在P（2）或P（3）中，始发者被约束到xorig。当只转发我我消息，例如使用语句RREq，xsrc，xdst，li [xorig]！我，创始人仍然存在。4.2分析结果对于某个n∈N，我们分析表7中的网络Nn。在没有攻击者的情况下，所有节点都根据规范进行操作。对于i，j，k，m∈{1，.，n}，我们的分析在网络环境中准确地放置了以下消息：i。 i，j = i。格列克，kJ.RREq，li，lj，lk<$[li]lk ∈κ<$你好 i，i=j。 k，k/=1。 m，m/=k。rreP，lj，li，lk，lm ∈κˆ这证实了分析非常精确，特别适合对于起源分析：具有作为源的L1的RREQ仅具有作为发起者的L1，并且类似地对于具有Lj的RREPs。在这两种情况下，直接发送者lk在这个例子中。对存贮量σ_i的计算也有类似的精度。j.J. REV，li，lk<$[li]lk∈σ<$i。 i，j=i。 k，k/=1。f或RW，lj，lk<$[lj]lk∈Σ<$l对于反向路径REV，其被设置为将可能的路由到源i，我们有一个完整的存储器σrevj 其中hii=j是由l i发起的n个元组，并且具有与lj不同的下一跳l k。类似地，这适用于具有切换的l i和l j的角色的前向路径forw。由此，很明显，我们的分析正确地将误差分量ε计算为空集。一旦3.3节中描述的攻击者A被添加到分析中，这种情况就会改变对于攻击者的影响的一个具体例子，考虑网络N4与四个在ε中，分析将插入f（lA，l，lJ，E）的元组，其中relA（fixedd）是该attacker的位置当将更新E插入到σl中时，会出现以下问题。我们考虑攻击者伪装成l4的情况，即。lJ=l4，J我S. 南斯角Hankin/Electronic Notes in Theoretical Computer Science 142（2006）195213再看看l= l1，l2，l3的情况。为了清楚起见，我们将在表8中示出uple（E）而不是全元组（lA，l，l4，E），并且在顶行中指示在哪个位置l处插入该元组。1234表8存储攻击者由于攻击者A可以使用他能够窃听的通信中出现的名称和位置来伪造任何消息，因此A可以成功地在所有位置插入任意元组。因此，每个可能的下一跳l1，.，14示出为每个存储元组的第三分量。重要的是要注意，这些值实际上都不是假阳性：错误组件中的元组确切地表示违反属性，并且这些元组中的任何一个都可能影响协议的正常工作然而，并不是任何插入的元组都具有相同的效果，通常成功的攻击者需要一些策略。例如，如果A在位置li（i=1， 2， 3）处插入来自表8的行1的相应元组，则目的地l 4的“下一跳”将被指定为l i本身：可能的是，该不一致性将由相应节点通过不包括在我们的建模中的如果A选择插入元组，第4行：节点将仅尝试将消息转发到它们期望在其邻域中的节点14如果l4确实在邻域内，则协议的功能不受限制。否则，节点将仅假设l4移动出它们的传输范围并且开始路由修复过程。另一方面，选择线路2或线路3将被证明是对网络的强大攻击：在这两种情况下，转发链路形成一个循环，例如在线路2中，l1将转发到l2，l2转发到l3，l3转发到l1。因此，如果A发送消息对于系统中的L4，只要节点最后一个或者节点由于其它原因离开网络。 这个资源消费攻击被称为路由环路[5]。然而，关于AODV协议安全性的定义性结论需要看一下我们在第4节中的假设。省略到期时间信息似乎是有效的，因为它只涉及反向路由。同样，L1L2L3（FORW，l4，l1）（前，l4，l2）（前，l4，l3）（前，l4，l2）（前，l4，l3）（FORW，l4，l1）（前，l4，（FORW，（前，l4，214S. 南斯角Hankin/Electronic Notes in Theoretical Computer Science 142（2006）195攻击者可以随意选择距离信息，并且因此总是通告需要较少跳数的路由，从而被诚实节点接受。相比之下，序列号是在[8]中证明AODV协议的无环属性时使用的关键事实，并且在我们的模型中省略它们似乎有问题。然而，我们可以参考[4]，其中描述了将节点的序列号设置为任何期望值的攻击。我们的最后一个假设涉及网络的拓扑结构。我们的框架可以表达细粒度的拓扑信息，如[6]所示，但在我们的模型中，我们选择只考虑全连通图。这个决定来自以下观察：如果我们为n个节点的场景指定一个特定的拓扑，结果将限于此选择。如果我们推导出某个攻击在网络中是不可能的，那么同样的攻击在另一个拓扑中仍然是可能的。通过采取完整的图，我们执行一个安全的分析，在这个意义上说，攻击者将监视网络中可能发送的消息的最大值，并获得最大的知识攻击。但是，不可能得出攻击者A可以将路由环路引入到具有四个以上节点的任何网络中的结论。相反，A必须使用关于网络拓扑的知识，以便在不同的位置插入不同的元组：例如，它可能需要移动到更靠近特定节点的位置，并防止其他人听到某个通信。对于其他拓扑，攻击可能根本不可能，例如，如果可行的物理连接从未形成环路。5结论我们已经提出了一个广播过程演算与本地存储操作，证明是表达足够的模型的核心ad-hoc网络的距离矢量协议。演算扩展了注释，允许验证参与节点