Modeling freshness concept to overcome Replay attack in Kerberos protocol using NuSMV

Today with the tremendous growth in the era of networking, the services provided to users have become diverse. In such a distributed environment, multiple users can access multiple services simultaneously. It has therefore become essential to provide security to the services being provided along with the identity of the users. Various security protocols have been proposed and used over the years and have evolved into better versions with time. In this paper, we present a simple way to perform symbolic model checking of a widely used security protocol called the Kerberos protocol, mainly a network authentication protocol, using the NuSMV model checker. It also demonstrates how the use of the freshness concept helps to overcome a common security attack called the Replay attack in the protocol.