Abstract Formal Methods for Security Protocols: Three Examples of the Black-Box Approach C.J.F. Cremers, S. Mauw and E.P. de Vink Security protocols are hard to design, even under the assumption of perfect cryptography. With the `classical' Needham-Schroeder protocol as leading example, three so-called black-box approaches to the formal verification of security protocols are sketched. BAN-logic is a light-weight method under the assumption of honest agents and a passive intruder. The Casper/FDR approach translates a high-level description of a security protocol, together with its security requirements and a particular instantiation into CSP, that can be machine-verified using the FDR model checker. In this approach the intruder is in control of the network and is allowed to participate as one of the agents. The same holds for the strand space approach. By focusing on the causal dependency of actions and message passing, one aims to prove security properties of general class of protocols instantiations at the