This paper discusses the security of public key protocols, focusing on two types of protocols: cascade protocols and name-stamp protocols. It analyzes how these protocols can be compromised by active saboteurs who may impersonate users or alter messages. The paper introduces formal models to precisely define and analyze protocol security. For cascade protocols, the paper proves that a protocol is secure if and only if two conditions are met: (1) the messages transmitted between users contain some layers of encryption functions, and (2) in generating a reply message, each participant never applies the decryption function without also applying the encryption function. This provides a simple characterization of secure cascade protocols. For name-stamp protocols, the paper presents a polynomial-time algorithm to determine if a protocol is secure. It also extends the results to the case where a saboteur can break a protocol without waiting for others to initiate a conversation. The paper also discusses the security of protocols against impatient saboteurs, who initiate conversations but do not rely on being spoken to. It provides characterizations for both cascade and name-stamp protocols in this scenario. The paper concludes by emphasizing the importance of formal models in analyzing protocol security and highlights the need for careful design to prevent vulnerabilities to active saboteurs. It also notes that other types of sabotage may exist that can defeat the purpose of a public-key protocol.This paper discusses the security of public key protocols, focusing on two types of protocols: cascade protocols and name-stamp protocols. It analyzes how these protocols can be compromised by active saboteurs who may impersonate users or alter messages. The paper introduces formal models to precisely define and analyze protocol security. For cascade protocols, the paper proves that a protocol is secure if and only if two conditions are met: (1) the messages transmitted between users contain some layers of encryption functions, and (2) in generating a reply message, each participant never applies the decryption function without also applying the encryption function. This provides a simple characterization of secure cascade protocols. For name-stamp protocols, the paper presents a polynomial-time algorithm to determine if a protocol is secure. It also extends the results to the case where a saboteur can break a protocol without waiting for others to initiate a conversation. The paper also discusses the security of protocols against impatient saboteurs, who initiate conversations but do not rely on being spoken to. It provides characterizations for both cascade and name-stamp protocols in this scenario. The paper concludes by emphasizing the importance of formal models in analyzing protocol security and highlights the need for careful design to prevent vulnerabilities to active saboteurs. It also notes that other types of sabotage may exist that can defeat the purpose of a public-key protocol.