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.

  • I created the formal-verification tag, thanks for mentioning that! It seems to be an established term to describe what you are talking about, and I don't see any other tag that already covers it. (Note, I've edited a few other questions that I think could benefit from this tag.) – Luc Feb 2 at 14:21

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.