Analysing the Kerberos Timed Authentication Protocol Using CSP-Rank Functions

Despite advances in network security, malicious attacks have shown a significant increase in recent times. Authentication mechanisms coupled with strong encryption techniques are used for security purposes; however, given sufficient time, well-equipped intruders succeed in breaking encryptions and compromising system security. The protocols often fail when they are analysed critically. Formal approaches have emerged to analyse protocol failures. Communicating Sequential Processes (CSP) is an abstract language designed especially for the description of communication patterns. A notion of rank functions is introduced for analysing purposes as well. This paper presents an application of this formal approach to a newly designed authentication protocol that combines delaying the decryption process with timed authentication while keys are dynamically renewed under pseudo-secure situations. The analysis and verification of authentication properties and results of the designed protocol are presented and discussed.