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

被引：17

作者：

李梦君 ^{[1
]}

李舟军 ^{[2
]}

陈火旺 ^{[1
]}

机构：

[1] 国防科学技术大学计算机学院

[2] 北京航空航天大学计算机科学与工程学院

来源：

软件学报 | 2006年 / 04期

关键词：

形式化验证; 安全协议; 逻辑程序;

D O I：

暂无

中图分类号：

TP393.08 [];

学科分类号：

0839 ; 1402 ;

摘要：

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

引用

页码：898 / 906

页数：9

共 4 条

[1] 基于逻辑程序的安全协议验证 [J].