時間敏感的安全協議建模與驗證研究(pdf 6頁)

時間敏感的安全協議建模與驗證研究內容提要：
協議用於實現開放互連網的通訊安全，時間戳可以保證協議傳榆消息時的新鮮性。但目前對含有時間特性的協議的研究還很不成熟，還沒有有效的方法來驗證帶時間戳的安全協議。這使得一些大規模複雜協議的安全性質無法通過形式化方法進行全麵的驗證。詳細說明了時間戳的起因和研究時間戳的原因；詳細介紹了國際上時間戳特性的幾種主流研究方法——MSR方法、歸納法、CSP方法和BAN邏輯在時間敏感安全協議驗證方麵的工作，對它們的優缺點進行了評述，並指出了進一步的研究方向。
..............................