题目：时间敏感安全协议的形式化验证方法及工具

采用时间戳机制来保证消息的新鲜性以防止重放攻击的安全协议称为时间敏感安全协议，随着网络安全日益苛刻的要求，时间敏感安全协议逐渐应用于愈来愈多的领域以实现更复杂的安全性目标。如何对时间敏感安全协议进行形式化建模、分析及验证已经成为研究的热点和难点。 本文首先全面系统地分析了目前国际上对时间敏感安全协议Kerberos 5的形式化验证工作。对该协议的形式化分析方法可归结为两类：基于符号模型的验证方法和基于计算模型的验证方法。目前国际上已在计算模型下对Kerberos 5协议进行了完整建模，并在交互式验证工具的辅助下完成了相应的验证工作，但尚未在符号模型下开发出有效工具以实现自动化验证Kerberos 5。 本文扩展了类演算模型及霍恩逻辑模型，实现了对时间敏感安全协议的建模与分析，在此基础上设计和实现了时间敏感安全协议验证工具TSPVT，该工具首次实现了在符号模型下自动验证时间敏感安全协议的认证性。本文详细介绍了TSPVT的基本原理、主体框架、核心模块及采用的核心算法和技术。并以Denning-Sacco协议为例，描述使用TSPVT自动验证协议的过程，表明了TSPVT用于验证时间敏感安全协议的有效性。最后本文实现了建模与验证Kerberos 5，分别考察三个认证性目标，利用TSPVT，实现了在符号模型下自动验证该协议的认证性，验证结果表明，Kerberos 5协议满足C对KAS、C对TGS以及C对S的认证性。