Different approaches for the formal definition of authentication property

Security goals should be parts of the description of security protocols. If the security goal cannot be precisely described in the narration, formal verification will lose its sense. But unlike secrecy, authentication property is rarely made clear precisely what it means. Various approaches were previously proposed for the formal definition of authentication property. This article describes taxonomy of these different definitions and discusses their respective problems. It is intended to be a survey and arise some deeper research.