Kerberos协议安全性的符号模型检验分析

Symbolic Model Checking Analysis for Security of Kerberos Protocol

基于模型检验的安全协议分析和验证是协议工程研究的一个新方向。该文建立了Kerberos协议的有限状态机模型,并用符号模型检验器(SMV)从安全属性的两个方面———认证性和保密性分析了Kerberos协议,指出了Kerberos协议的缺陷。

Model-checking has been a new direction of analyzing and verifying security protocols.In this paper,Kerberos protocol is modeled as finite state machine,and analyzed in two aspects of security property-authentication and secret property using SMV.As a result,an attack upon the protocol is discovered.