Does anyone still use BAN or GNY logic in practice?

Question

I want to implement a simple protocol, and I'd like to verify it through BAN or GNY logic. I would assume that if these logics are still used that there would be some programs available that would automate this. In fact I found one paper on how to automate GNY logic, and another mentioning a tool called SPEAR that automates BAN and GNY logic, but in no case could I actually find these tools.

All of these references are pretty old, and it looks like these logics are only used academically. Are there any examples of more modern or practical use of these, and are there any tools that are available for automating them?

Answer 1

I don't think they are even used academically anymore, possibly because of soundness problems and limited expressivity. I would not recommend this approach.