Extensional goals seem more important for the protocol designer than intensional ones. It has been suggested in this paper that attacks should be measured by whether or not they violate extensional specifications, even if intensional specifications have been used to find the attacks in the first place. It has been shown that it is possible to find extensional specifications for entity authentication. It is a challenge to formalise the work in this paper to provide ways prove that extensional goals are satisfied. It may be useful to find extensional specifications for other more complex protocols, such as those being proposed for electronic commerce payments.