I have been playing with [old link: http://www.avispa-project.org] AVISPA recently, a tool to model protocols and check them for security vulnerabilities. Overall this is quite an impressive piece of software. The installation is painless, the documentation is good, and it has some neat features, like the presentation of attack traces as Message Sequence Charts.
It is quite amazing, and scary, how even the most trivial protocols (I tried some with just a handful of messages) are subject to non-obvious attacks. However, I am still not convinced that tools like AVISPA, certainly in their current incarnations, are good enough to find these attacks without the user having thought of them in the first place. In my, admittedly limited, experience, vulnerabilities are usually found in the process of constructing a formal model. Checking the model merely serves as a confirmation. Indeed it is often the case that some effort is required to bend the model into a shape that allows the model checker to detect the attacks.