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.