密码协议代码执行的安全验证分析综述

• 作者: 吴福生 张焕国 王后珍 王张宜
• 来源期刊: 计算机学报
• 学科: 工学
• 关键词: 密码协议 模型 代码 执行 安全验证
• 年，卷（期）: 2018,（2）
• 所属期刊栏目: 信息安全
• 页码范围: 288-308
• 页数: 21页
• 分类号: TP309
• 字数: 14801字
• 语种: 中文
• DOI: 10.11897/SP.J.1016.2018.00288

摘要

密码协议安全验证分析是信息安全重点研究之一.常用的密码协议安全分析(例如,形式化分析、计算模型分析、计算可靠的形式化分析)只能从理论上验证或证明密码协议的安全,无法确保密码协议代码实际执行的安全.只有当密码协议在代码执行时被验证或证明安全,才能保障密码协议在实现中是安全的.因此,代码级的密码协议安全验证分析是值得关注的方向.文中分别从自动模型提取、代码自动生成、操作语义及程序精化4个方面,综述代码级的密码协议安全验证分析,并对当前代码级的密码协议安全验证分析领域中的最新成果进行详细比较、分析、总结和评论.文中以常用程序语言(C、Java、F#等)编写的密码协议为例,重点阐述密码协议代码执行的安全验证分析,并展望代码级的密码协议安伞验证分析的研究方向.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张焕国	武汉大学计算机学院	244	4083	31.0	56.0
2	王后珍	武汉大学计算机学院	9	60	6.0	7.0
3	吴福生	武汉大学空天信息安全与可信计算教育部重点实验室	5	22	3.0	4.0
4	王张宜	武汉大学空天信息安全与可信计算教育部重点实验室	11	228	7.0	11.0