Kerberos协议安全性的SPIN分析

SPIN Analysis for Security of Kerberos Protocol

随着网络应用的迅速发展,协议的安全性显得越来越重要,对协议的安全性分析和研究也成为目前一个非常紧迫的课题。介绍Kerberos协议,然后采用非形式化方法对协议进行分析,最后使用模型检测工具SPIN对协议从安全属性的两个方面,认证性和保密性进行了分析,模拟实现了协议的重放攻击。

With the rapid development of network applications, security of protocols has been of great importance and now the analysis and research on protocols＇ security has also been an urgent task. Introduces Kerberos protocol, then uses informal methods to analysis protocols, and finally applies model checker SPIN to analyse the protocol in two aspects of security property, authentication and secret property and simulates to achieve the replay attacks.