时间敏感的安全协议建模与验证:研究综述

安全协议用于实现开放互连网的通讯安全，时间戳可以保证协议传输消息时的新鲜性。但目前对含有时间特性的协议的研究还很不成熟，还没有有效的方法来验证带时间戳的安全协议。这使得一些大规模复杂协议的安全性质无法通过形式化方法进行全面的验证。详细说明了时间戳的起因和研究时间戳的原因;详细介绍了国际上时间戳特性的几种主流研究方法—msr方法、归纳法、csp方法和ban逻辑在时间敏感安全协议验证方面的工作，对它们的优缺点进行了评述，并指出了进一步的研究方向。