The original BAN logic has proved successful for finding many unintended errors in security protocols. It does, though, not spot all potential security breaches and thus is less suited for finding intentional (possibly malicious) errors.
Our formalism resulted from a systematic attempt to formulate precise restrictions under which the changing beliefs of principals during a protocol run accurately reflect the changing state of affairs while communication takes place. The restrictions that emerged from our investigation are rather unelegant and complicated, the reason being that we wanted to keep them such that they can be checked statically and do not exclude well-known examples of protocols. They are, however, necessary; for most of the restrictions we have an example of a simple concrete protocol (not obeying the restriction) that leads to a false conclusion.
The semantic correctness criterium we have formulated is weak; it does not take the threats imposed by intruders and impostors into account. It remains to be investigated whether a stronger correctness criterium requires further restrictions. Extrapolating from our experience, we think in fact that that is rather likely. In view of the complications already engendered, an appropriate question is whether the approach of translating protocols into a logical framework is the most felicitous one.