基于自适应模型检测的安全协议自动建模与设计研究

Security protocols are the foundation of network security, and formal method is the most popular method for the security protocol analysis. While at the present, in order to improve the flawed security protocols, the only way is artificial adjustment or redesign, which mostly relies on the experience and skills of the technical personnel. It is not only inefficient and costly but also easy to introduce new errors. To deal with these problems, preliminary research has shown that the newly proposed adaptive formal method, which can modify its model automatically with the help of the counter examples, will be a reasonable candidate...The main purpose of this project is to do some further research about the adaptive analysis and design of security protocols. We aim to build a real-time dynamic analysis system offering optimal design solutions for security protocols. The key point is to construct a set of adaptive formal analysis algorithms, by which the security models of the protocols will be refined automatically with the help of counter examples given by the formal verification. This scheme can automate the whole process of design, verification, and optimization of the security protocols by taking advantage of the adaptive technique. The researches include adaptive modeling of both protocols and security requirements, design of the adaptive learning algorithms, and construction of the integrated simulation platform. The research of this project will set the foundation for liberating the security design and refinement from tedious human tests. It has important theoretical and practical significance in improving the efficiency of security protocol analysis, reducing the protocol design cost, and raising the adaptive ability of the security protocols to the rapid change of network environment and constantly updated attack techniques..

安全协议是保证网络安全的基础，形式化方法是分析安全协议是否符合安全目标的主流方法。目前对于存在漏洞的协议，需人为对其修正或设计新协议，这种人工处理方式不仅效率低下，而且严重依赖经验、易引入新的漏洞。初步研究表明，根据反例自动修正模型的自适应模型检测方法将有望解决安全协议分析的上述问题，目前国际上尚未出现相关研究工作。. 本课题是对安全协议自动建模及设计进行的探索性研究，主要内容包括安全协议的自适应建模、自适应学习等算法的设计及实例仿真验证。旨在借鉴实时更新模型的自适应技术将安全协议的设计过程与分析过程统一起来，构造一套自适应建模方案及算法。该方案将根据攻击路径自动改进模型，并以此指导协议的设计，从而将协议的设计和改进从繁琐的人为试探中解放出来。安全协议自适应建模及设计的实现对于提高其验证和设计效率、降低分析和设计成本、增强协议本身对环境和攻击手段的自适应防御能力有重要意义。

安全协议是保证网络安全的基础，形式化方法是分析安全协议是否符合安全目标的主流方法。目前对于存在漏洞的协议，需人为进行修正或重新设计，这种人工处理方式不仅效率低下，而且严重依赖经验、易引入新的漏洞。本课题基于自适应模型检测提出一种自适应形式化建模及分析方案，该方案能够通过对反例的学习自动改进模型并指导协议的改进和设计。主要内容包括：安全协议的自适应建模、模型学习算法的设计与实现、以及仿真环境的搭建及实例验证。与现有的分析和验证方法相比，本方案最大的优势在于：当需求产生变化时，它可以对协议模型进行自适应地更新，而不需要重新进行设计，从而提高安全协议的验证和设计效率、降低分析和设计成本、增强协议本身对环境和攻击手段的自适应防御能力。针对经典协议及新型协议的验证表明，该方案是行之有效的。