基于SPI演算的移动自主网络安全路由协议分析

安全协议是许多分布式系统安全的基础,也是MANET网络的基础,确保MANET路由协议的安全运行是极为重要的。对于MANET的特点,设计一个可靠的安全路由协议是必须的,也是一个艰巨的任务,但大多数的安全路由协议都是通过模拟结果来进行解释的,缺乏严格形式化分析来确保其安全属性。在传统的安全属性中,加密协议已经被形式化分析许多年了,然而去形式化分析移动adhoc网路由协议的工作并没有出现已成熟的方法和理论的文献。论文针对SRP(secureroutingprotocol)协议模型用SPI演算做出形式化分析,在论文提出的攻击者进程模型下,可以推导出SRP产生一定的脆弱性。

Security Analysis of Routing Protocol for MANET Based on SPI Calculus

Security protocol is the basis for the distributed system,the same is required of the manet,it is important to ensure the running of this protocols.According to the character of manet,it is necessary to design reliable secure routing protocol and it is a hard task.But new protocols are predominantly validated by an interpretation of simulation results, thus lacking a rigid formal analysis necessary for ensuring security.It has been analysed by formalization for a lot of years in traditional cryptograph protocol attribute,however it appears no mature formal method and reference in formal analysis mobile ad hoc network security routing protocol.Tbe article presents a formal analysis of the SRP routing protocols that are suitable to the mobile Ad hoc network and in the circumstance of attacker model described in the article.The authors abstract the attack and conclude that protocols developed in the likeness of SRP are equally vulnerable.The analysis follows the methodology of SPI calculus and abstract interpretation.