A State Transition Model for Honest Executions of Authentication Protocols

Cryptographic protocols are very good tools to achieve authentication in large distributed computer network. These protocols are precisely defined sequences of actions (communication and computation steps) which use some cryptographic mechanism such as encryption and decryption. It is well known that the design of authentication cryptographic protocols is error prone. Several protocols have been shown flawed in computer security literature. Due to this it is necessary to have some methods of analysis and properties verification of these protocols. It is obvious that in investigations of these properties a suitable formal model is needed. This model should express all important properties and ideas of protocols. Usually size of modeIs introduced by many people is very huge and searching of these modeIs is impossible. In this paper we propose a new formal model of honest executions of cryptographic authentication protocol. To decrease number of states in our model we propose some partial order reduction. We hope that this model is a good startpoint for further investigations and will be usefull in verification of real executions of cryptographic protocols.