安全协议用于实现开放互连网的通讯安全,时间戳可以保证协议传输消息时的新鲜性。但目前对含有时间特性的协议的研究还很不成熟,还没有有效的方法来验证带时间戳的安全协议。这使得一些大规模复杂协议的安全性质无法通过形式化方法进行全面的验证。详细说明了时间戳的起因和研究时间戳的原因;详细介绍了国际上时间戳特性的几种主流研究方法——MSR方法、归纳法、CSP方法和BAN逻辑在时间敏感安全协议验证方面的工作,对它们的优缺点进行了评述,并指出了进一步的研究方向。
Security protocols are used to provide secure communication over open network. Time-stamp can make sure the freshness of the message in the protocol, but it is not enough to research the time sensitive protocols, and there are no effective methods that can verify these protocols. So it's very difficult to verify all aspects of those huge and complex protocols in formal ways. This paper described why using time-stamp and researching it, and discussed several popular methods in this field which are MSR method, induction method, CSP method and BAN logic method in verification of time sensitive security protocols. This paper gave out their estimations. Finally we also stated the possible new directions of time sensitive security protocols verification.