Using the NuSMV Model Checker to verify the Kerberos Protocol

摘要: The aim of this paper is to present a methodology for verifying cryptographic protocols by means NuSMV, symbolic model checker. We illustrate approach describing our analysis the basic version Kerberos, widely used authentication protocol. most innovative feature constituted formal representation security requirements. Indeed, we propose an extension correspondence property, so far only authentication, other requirements, as secrecy and integrity. This generalization leads unifying view adequacy proved nding unpublished attack on Kerberos that may lead serious consequences systems adopt it.