Formal Analysis of the Kerberos Authentication Protocol.

The security of cryptographic protocols has traditionally been verified with respect to one of two mathematical models: One, known as the Dolev-Yao or symbolic model, abstracts cryptographic concepts into an algebra of symbolic messages. Methods based on the Dolev-Yao abstraction, which make use of simple formal languages or logics, have been successfully applied to discover structural flaws in numerous cryptographic protocols, and have also become efficient and robust enough to tackle large commercial protocols, often even automatically. The other, known as the computational or cryptographic model, retains the concrete view of messages as bitstrings and cryptographic operations as algorithmic mappings between bitstrings, while drawing security definitions from complexity theory. Proofs in the computational approach entail strong security guarantees, however, only simple cryptographic protocols, mainly of academic interest, have been verified with respect to the computational model. This dissertation contributes to the ongoing case study of the Kerberos 5 protocol suite, a widely used authentication protocol. We report on a man-in-the-middle attack on PKINIT, the public key extension of Kerberos, which allows an attacker to impersonate Kerberos administrative principals (KDC) and end-servers to a client and also gives the attacker the keys that the KDC would normally generate to encrypt the service requests of this client, hence defeating authentication and confidentiality guarantees of Kerberos. We have formally verified several possible fixes to PKINIT that prevent our attack using the symbolic Multiset Rewriting formalism. We also present proofs of the full Kerberos 5 suite with and without its public-key extension for the first time in the more detailed Dolev-Yao dialect of the BPW model. These proofs may be used to gain computationally sound results. Furthermore, we present a computationally sound mechanized analysis of Kerberos 5, both with and without its public-key extension PKINIT, using the prover CryptoVerif, which works directly in the computational model. We obtain proofs of authentication and key secrecy properties that are the first mechanical proofs of a full industrial protocol at the computational level. We generalize the notion of key usability, which, although weaker than the standard notion of key indistinguishability, guarantees under certain assumptions that a key can be securely used for cryptographic operations, and show that this definition is satisfied by keys in Kerberos.