软件学报

作者：张协力，祝跃飞，顾纯祥，陈熹

单位：张协力，数学工程与先进计算国家重点实验室, 河南 郑州 450001;网络密码技术河南省重点实验室, 河南 郑州 45000211,祝跃飞，数学工程与先进计算国家重点实验室, 河南 郑州 450001;网络密码技术河南省重点实验室, 河南 郑州 45000202,顾纯祥，数学工程与先进计算国家重点实验室, 河南 郑州 450001;网络密码技术河南省重点实验室, 河南 郑州 45000203,陈熹，数学工程与先进计算国家重点实验室, 河南 郑州 450001;网络密码技术河南省重点实验室, 河南 郑州 45000204

关键词：协议实现;形式化验证;Pi演算;模型抽取;ProVerif

基金：国家重点研发计划（2019QY1302）

形式化方法为安全协议分析提供了理论工具，但经过形式化验证过的协议标准在转换为具体程序实现时，可能无法满足相应的安全属性.为此，提出了一种检测安全协议代码语义逻辑错误的形式化验证方法.通过将协议C源码自动化抽象为Pi演算模型，基于Pi演算模型对协议安全属性形式化验证.最后给出了方案转换的正确性证明，并通过对Kerberos协议实例代码验证表明方法的有效性.根据该方案实现了自动化模型抽象工具C2P与成熟的协议验证工具ProVerif结合，能够为协议开发者或测试人员检测代码中的语义逻辑错误提供帮助.

来源：2021年第6期

《软件学报》期刊编辑部

查看软件学报杂志2021年第6期