TSPVT:一个有效的时间敏感安全协议验证工具
如何自动化验证时间敏感安全协议的安全性一直是形式化研究领域的热点和难点,如何在验证过程中简单而有效地考察由时间戳而引入的约束条件信息成为验证时间敏感协议的难点问题.TSPVT是基于Objective Caml语言,在安全协议验证工具SPVT的基础上开发的时间敏感安全协议验证工具.TSPVT在SPVT基础上,首先以扩展了时间事件的类π演算作为时间敏感安全协议描述语言,然后TSPVT将协议的类π演算模型自动转换为带时间约束系统的霍恩逻辑程序P,P由刻画安全协议诚实角色的一组逻辑规则和一组基于扩展的Dolev-Yao模型的攻击者规则组成;最后在对协议霍恩逻辑模型的验证阶段,考察带时间约束系统的规则消解,基于安全协议逻辑程序P解形式不动点的计算,验证安全协议的认证性.以Denning-Sacco协议为例,描述了使用TSPVT自动验证安全协议的过程,表明了TSPVT用于验证时间敏感安全协议的有效性.
时间敏感安全协议 验证工具 安全性
李舟军 赵倩倩 周倜
北京航空航天大学,计算机学院,北京,100191 北京航天飞行控制中心,软件室,北京,100094
国内会议
合肥
中文
61-74
2010-10-01（万方平台首次上网日期，不代表论文的发表时间）