Form Analysis of Kerberos Protocal and NuSMV Verification
Zhang Chun-yong · Journal of Yancheng Institute of Technology · 2009
NuSMV is a symbolic model verification tool based on computation tree logic.The Kerberos authentication protocal was analysed,and the finite state model was set up.The non-security of Kerberos protocol exists which was verifing from security property,authentication and liveness using NuSMV.