This paper presents a logic for analyzing authentication protocols, which allows for the formal description of the beliefs of trustworthy parties involved in such protocols and the evolution of these beliefs as a consequence of communication. The authors describe a logic that enables them to explain authentication protocols formally, discover subtleties and errors in them, and suggest improvements. They analyze four published protocols, chosen either because of their practical importance or because they serve to illustrate their method. The logic is based on a many-sorted model and includes constructs for beliefs, seeing, saying, and controlling. It also includes rules for deriving beliefs about the origin of messages, verifying nonces, and handling jurisdiction. The authors transform protocols into an idealized form for analysis, which is more precise and complete than traditional descriptions. The paper analyzes several authentication protocols, including Kerberos, Andrew Secure RPC, Needham-Schroeder, and X.509. It identifies weaknesses in these protocols, such as the possibility of replay attacks and the lack of guarantees for message timeliness. The authors suggest improvements, such as adding timestamps and ensuring the freshness of nonces. The paper concludes that a formal logic is essential for ensuring the correctness of authentication protocols, as their design is often error-prone. The logic allows for the systematic analysis of protocols and the identification of subtle issues that may be overlooked in informal descriptions. The authors hope that protocol designers will build on their techniques to suit their specific needs.This paper presents a logic for analyzing authentication protocols, which allows for the formal description of the beliefs of trustworthy parties involved in such protocols and the evolution of these beliefs as a consequence of communication. The authors describe a logic that enables them to explain authentication protocols formally, discover subtleties and errors in them, and suggest improvements. They analyze four published protocols, chosen either because of their practical importance or because they serve to illustrate their method. The logic is based on a many-sorted model and includes constructs for beliefs, seeing, saying, and controlling. It also includes rules for deriving beliefs about the origin of messages, verifying nonces, and handling jurisdiction. The authors transform protocols into an idealized form for analysis, which is more precise and complete than traditional descriptions. The paper analyzes several authentication protocols, including Kerberos, Andrew Secure RPC, Needham-Schroeder, and X.509. It identifies weaknesses in these protocols, such as the possibility of replay attacks and the lack of guarantees for message timeliness. The authors suggest improvements, such as adding timestamps and ensuring the freshness of nonces. The paper concludes that a formal logic is essential for ensuring the correctness of authentication protocols, as their design is often error-prone. The logic allows for the systematic analysis of protocols and the identification of subtle issues that may be overlooked in informal descriptions. The authors hope that protocol designers will build on their techniques to suit their specific needs.