This paper analyzes the Needham-Schroeder Public-Key Protocol using FDR, a refinement checker for CSP. The protocol is used to establish mutual authentication between an initiator A and a responder B. The paper uses FDR to discover an attack that allows an intruder to impersonate another agent. The protocol is then adapted to prevent this attack, and FDR is used to show that the new protocol is secure for a small system. The paper also proves that if the small system is secure, then a system of arbitrary size is also secure. The attack discovered by FDR is more subtle than previously known attacks on the full protocol. The paper also discusses the use of process algebra tools for analyzing security protocols and highlights the importance of formal methods in verifying protocol security. The main contributions are the study of how errors can be found in security protocols using FDR and how a protocol running on a system of arbitrary size can be verified by considering a small system. The paper concludes that the protocol is secure under the assumptions made about encryption and key management.This paper analyzes the Needham-Schroeder Public-Key Protocol using FDR, a refinement checker for CSP. The protocol is used to establish mutual authentication between an initiator A and a responder B. The paper uses FDR to discover an attack that allows an intruder to impersonate another agent. The protocol is then adapted to prevent this attack, and FDR is used to show that the new protocol is secure for a small system. The paper also proves that if the small system is secure, then a system of arbitrary size is also secure. The attack discovered by FDR is more subtle than previously known attacks on the full protocol. The paper also discusses the use of process algebra tools for analyzing security protocols and highlights the importance of formal methods in verifying protocol security. The main contributions are the study of how errors can be found in security protocols using FDR and how a protocol running on a system of arbitrary size can be verified by considering a small system. The paper concludes that the protocol is secure under the assumptions made about encryption and key management.