Go home now Header Background Image
Submission Procedure
share: |
Follow us
Volume 3 / Issue 12

available in:   PDF (481 kB) PS (152 kB)
Similar Docs BibTeX   Write a comment
Links into Future
DOI:   10.3217/jucs-003-12-1337


Formal Analysis of the Kerberos Authentication System

Giampaolo Bella (Computer Laboratory, University of Cambridge, UK)

Elvinia Riccobene (Dipartimento di Matematica, Universit`a di Catania, ITALY)

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, Gurevich's Abstract State Machine, Kerberos., Key distribution protocol, Protocol specification, Protocol verification, Refinement, Security

Categories: C.2.2, D.