Provable-security analysis of authenticated encryption in Kerberos

Kerberos is a widely deployed network authentication protocol currently being considered for standardisation. Many works have analysed its security, identifying flaws and often suggesting fixes, thus promoting the protocol´s evolution. Several recent results present successful, formal methods-based verifications of a significant portion of the current version, v.5 and some even imply security in the computational setting. For these results to hold, encryption in Kerberos should satisfy strong cryptographic security notions. However, prior to the authors´ work, none of the encryption schemes currently deployed as part of Kerberos, nor their proposed revisions, were known to provably satisfy such notions. The authors take a close look at Kerberos´ encryption, and they confirm that most of the options in the current version provably provide privacy and authenticity, although some require slight modifications which they suggest. The authors´ results complement the formal methods-based analysis of Kerberos that justifies its current design.