摘要： BAN 逻辑可以证明协议是否能够达到预期目标，还能够发现协议中存在的一些缺陷，为进一步改进提供参考。但是，通过一个认证协议的例子证明，该文指出，BAN 逻辑对于诸如弱密钥方面存在的密钥猜测攻击的分析存在缺陷，还需结合非形化的方法来加以解决。

关键词: BAN 逻辑；认证协议；密钥猜测攻击；椭圆曲线

Abstract: BAN logic can prove whether a protocol can reach expected target and find some defects in the protocol, which helps the protocol get further improvement. However, this paper points out a drawback of BAN logic analysis in key guessing attacks though proving an authentication protocol with BAN logic. In this case, non-formal methods are needed in the analysis together

Key words: BAN logic; Authentication protocol; Key guessing attack; Elliptic curve