认证协议的形式化分析*

认证协议的设计是一项十分困难的工作。国际标准化组织(ISO)一直致力于不同环境的认证协议标准的制定．本文研究用BAN逻辑形式化地分析认证协议的方法，指出BAN逻辑分析并非总是推导出正确的结论．在此基础上，本文讨论了认证协议的设计原则以及改进BAN逻辑的设想