Abstract: Authentication protocols are very basic and pivotal in systems of network security. This paper presents a new authentication protocol based on traditional approach, then does formal analysis for it by BAN logic, and shows an attack mode to it and amend it. At the end it discusses the actions of BAN logical analysis in authentication protocols, besides the limitations and the direction for further improvement.

Key words: Authentication protocol; Formal analysis; BAN logic

摘要： 认证协议是网络安全体系中最基本和最关键的问题。在传统认证协议的基础上，提出了一个新的认证协议。经过用BAN 逻辑对这个协议进行了形式化分析，找出了可能的攻击方法并作出了相应修改。讨论了BAN 逻辑用于认证协议形式化分析的作用、局限性以及改进的方向。

关键词: 认证协议；形式分析；BAN 逻辑