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

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

使用形式化方法能够找到安全协议设计中存在的漏洞,但高效地对安全协议进行自动的形式化分析仍然是一个挑战。针对现有形式化自动验证工具无泛化性和效率低的不足,对基于强化学习的安全协议形式化验证框架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.