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

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

项目编号： No.61402434

项目类型： 青年科学基金项目

立项/批准年度： 2015

项目学科： 计算机科学学科

项目作者： 范丹

作者单位： 中央财经大学

项目金额： 10万元

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

中文关键词： 安全协议；形式化分析；模型检测；自适应；协议设计

英文摘要： 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 requirem

英文关键词： security protocol；formal analysis；model checking；adaptive method；protocol design