一种时间相关安全协议的自动验证工具  

Automated verification tool for time-dependent cryptographic protocols

作　　者：黎兴华[1] 雷新锋[1] 刘军[1] 

机构地区：[1]解放军理工大学通信工程学院,南京210007

出　　处：《计算机应用》2009年第6期1654-1658,共5页journal of Computer Applications

基　　金：江苏省自然科学基金资助项目(BK2008090)

摘　　要：设计并实现了一个时间相关安全协议的自动验证工具。工具以一种时间相关安全协议逻辑TCPL为基础,以XML语言为描述方式,采用构造分层逻辑树的方法,完成了对安全协议目标的自动验证。实现结果表明,该工具简化了安全协议的证明过程,提高了效率,具有较好的实用性。An automated verification tool for analyzing time-dependent cryptographic protocol was proposed and implemented. Based on Time-dependent Cryptographic Protocol Logic （TCPL）, the tool completed verifying the goals of cryptographic protocols automatically by the method of layered logic tree and using XML as its specification language. Experimental result shows that the tool can simplify the proving process, and improve the efficiency of security protocols verification.

关 键 词：分层逻辑树 时间相关 安全协议 自动验证 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]