We illustrate a number of verification methods using an example: how we recently analyzed a security protocol for a Danish company, found a vulnerability, and proved the security of the fixed protocol. The methods include a popular abstract interpretation approach, the adaptation for analysis of complex stateful systems, the integration into a mathematical proof checker, and compositional reasoning. We also present how an Alice-and-Bob style language can be used - without a background in logic - for making precise specifications, verify them, and automatically generate secure-by-design implementations.