基于安全协议代码的形式化辅助建模研究

随着安全协议形式化分析技术的不断发展，利用工具自动验证虽已得到实现，但建模环节仍需依赖专业人员手工建模，难度大且成本高，限制了此技术的进一步推广。为了提高建模的自动化程度，提出了依据安全协议代码进行形式化模型辅助生成的方案。首先，使用污点分析获取协议的通信流程，并且记录密码学原语操作；然后，根据通信流程之间的序列关系构建协议通信状态机；最终，根据目前主流的安全协议形式化分析工具Tamarin的模型语法生成形式化模型。实验结果表明，此方案可以生成形式化模型中的关键部分，提高了形式化建模的自动化程度，为形式化分析技术的推广作出贡献。

Research on computer-aided formal modeling for security protocol code

With the development of formal analysis technology of security protocols, automatic verification using tools has been realized, but modeling still needs to rely on manual modeling by professionals, which is difficult and costly and limits the further spread of formal analysis technology. In order to improve the automation of formal modeling, this paper proposed a scheme of formal assistant modeling based on security protocol code. Firstly, the method used taint analysis to obtain communication processes and record the cryptographic primitive operations. Then, it constructed the protocol communication state machine according to the sequential relationship between communication processes. Finally, it generated a formal model according to the syntax of Tamarin, a mainstream formal analysis tool for security protocols. Experimental results show that this scheme can generate the key parts of the formal model and improves the degree of automation of the formal modeling, which contributes to the spread of formal analysis technology.