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. © Springer Pub. Co.
Formal analysis of the kerberos authentication system
Bella G.
;Riccobene E.
1997-01-01
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. © Springer Pub. Co.File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
