Provable-security analysis of authenticated encryption in Kerberos