ProVerif is a fully automated tool to prove classical security properties (secrecy and authentication) on formal models of cryptographic protocols in a Dolev-Yao environment. With ProVerif, one writes a formal model of a cryptographic protocol in the applied pi-calculus, defines the security properties that the protocol should guarantee, and finally runs the tool to check whether the desired properties are actually fulfilled. The outcome could be "yes", "cannot tell" (with or without a counter-example) or the tool may run indefinitely.
After giving an overview of the underlying Dolev-Yao model and the applied pi-calculus, we will illustrate the features of the tool and how to use it. A comprehensive example of the SSH Transport Layer Protocol will be analysed: this will allow us to show some caveats and subtleties of the tool, and to share the lessons we have learnt by experiencing with it, in order to turn a "cannot tell" outcome to "yes".