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