What is the best way to prove a cryptographic protocol correct?

In this paper, we identify that protocol verification using invariants have significant limitations such as inapplicability to some protocols, non-standard attacker inferences and non-free term algebras. We argue that constraint solving for bounded process analysis can be used in conjunction with decidability of context-explicit protocols as a verification tool and can overcome those limitations. However, this is possible only when new decidability results are obtained for protocol security, especially in presence of non-standard inferences and non-free term algebras.