基于SAT的安全协议形式化分析方法研究与应用

发布时间：2018-03-17 00:04

本文选题：安全协议　切入点：形式化分析　出处：《解放军信息工程大学》2014年硕士论文　论文类型：学位论文

【摘要】：安全协议是借助于密码学技术在不安全的公共网络上提供安全服务的通信协议,其正确性和安全性对于保障网络信息安全而言有至关重要的作用。然而安全协议的设计是一项极其复杂的系统工程,即使在完美密码假设的前提下,安全协议仍然可能存在严重漏洞或缺陷,因此在安全协议被广泛应用之前,必须对其正确性与安全性进行全面深入的分析与检测。形式化分析方法能够有效的检验安全协议的正确性与安全性,被公认为辅助安全协议设计与分析的有效方法,安全协议的自动化检测和形式化分析相关技术的研究已成为信息安全领域极其重要的研究方向,具有重要的理论意义和现实应用价值。本文在对现有安全协议形式化分析方法研究和分析的基础上,提出了一种新的基于布尔可满足性问题的安全协议模型检测方法,并利用该方法对实际网络环境中运行的安全协议进行安全性分析。详细工作总结如下:1.提出了基于布尔可满足性的安全协议形式化分析方法SAT-LMC。SAT-LMC引入协议初始状态惰性描述方法,通过变量保持以及协议参与方能力混淆等优化方法,使协议分析的初始状态大大减少,与传统协议分析工具相比效率得到很大提升;在协议重写规则中添加了类型缺陷攻击、并行会话攻击等多种攻击类型的检测支持,并通过重写规则的变量保持以及惰性的攻击者技术得到惰性的协议重写规则,效率进一步得到提升,攻击检测更加全面;采用项重写技术将协议的形式化描述转换为协议不安全问题,通过智能规划技术对其进行图形编码,最终转换为求解一个布尔可满足性问题;最后,针对现有的求解布尔可满足性问题的完备搜索算法和局部搜索算法的不足,设计了一种基于中间解加速的启发式复合算法IS-CSAT,该算法通过对两种算法的结合,在保持了完备搜索算法完备性的同时,对大部分实例具备了局部搜索算法高效性的特点。2.以SAT-LMC协议分析方法为基础,实现了安全协议分析工具SAT-LMC Tool。该工具中的可满足性问题复合求解算法集成了传统局部搜索算法的高效以及传统全局搜索算法的求全解和证伪的优点;与传统协议形式化分析工具OFMC以及SATMC比较,SAT-LMC Tool的分析速度更快,检测效率更高,同时具备对类型缺陷攻击以及并行会话攻击的检测能力,攻击检测范围更全面。3.利用安全协议分析工具SAT-LMC Tool,分析了云上开放授权协议OAuth2.0的安全性。对其在安全信道四种使用情景下的安全性分别进行分析,对可能存在的攻击给出了相应的攻击路径;另外,基于工具所给出的攻击路径,实现了针对新浪微博和优酷网的用户账号劫持攻击,上述实验结果表明,SAT-LMC Tool的设计与应用对于对规范网络安全环境有重要的作用和意义。
[Abstract]:Security protocol is a communication protocol that provides secure services on an insecure public network by means of cryptography. Its correctness and security play an important role in ensuring network information security. However, the design of security protocols is an extremely complex system engineering, even under the premise of perfect cryptographic assumption. Security protocols can still have serious vulnerabilities or flaws, so before they are widely used, Formal analysis method can effectively verify the correctness and security of security protocols, and is recognized as an effective method to assist the design and analysis of security protocols. The research of automatic detection and formal analysis of security protocols has become a very important research direction in the field of information security. Based on the research and analysis of the existing formal analysis methods of security protocols, a new security protocol model detection method based on Boolean satisfiability problem is proposed in this paper. The detailed work is summarized as follows: 1. A formal analysis method for security protocols based on Boolean satisfiability is proposed. SAT-LMC.SAT-LMC introduces the protocol initial state inertia description method. The initial state of protocol analysis is greatly reduced and the efficiency is greatly improved compared with the traditional protocol analysis tools, and the type defect attack is added to the protocol rewriting rules. Parallel session attacks and other attack types of detection support, and through overwriting rules of variable retention and lazy attacker technology to obtain lazy protocol rewriting rules, the efficiency is further improved, attack detection is more comprehensive; The formal description of the protocol is transformed into a protocol insecurity problem by item rewriting technology. Finally, the formal description of the protocol is transformed into a Boolean satisfiability problem by the graphic coding of the protocol through intelligent planning technology. Finally, a Boolean satisfiability problem is solved. Aiming at the shortcomings of the existing complete search algorithm and local search algorithm for solving Boolean satisfiability problem, a heuristic compound algorithm is designed based on intermediate solution acceleration, which combines the two algorithms. While maintaining the completeness of the complete search algorithm, it has the characteristic of high efficiency of the local search algorithm for most examples. 2. Based on the SAT-LMC protocol analysis method, A security protocol analysis tool, SAT-LMC Toolkit, is implemented, which integrates the advantages of the traditional local search algorithm and the global search algorithm. Compared with OFMC and SATMC, SAT-LMC Tool has faster analysis speed and higher detection efficiency. It also has the ability to detect type defect attacks and parallel session attacks. The security of Open Authorization Protocol (OAuth2.0) on the cloud is analyzed by using the security protocol analysis tool SAT-LMC tools. In addition, based on the attack path given by the tool, the hijacking attack against user accounts of Sina Weibo and Youku net is realized. The experimental results show that the design and application of SAT-LMC Tool play an important role in standardizing the network security environment.
【学位授予单位】：解放军信息工程大学
【学位级别】：硕士
【学位授予年份】：2014
【分类号】：TN918.4

【参考文献】