: As soon as major protocol flaws were discovered empirically -- a good luck that is not older than the early 1990s -- this title question came up to the world. It was soon realised that some notion of formal correctness was necessary to substantiate the confidence derived from informal analyses. But protocol correctness was born in a decade when security in general was only beginning to ferment. Security protocols aim at a large variety of goals. This is partly due to the increasing domains where the protocols are finding an application, such as secure access to localarea network services, secure e-mail, e-commerce, public-key registration at certification authorities and so on. Also, several interpretations are possible about each goal. Clearly, it is impossible to study protocol correctness profitably without a universal and unambiguous interpretation of its goals. What may be typical of security problems is that it is at least as important to state a detailed and appropriate model ...