| SPVT:一个有效的安全协议验证工具 |
| |
| 引用本文： | 李梦君,李舟军,陈火旺.SPVT:一个有效的安全协议验证工具[J].软件学报,2006,17(4):898-906. |
| |
| 作者姓名： | 李梦君 李舟军 陈火旺 |
| |
| 作者单位： | 1. 国防科学技术大学,计算机学院,湖南,长沙,410073
2. 北京航空航天大学,计算机科学与工程学院,北京,100083 |
| |
| 基金项目： | 中国科学院资助项目;国家科技攻关项目 |
| |
| 摘 要： | 描述了基于Objective Caml开发的一个安全协议验证工具SPVT(security protocol verifying tool).在SPVT中,以扩展附加项的类(演算作为安全协议描述语言,以扩展附加项的Horn逻辑规则描述协议攻击者的Dolev-Yao模型,通过一组抽象规则将安全协议的类(演算模型转换为逻辑程序模型,基于安全协议逻辑程序的不动点计算验证安全性质,从安全协议逻辑程序的不动点计算和安全性质的验证过程中构造不满足安全性质的安全协议反例.以简化的Needham-Schroeder公钥认证协议为例,描述了使用SPVT自动验证安全协议的过程,表明了SPVT用于安全协议验证的有效性.
|
| 关 键 词： | 形式化验证 安全协议 逻辑程序 |
| 收稿时间： | 2004-09-28 |
| 修稿时间： | 2005-11-08 |
SPVT: An Efficient Verification Tool for Security Protocol |
| |
| LI Meng-Jun,LI Zhou-Jun and CHEN Huo-Wang.SPVT: An Efficient Verification Tool for Security Protocol[J].Journal of Software,2006,17(4):898-906. |
| |
| Authors: | LI Meng-Jun LI Zhou-Jun and CHEN Huo-Wang |
| |
| Affiliation: | 1.School of Computer, National University of Defense Technology, Changsha 410073, China; 2.School of Computer Science and Engineering, BeiHang University, Beijing 100083, China |
| |
| Abstract: | |
| |
| Keywords: | formal verification security protocol logic program |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
|
