作者投稿和查稿 主编审稿 专家审稿 编委审稿 远程编辑

计算机工程 ›› 2021, Vol. 47 ›› Issue (12): 141-146. doi: 10.19678/j.issn.1000-3428.0060179

• 网络空间安全 • 上一篇    下一篇

基于强化学习的安全协议形式化验证优化研究

杨锦翔1, 熊焰2, 黄文超2   

  1. 1. 中国科学技术大学 网络空间安全学院, 合肥 230022;
    2. 中国科学技术大学 计算机科学与技术学院, 合肥 230022
  • 收稿日期:2020-12-03 修回日期:2021-01-25 发布日期:2021-01-30
  • 作者简介:杨锦翔(1996-),男,硕士研究生,主研方向为安全协议、形式化自动验证;熊焰,教授、博士后、博士生导师;黄文超,副教授、博士。
  • 基金资助:
    国家重点研发计划(2018YFB2100300,2018YFB0803400);国家自然科学基金(61972369,61572453,61520106007,61572454);中央高校基本科研业务费专项资金(WK2150110009)。

Research on Optimization of Security Protocol Formal Verification Based on Reinforcement Learning

YANG Jinxiang1, XIONG Yan2, HUANG Wenchao2   

  1. 1. School of Cyberspace Security, University of Science and Technology of China, Hefei 230022, China;
    2. School of Computer Science and Technology, University of Science and Technology of China, Hefei 230022, China
  • Received:2020-12-03 Revised:2021-01-25 Published:2021-01-30

摘要: 使用形式化方法能够找到安全协议设计中存在的漏洞,但高效地对安全协议进行自动的形式化分析仍然是一个挑战。针对现有形式化自动验证工具无泛化性和效率低的不足,对基于强化学习的安全协议形式化验证框架smartVerif进行优化。使用无人工特征、完全进行自我学习的蒙特卡洛树搜索与深度神经网络相结合的强化学习框架,同时设计能够保留形式化数据结构信息的数据转换方法。实验结果表明,利用该优化方案训练的强化学习模型具有泛化性且能高效地验证安全协议。

关键词: 强化学习, 安全协议, 形式化方法, 自动验证, 泛化性

Abstract: Many formal methods can find the loopholes in the design of security protocols, but it is still a challenge to analyze the security protocols automatically and efficiently.To address the poor generalization performance and low efficiency of the existing formal automatic verification tools, the reinforcement learning-based formal verification framework, smartVerif, for security protocols is optimized.A reinforcement learning framework combining deep neural network with Monte Carlo tree search that learns without human intervention is used.At the same time, a data conversion method which can preserve the formal data structure information is designed.The experimental results show that the reinforcement learning model trained by the optimization scheme exhibits high generalization performance, and can effectively verify a security protocol.

Key words: reinfoecement learning, security protocol, formal method, automated verification, generalization performance

中图分类号: