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

摘要：

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

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

所属期刊栏目：40

分类号：TP309(计算技术、计算机技术)

资助基金：国家自然科学基金;国家自然科学基金;安徽省自然科学基金资助项目

在线出版日期：2023-05-10（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：1189-1193,1202