New mathematical model of authentication protocols and verification method based on this model

Authentication protocols are distributed algorithms designed to provide authentication of agents and the transfer of confidential information (cryptographic keys, etc.) in an in secure environment. They are used, for example, in electronic payments, electronic voting procedures, database access systems, etc. On the reason of the large financial and social damage in the case of the incorrect execution of such protocols, it is necessary to use mathematical methods to justify their correctness and security. In the present work, a new mathematical model of such authentication protocols is introduced, which provides a possibility to describe both the protocols and their properties. It is shown a possibility to solve problems of verification of authentication protocols.