Survey on Formal Analysis of Kerberos 5
Ti Zhou · 2009
Network Authentication Protocol Kerberos 5 provides us with a third-party authentication mechanism.The protocol was designed to allow a client to repeatedly authenticate herself to multiple network servers based on a single login.Nowadays this protocol has been widely used in Windows serials as well as FreeBSD and Linux system for network authentication.As a result,the security properties of it attract great attention.Since the protocol adopts timestamp and involves four participants,how to formally analyze and verify its security comes to be a hot and hard research point.Many methods were carried out internationally,which can be divided into two main approaches:one based the symbolic model and another based on the computational model.This paper introduced and analyzed typical formally work on analyses of Kerberos 5 over the world across-the-board and systematically,finally showed out our current research effort.