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

Research on computer-aided formal modeling for security protocol code

作　　者：葛艺 黄文超[1] 熊焰[1] Ge Yi;Huang Wenchao;Xiong Yan(School of Computer Science&Technology,University of Science&Technology of China,Hefei 230000,China)

机构地区：[1]中国科学技术大学计算机科学与技术学院,合肥230000

出　　处：《计算机应用研究》2023年第4期1189-1193,1202,共6页Application Research of Computers

基　　金：国家自然科学基金面上项目(61972369);国家自然科学基金青年项目(62102385);安徽省自然科学基金资助项目(2108085QF262)。

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

关 键 词：形式化验证 形式化建模 协议代码 污点分析 TAMARIN 

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