This paper analyzes the Needham-Schroeder Public-Key Protocol using the Failures Divergences Refinement Checker (FDR), a model checker for CSP. The authors use FDR to discover an attack that allows an intruder to impersonate another agent. They adapt the protocol to address this attack and then use FDR to show that the modified protocol is secure for a small system with a single initiator and responder. Finally, they prove that if this small system is secure, then a system of arbitrary size is also secure. The main contributions of the paper are two-fold: (1) demonstrating how errors can be found in security protocols using tools like FDR, and (2) showing that the security of a small system implies the security of a larger system. The paper also includes a detailed analysis of the protocol, the intruder's capabilities, and the formal methods used to verify the protocol's security.This paper analyzes the Needham-Schroeder Public-Key Protocol using the Failures Divergences Refinement Checker (FDR), a model checker for CSP. The authors use FDR to discover an attack that allows an intruder to impersonate another agent. They adapt the protocol to address this attack and then use FDR to show that the modified protocol is secure for a small system with a single initiator and responder. Finally, they prove that if this small system is secure, then a system of arbitrary size is also secure. The main contributions of the paper are two-fold: (1) demonstrating how errors can be found in security protocols using tools like FDR, and (2) showing that the security of a small system implies the security of a larger system. The paper also includes a detailed analysis of the protocol, the intruder's capabilities, and the formal methods used to verify the protocol's security.