The version of Kerberos presented by Burrows et al. [5] is fully mechanised using the Inductive Method. Two models are presented, allowing respectively the leak of any session keys, and of expired session keys. Thanks to timestamping, the protocol provides the involved par-ties with strong guarantees in a realistically hostile environment. These guarantees are supported by the generic theorem prover Isabelle. 1