一种安全DSR协议的形式化分析方法  

Formal analysis method for secure dynamic source routing protocols

作　　者：刘晶[1] 伏飞[2] 肖军模[1] 

机构地区：[1]解放军理工大学通信工程学院,江苏南京210007 [2]解放军理工大学指挥自动化学院,江苏南京210007

出　　处：《解放军理工大学学报（自然科学版）》2009年第5期423-429,共7页Journal of PLA University of Science and Technology(Natural Science Edition)

基　　金：国家自然科学基金资助项目(69931040)

摘　　要：目前安全DSR协议由于缺乏有效的形式化分析方法,难以发现一些隐蔽的安全漏洞。针对这一问题,通过分析DSR协议路由过程,给出了安全DSR协议的安全目标。提出了一种基于逻辑的安全DSR协议形式化分析方法,定义了能够反映安全DSR协议特性的基本逻辑构件(包括主体、目标和公式)和推理规则。首先用逻辑公式描述协议初始假设及过程,然后用推理规则进行推导产生推导结果,最后依据推导结果判断协议安全性。使用这种方法对SADSR协议进行了形式化分析与改进,发现了SADSR协议存在的安全漏洞。分析结果表明,提出的方法能够用于安全DSR协议形式化分析,能够发现一些较为隐蔽的安全缺陷。Currently, secure DSR protocols are short of formal analysis methods to find out their hidden vulnerabilities. To solve this problem, by analyzing the routing process of DSR protocols, a logic based analysis method was proposed. The method defined the basic logic items（subject, goal and formula）and inference rules. The original hypothesis and process were defined by formulas. Then, inference rules were used to produce results for judging the security of the protocol. SADSR protocol was found insecure and corrected by this method. The result shows that the proposed method is fit for secure DSR protocols formal analysis and can be used to find the concealed vulnerabilites.

关 键 词：移动自组织网络 安全路由协议 形式化分析 攻击 

分 类 号：TN918[电子电信—通信与信息系统]