Using the NuSMV Model Checker to verify the Kerberos Protocol