Frederick Butler, Iliano Cervesato, Aaron D. Jaggard, Andre Scedrov: Verifying Confidentiality and Authentication in Kerberos 5. ISSS 2003: 1-24