Abstract:

Kerberos authentication is one of the information security technologies for the cloud computing security. The formal verification of the Kerberos protocol helps to discover and avoid the protocol design flaws and attacks. An automatic tool named SPEAR Ⅱ for modeling and analyzing security protocols is used to analyze the security of the Kerberos protocol. Firstly, three attack scenarios such as eavesdropping, replay and tampering are designed and characteristics of communication partners in each scenario are researched. Then, several hypothesizes are proposed, which are used as the input of a Prolog based analyzer in SPEAR Ⅱ to reason the working of the Kerberos protocol. The results show that the Kerberos protocol can keep the key safety between legal communication partners in the eavesdropping and replay attack scenarios, but the attacker can use a fake key to communicate with a legal user in the tampering attack scenario.