JUCS - Journal of Universal Computer Science 3(12): 1337-1381, doi: 10.3217/jucs-003-12-1337
Formal Analysis of the Kerberos Authentication System
expand article infoGiampaolo Bella‡, Elvinia Riccobene§
‡ Computer Laboratory, University of Cambridge, Cambridge, United Kingdom§ Dipartimento di Matematica, Universit`a di Catania, Catania, Italy

Corresponding author: Giampaolo Bella ( giampaolo.bella@cl.cam.ac.uk )

© Giampaolo Bella, Elvinia Riccobene.
This article is freely available under the J.UCS Open Content License.
Citation: Bella G, Riccobene E (1997) Formal Analysis of the Kerberos Authentication System. JUCS - Journal of Universal Computer Science 3(12): 1337-1381. https://doi.org/10.3217/jucs-003-12-1337
Open Access
Abstract
The Gurevich's Abstract State Machine formalism is used to specify the well known Kerberos Authentication System based on the Needham-Schroeder authentication protocol. A complete model of the system is reached through stepwise refinements of ASMs, and is used as a basis both to discover the minimum assumptions to guarantee the correctness of the system and to analyse its security weaknesses. Each refined model comes together with a correctness refinement theorem.
Keywords
Formal Methods, Security, Protocol specification, Refinement, Protocol verification, Key distribution protocol, Gurevich's Abstract State Machine, Kerberos.