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

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

作　　者：杨锦翔 熊焰[2] 黄文超[2] YANG Jinxiang;XIONG Yan;HUANG Wenchao(School of Cyberspace Security,University of Science and Technology of China,Hefei 230022,China;School of Computer Science and Technology,University of Science and Technology of China,Hefei 230022,China)

机构地区：[1]中国科学技术大学网络空间安全学院,合肥230022 [2]中国科学技术大学计算机科学与技术学院,合肥230022

出　　处：《计算机工程》2021年第12期141-146,共6页Computer Engineering

基　　金：国家重点研发计划(2018YFB2100300,2018YFB0803400);国家自然科学基金(61972369,61572453,61520106007,61572454);中央高校基本科研业务费专项资金(WK2150110009)。

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

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

分 类 号：TP309[自动化与计算机技术—计算机系统结构]