Formal Analysis of the Kerberos Authentication System
Дата
Авторы
Bella,Giampaolo
Riccobene,Elvinia
Journal Title
Journal ISSN
Volume Title
Издатель
Journal of Universal Computer Science
Аннотация
Описание
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.
Ключевые слова
Formal Methods , Security , Protocol specification , Refinement , Protocol verification , Key distribution protocol , Gurevich's Abstract State Machine , Kerberos.