When you try to verify security protocols you have to do a lot of different steps like formalizing a simpler version based on a extremely complex real protocol using some extended Dolev Yao model. Afterwards you have to look for a tool and a programming language to map your algebraic model to it like "*.csp". Somewhere in between you have to limit the capabilities of the attacker and sometimes even the all the other participants/agents without removing parts of the protocol that could possibly reveal vulnerabilities of the protocol.
What are the most difficult steps - regarding time - trial and error processes and so on when trying to verify a modern protocol. I don't want to know the opinion of someone who stuck in the process but more the objective view of the expected complexities of the process. Also I would like to know if I missed important steps in my description in my first paragraph.