Modeling Kerberos Authentication Protocol Using Colored Petri Net

Abstract

Information security is essential in today's digital world and plays an important role in message exchanges and trading. Authentication protocols play an important role in information security. Kerberos is one of the famous and commonly used authentication protocols. These factors cause attention of many researchers for formal modeling and analyzing of security properties of this protocol. Colored Petri net is powerful formal modeling language with great modeling capabilities and is one of the suitable methods for verifying properties of various systems like security protocols. Hierarchical modeling of Kerberos authentication protocol version 5 using colored Petri net is presented in this paper. Operations and messages of Kerberos protocol are modeled with full detailes. Presented model can be extended easily for studying different properties of this protocol and its strength against various attacks.