An Approach for Formal Verification of Authentication Protocols

Authentication protocols (APs) are one of the most important components of secure information systems. Authentication Protocols are distributed algorithms intended for secure authentication of users in an insecure environment. They are used, for example, in electronic payments, electronic voting procedures, systems of confidential data processing, etc. Errors in APs can bring to great financial and social damage, therefore it is necessary to use mathematical methods to substantiate the correctness and safety of APs. In this paper, a process model of APs is presented, which allows one to formally describe APs and their properties. It is shown how to solve the problems of verification of APs on the base of this model.