MANET安全路由协议自动化分析

毛立强，黄 影

(1. 西安电子科技大学 计算机学院，陕西 西安 710071; 2. 西安文理学院 数学与计算机工程学院，陕西 西安 710068)



MANET安全路由协议自动化分析

毛立强1，黄 影2

(1. 西安电子科技大学 计算机学院，陕西 西安 710071; 2. 西安文理学院 数学与计算机工程学院，陕西 西安 710068)

移动ad hoc网络安全路由协议已经成为一个热门的研究领域，其中协议的安全性分析方法及其自动化实现倍受关注．利用SPIN工具自动分析了SRP和Ariadne协议，首先通过网络拓扑建模和自动生成，可以全面分析在不同网络拓扑下协议的安全性．再通过节点丢弃攻击和协议建模，自动发现了针对协议的有效攻击，证明基于模型检测及SPIN工具自动分析安全路由协议的方法是有效的．

路由协议;形式化分析;SPIN;模拟模型

移动自组网(Mobile Ad Hoc Networks，MANET)是一个非常复杂的分布式系统，在诸如指挥作战、会务通信、保障救灾、实施危险环境或远距离监控等无固定网络设施的环境中，有着广泛的应用．安全路由协议的设计与分析[1]是移动ad hoc网络中一个热门的研究领域，目前大部分安全路由协议分析都是基于直接观察或者模拟仿真等方法，这些非形式方法缺乏严格精确的分析过程，导致协议设计者宣称“安全”的路由协议相继被发现仍存在安全漏洞．

近年来有学者开始尝试MANET安全路由协议形式化分析方法及其自动化实现的研究．文献[2]利用Succinct Solver分析安全按需距离矢量路由(Secure Ad hoc On-demand Distance Vector，SAODV)协议，但有着严格的通信环境假设，不具有通用性．文献[3]提出了基于演绎证明和反向可达性的分析方法，利用Java开发了自动化分析工具，发现了针对安全路由协议(Secure Routing Protocol，SRP)和Ariadne协议的攻击，该方法对网络拓扑没有严格要求，但其分析过程只适用于一个敌手节点的情况．文献[4]基于代数Petri网，利用模型检测工具AlPiNA，发现了针对ad hoc认证路由协议(Authenticated Routing for Ad-hoc Networks，ARAN)的攻击，但该分析过程仅针对ARAN协议，缺乏通用性．文献[5]利用模型检测工具AVISPA分析ARAN和endairA协议，发现了针对ARAN的3个攻击方法，未发现针对endairA的攻击，但其分析仅限于固定的网络拓扑．文献[6]同样利用AVISPA分析ARAN，试图分析所有的网络拓扑和消息交互过程，但没有很好的解决时间复杂度问题．

与AVISPA类似，简单进程元语言解释器(Simple Promela INterpreter，SPIN)是一个用来验证分布式系统操作的通用模型检测工具，已经成功应用于安全认证协议的自动化分析及安全环境下MANET路由协议性能分析[7-8]．SPIN利用建模语言Promela描述协议操作和目标，构造一个有限状态机并进行搜索，以确定目标是否能够达到．若不能达到目标，SPIN则产生导致目标失败的事件序列．笔者利用SPIN工具，通过对协议、攻击者和网络拓扑的建模，分析SRP和Ariadne，表明SPIN分析MANET安全路由协议的有效性．

1 协议建模

无线ad hoc网络安全路由协议的两个基本目标是正确性和可靠性，前者是指在路由发现阶段，协议能够发现在当时网络拓扑下确实“存在的”路由; 后者是指在数据传输阶段，协议能够识别路由是否失效，并启动路由发现过程或者选用其他可用路由．利用基于模型检测的自动化分析工具，通过对路由发现过程进行建模分析，验证是否攻击者可以破坏路由发现过程，如果不能成功进行攻击，则表明协议是安全的; 如果可以成功进行攻击，则能够发现攻击步骤和方法．

按需源路由协议将路由信息嵌入在节点间互相发送的路由消息中，其路由发现过程可以分为路由请求过程和路由回复过程，两个过程都有可能被攻击．动态源路由(Dynamic Source Routing，DSR)是被广泛研究的按需源路由协议，SRP和Ariadne都是在DSR基础上进行安全扩展．假设节点通信都是双向的，目标节点接收到路由请求rreq，通过路由回复rrep返回发现的路由．通过验证安全环境下协议能够发现所有可能的路由，以及协议安全机制能够发现协议可能受到的攻击，来证明协议满足其安全目标．

DSR只实现了基本的移动路由功能，没有任何安全机制保护路由发现过程，其路由发现过程如下：

rreq process:

◆Initiator node

—Initiate rreq to target

◆Intermediate nodes

—If previously seen rreq→take no action

—Else

◇If not target→append id to path

and retransmit rreq

◇If target→generate rrep rrep process:

◆Target node

—Unicast the rrep

◆Intermediate nodes(along unicast path)

—If not initiator→retransmit rrep

—If initiator→accept route

DSR路由发现过程的消息格式为_msg_type， initiator， target， id， accum_path．其中msg_type表示消息类型为路由请求或者路由回复; initiator和target表示路由的源节点和目标节点; id作为消息惟一标识，保证节点发送的rreq为该节点第一次接收的路由请求; accum_path表示已经发现的节点路径，包括路径上所有中间节点，当节点继续发送该路由请求时，节点路径被更新，这里所发现的路由将包括路由源节点和目标节点在内的路径上的所有节点，并允许模型检测器在分析过程中将该信息与网络拓扑结构进行比较;增加定义一个位置参数accum_pos用来跟踪记录节点数组的当前位置，于是DSR路由消息格式可以建模为_msg_type， initiator， target， accum_path， accum_pos．一旦路由请求到达目标节点，目标节点就产生一个路由回复并发送回源节点．在路由回复过程中，模型检测器通过读取accum_path和accum_pos，决定路由回复消息发送给接下来哪一个节点．

SRP对DSR进行了安全扩展，其假设源节点和目标节点之间存在安全链接，可以共享加密消息认证码(Message Authentication Code，MAC)，此MAC只能由源节点或目标节点进行计算和验证，中间节点在路由发现过程中没有任何加密机制，与DSR中间节点的操作相同，路由过程如下:

rreq process:

◆Initiator node

—Compute MAC over initiator， target，Qid，

andQsn

—Initiate rreq to target

◆Intermediate nodes

—If previously seen rreq→take no action

—Else

◇If not target→append id to path

and retransmit rreq

◇If target→take actions below in rreprrep process:

◆Target node

—Validate MAC contained in rreq

—Compute new MAC over initiator， target，

Qid，Qsn， and accumulated path

—Unicast the rrep

◆Intermediate nodes(along unicast path)

—If not initiator→retransmit rrep

—If initiator

◇Validate MAC contained in rrep

◇Accept path if MAC validates

SRP消息格式表示为_ msg_type， initiator， target，Qid，Qsn， MACit， accum_path．其中，参数Qid和Qsn用来保证路由请求是惟一的，中间节点可以利用一个布尔参数判断其是否多次转发某一rreq．对于给定的一个路由发现过程，MAC的计算包含了惟一的Qid和Qsn，所以路由请求过程中加密的MACit可以抵御replay攻击．因为假设中间节点不具备攻击MAC的能力，所以在路由请求过程中不需建模MAC计算过程．然而，在路由回复过程中，需要建模MAC计算过程，以分析可能的针对所发现路由的攻击．这样，也可以减少建模后的状态空间．为了能够分析针对accum_path的攻击，正确计算并验证rrep中的MAC，SRP路由消息格式可以建模为_msg_type， initiator， target， accum_path， accum_pos， mac_path．在路由发现过程中，目标节点拷贝rreq中收到的路由信息到mac_path变量中，并将其加到rrep中，以此来建模其对所发现路由进行的MAC计算．根据假设条件，MAC只能由源节点和目标节点计算和验证，攻击者不具备破坏MAC的能力，这一点通过不允许模型的中间节点访问mac_path来表示．一旦源节点接收到rrep，通过验证发现的路由与mac_path中包含的路由信息的一致性，来判断是否接受所发现的路由．

Ariadne协议也是对DSR的扩展，其安全机制包括每个中间节点计算每跳单向散列值，保证路由请求安全;附加目标节点对于所发现路由的签名信息，保证路由回复安全．其消息格式为:

_rreq， initiator， target， id， hash_value， accum_path，sig_list，

_rrep， initiator， target， accum_path， sig_list， target_sig．

散列值hx是防止攻击者从已经发现的路由中删除某个节点，每个中间节点增加其id到accum_path中，计算并插入一个新的每跳散列值hash_value．此外，还计算并附加一个签名sig_list到完整的消息上，以保证路由只包含可信节点，节点x的签名表示为sigx．一旦目标节点收到rreq，就对单向散列值进行验证，如果验证有效，则目标节点对发现的路由进行签名，并将路由和签名一起通过rrep返回．在路由回复过程中，中间节点按照路由上的节点反向依次发送路由回复．源节点通过验证收到的签名是否有效，判断是否接受收到的路由．Ariadne协议路由发现过程与DSR类似，只是增加了散列和签名计算，以及相应的源节点和目标节点的有效性验证，其路由过程如下：

rreq process:

◆Initiator node

—Compute initial hash value over the message

id and initiator-target secret

—Initiate rreq to target

◆Intermediate nodes

—If previously seen rreq→take no action

—Else

◇If not target

Append node_id to path

Calculate new hash value

Attach signature

Retransmit rreq

◇If target→take actions below in rreprrep process:

◆Target node

—Validate one-way hash to detect

path attacks against rreq

—Calculate and attach signature

over the received rreq

—Unicast the rrep

◆Intermediate nodes(along unicast path)

—If not initiator→retransmit rrep

—If initiator

◇Validate node signature to ensure path

only contains insiders

◇Validate target signature to ensure

route not corrupted during rrep

这里把rreq和rrep表示成相同形式，将目标节点和中间节点的签名进行组合，消息结构建模为_msg_type， initiator， target， accum_path， hash_chain， sig_list．需要注意的是，hash_chain和sig_list分别表示加密的单向散列值和签名列表．对于前者，每个中间节点都需要增加其id到先前的散列值之后，重新进行散列计算，于是产生了单向散列链 hi= H[ni， hn(i-1)]= Hni， H[ni-1，…， H[n0， h0]]，这里i表示rreq中当前节点，i-1 表示前一节点．在协议操作过程中，重新计算的散列链包含在每个发送的消息中，这里将散列计算和散列链表示成[ni， ni-1，…， n1， n0]．中间节点只能转发整个散列链或者附加之前收到的散列链重新进行散列计算．与accum_path不同，hash_chain不允许中间节点修改．当目标节点收到路由请求时，验证其中发现的路由与散列链是否匹配．Ariadne协议通过中间节点的签名列表sig_list防止路由中插入外部恶意节点，源节点通过签名验证接收到的路由．sig_list的表示方式与散列值相同，通过增加节点id到sig_list来表示对收到的消息进行签名．sig_list用数组来表示，其中最后一个元素表示最新的一个用接收到的消息和之前所有签名信息计算得到的签名．这里，签名列表不能被重新排序，但是最后一个签名可以被丢弃，以表示攻击者可以丢弃当前所发现路由中最后一个节点信息．

综上，Ariadne建模需要表示路由请求过程中的每跳单向散列值和路由回复过程中保证所发现路由安全的目标节点的签名．目标节点通过拷贝rreq中所发现的路由到rrep的签名中，来表示对接收消息的签名．路由回复过程中的签名机制不能被破坏，这样源节点就能够通过签名来验证返回的路由，由此发现针对路由回复过程的攻击．于是，Ariadne协议消息格式可以建模为_msg_type， initiator， target， accum_path， accum_pos， crypt_val， hash_pos．其中，accum_pos用来表示内部可信节点增加其id到发现的路由后的当前位置，hash_pos表示当前路由请求rreq消息中散列链的当前位置．数组crypt_val用来表示散列链和目标节点签名，在路由请求过程中，代表散列链; 在路由回复过程中，代表目标节点签名．

2 攻击者建模

假设攻击者将主动攻击路由发现过程，成功攻击的结果使得协议返回与实际网络拓扑不一致的路由．针对SRP的攻击可以考虑节点丢弃攻击(Node Drop Attack，NDA)，可以选择攻击路由请求过程，使得目标节点对已经破坏的路由计算MAC，源节点在验证时，就不会发现不一致．上述针对SRP的NDA模型能够利用SPIN完全自动化实现，不需要任何手动交互，具体过程描述如下：

rreq process:

◆If previous node initiator→take no action

◆Else

—Remove previous node id from

accumulated path

—Add own id to path

—Retransmit rreq rrep process:

◆Relay unicast message to all

upstream nodes

在路由请求过程中，攻击者将当前收到的路由的最后一个节点信息删除，用自己的id替换，只要删除的节点不是源节点即可成功．该路由信息到达目标节点后，MAC依此进行计算．在路由回复过程中，攻击者转发rrep给路由上所有的节点，试图将该信息发送给源节点或者能够转发该信息给源节点的节点．只要消息能够被源节点接收，则攻击就成功了．

针对Ariadne的攻击也可以考虑在路由请求过程进行节点丢弃攻击．观察rreq消息结构可以发现，其中的路由信息是可以修改的，只要相应的散列链和签名与所做修改一致即可．虽然签名机制使得攻击者不能改变路由中的节点顺序，也能够防止路由中插入外部节点，但是恶意的内部节点还是可以在当前路由最后位置插入或者丢弃一个节点，恶意的外部节点就只能丢弃最后一个节点．下面描述一个恶意内部节点针对Ariadne的NDA过程，如果攻击者直接收到源节点的rreq，就将散列值存储下来，不进行任何其他操作，一旦收到其他中间节点的rreq，则先存储这个节点的散列值，并与之前存储的散列值进行比较，以便形成可以用来攻击所必需的信息．

rreq process:

◆If previous node initiator→store hash value

◆Else

—store hash value

—if a hash is known for any upstrorm node in

the embedded path

◇Drop previous node and add own id to path

◇Compute hash value to match current path

◇Retransmit changed rreqrrep process:

◆Relay unicast message to all upstream nodes

3 SPIN运行实例

利用SPIN实现针对Ariadne协议的NDA模型．系统中定义了一个反映当前网络拓扑结构的连通性数组，当发起路由发现过程的源节点接收到返回的路由时，将路由节点列表与该数组进行比较，如果验证失败，SPIN则产生一个异常警告并终止运行，同时生成一个文件用来记录导致失败的消息序列．通过对该序列的分析，可以得到针对协议的有效攻击方法．

图1 Ariadne协议攻击序列

给定一个含有5个节点的网络拓扑，如图1所示．0为源节点，3为目标节点，4为攻击者．图中显示了一个导致路由失败的消息序列，节点4将msg3中的节点2删除，将自己id增加到当前的路由中，计算相对应的散列值，形成msg4继续发送．被破坏的路由0-1-4-3通过msg5返回到源节点0，并将验证通过．文献[9]通过模拟模型和直接观察方法也发现了同样的针对Ariadne协议的攻击．

4 结 束 语

MANET安全路由协议的形式化分析方法受到了越来越多的关注，也有学者尝试对协议进行自动化分析．笔者利用SPIN工具，通过对协议过程及攻击者的建模，分析按需源路由协议SRP和Ariadne，发现了针对协议的有效攻击，表明了SPIN分析移动MANET安全路由协议的有效性．因为无线环境下不能保证所有消息都能够被接收，SPIN需要对攻击者可能产生的破坏路由发现过程的所有消息序列进行分析．此外，针对协议的可能攻击与协议本身的漏洞、所分析的网络拓扑都有关系，所以分析过程需要针对所有可能的网络拓扑结构．后续将对SPIN中如何更好地表示网络拓扑结构以及如何减少状态空间[10]，避免状态空间爆炸问题进行研究．

[1] SHARMA S B, CHAUHAN N. Security Issues and Their Solutions in MANET[C]//Proceedings of the 2015 1st International Conference on Futuristic Trends in Computational Analysis and Knowledge Management. Piscataway: IEEE, 2015: 289-294.

[2]NANZ S, HANKIN C. A Framework for Security Analysis of Mobile Wireless Networks [J]. Theoretical Computer Science, 2006, 367(1/2): 203-227.

[3]THONG T V, BUTTYAN L. On Automating the Verification of Secure Ad-hoc Network Routing Protocols[J]. Telecommunication Systems, 2013, 52(4): 2611-2635.

[4]PURA M L, BUCHS D. Model Checking ARAN Ad Hoc Secure Routing Protocol with Algebraic Petri Nets[C]//Proceedings of the 10th IEEE International Conference on Communications. Piscataway: IEEE, 2014: 1-4.

[5]BENETTI D, MERRO M, VIGANO L. Model Checking Ad Hoc Network Routing Protocols: ARAN vs Endair A[C]//Proceedings of the 8th IEEE International Conference on Software Engineering and Formal Methods. Piscataway: IEEE, 2010: 191-202.

[6]PURA M L, PATRICIU V V, BICA I. Formal Verification of Secure Ad Hoc Routing Protocols Using AVISPA: ARAN Case Study[C]//Proceedings of the 4th Conference on European Computing Conference. Athens: World Scientific and Engineering Academy and Society, 2010: 200-206.

[7]WIBLING O, PARROW J, PEARS A. Automatized Verification of Ad Hoc Routing Protocols[C]//Lecture Notes in Computer Science: 3235. Berlin: Springer Verlag, 2004: 343-358.

[8]ZAIDI F, LALLALI M, MAAG S. A Component Based Testing Technique for a MANET Routing Protocol[C]//Proceedings of the ACS/IEEE International Conference on Computer Systems and Applications. Piscataway: IEEE Computer Society, 2010: 5587040.

[9]ACS G, BUTTYAN L, VAJDA I. Provably Secure On-demand Source Routing in Mobile Ad Hoc Networks [J]. IEEE Transactions on Mobile Computing, 2006, 5(11): 1533-1546.

[10]CORTIER V, DEGRIECK J, DELAUNE S. Analysing Routing Protocols: Four Nodes Topologies Are Sufficient[C]//Lecture Notes in Computer Science: 7215. Berlin: Springer Verlag, 2012: 30-50.

(编辑：王 瑞)

Automated security analysis techniques in MANET routing protocols

MAOLiqiang1，HUANGYing2

(1. School of Computer Science and Technology, Xidian Univ., Xi’an 710071, China; 2. School of Mathematics and Computer Engineering, Xi’an Univ. of Arts and Science, Xi’an 710068, China)

Automated security analysis techniques in Mobile ad hoc network(MANET) routing protocols has become a hot research field. We have developed an automated evaluation process to analyze security properties of SRP and Ariadne. Using the automated security evaluation process, we can produce and analyze all topologies for a given network size. The NDA attackers and routing protocols are modeled in SPIN, and the route corruption attack is found automatically, which indicates the effectiveness of automated analysis of MANET route protocols using SPIN.

routing protocol;formal analysis;simple promela interpreter;simulatability model

2014-09-28

时间：2016-04-01

国家自然科学基金重点资助项目(U1135002)

毛立强(1978-)，男，高级工程师，博士，E-mail: lqmao@xidian.edu.cn．

http://www.cnki.net/kcms/detail/61.1076.tn.20160401.1622.020.html

10.3969/j.issn.1001-2400.2016.06.010

TP393.04

A

1001-2400(2016)06-0056-06