是否还有人在实践中使用禁令或GNY逻辑？

Question

我想实现一个简单的协议，我想通过BAN或GNY逻辑来验证它。我假设，如果仍然使用这些逻辑，就会有一些程序可以自动实现这一点。事实上，我找到了一篇关于如何自动化GNY逻辑的论文，另一篇文章提到了一个叫做SPEAR的工具，它使BAN和GNY逻辑自动化，但在任何情况下我都找不到这些工具。

所有这些参考资料都很古老，看起来这些逻辑只在学术上使用。是否有任何更现代或实际使用这些工具的例子，以及是否有任何工具可用于自动化？

Answer 1

我认为他们甚至不再是学术上使用，可能是因为健全的问题和有限的表现力。我不建议这样做。