We present an overview of techniques for verifying key-exchange and authentication protocols. In the past, these protocols were considered `safe until broken', but current techniques assist the protocol designer during the design phase, and allow for thorough, and often automatic, verification. We describe five major families of formal methods: finite-state machines, methods not originally designed to analyze cryptographic protocols, logics of knowledge ad belief, formal models based on algebraic term rewriting, complexity-theoretic approaches, and hybrid methods thereof. We look at the safety properties they assess, e.g. secrecy of a session key, and the scope of the analysis. We show examples of protocol analysis, from simple cases as the Needham-Schroeder protocol to more complex ones as SSL 3.0.