SPVT:一个有效的安全协议验证工具

• 作者: 李梦君 李舟军 陈火旺
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 形式化验证 安全协议 逻辑程序
• 年，卷（期）: 2006,（4）
• 所属期刊栏目: 计算机网络与信息安全
• 页码范围: 898-906
• 页数: 9页
• 分类号: TP309
• 字数: 9354字
• 语种: 中文

摘要

描述了基于Objective Caml开发的一个安全协议验证工具SPVT(security protocol verifying tool).在SPVT中,以扩展附加项的类(演算作为安全协议描述语言,以扩展附加项的Horn逻辑规则描述协议攻击者的Dolev-Yao模型,通过一组抽象规则将安全协议的类(演算模型转换为逻辑程序模型,基于安全协议逻辑程序的不动点计算验证安全性质,从安全协议逻辑程序的不动点计算和安全性质的验证过程中构造不满足安全性质的安全协议反例.以简化的Needham-Schroeder公钥认证协议为例,描述了使用SPVT自动验证安全协议的过程,表明了SPVT用于安全协议验证的有效性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李舟军	北京航空航天大学计算机科学与工程学院	136	2221	23.0	43.0
2	陈火旺	国防科学技术大学计算机学院	53	2116	23.0	45.0
3	李梦君	国防科学技术大学计算机学院	16	294	7.0	16.0