2
$\begingroup$

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?

$\endgroup$
1
$\begingroup$

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

|improve this answer|||||
$\endgroup$

Your Answer

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

Not the answer you're looking for?Browse other questions tagged or ask your own question.