Abstract: It has been proved in many researches that there are some design flaws in IEEE 802.1X standard. In order to eliminate the Denial of Service (DoS) attack, replay attack, session hijack, Man-In-the-Middle (MIM) attack and other security threats, the protocol was analyzed in view of the state machines. It is pointed out that the origin of these problems is the inequality and incompleteness of state machines as well as the lack of integrity protection and source authenticity on messages. However, an improvement proposal called Dual-way Challenge Handshake and Logoff Authentication was proposed, and a formal analysis was done on it with an improved BAN logic. It is proved that the proposal can effectively resist the security threats mentioned above.

Key words: Network Access Control (NAC), IEEE 802.1X standard, Extensible Authentication Protocol (EAP), state machine, formal analysis, BAN logic

摘要： IEEE 802.1X标准存在一些设计缺陷,为消除拒绝服务攻击(DoS)、重放攻击、会话劫持、中间人攻击等安全威胁,从状态机运行角度对协议进行了分析,指出产生这些问题的根源在于协议状态机的不平等和不完备,缺乏对消息完整性和源真实性的保护。提出并实现了一种双向挑战握手及下线验证的改进方案,并用一种改进的BAN逻辑对其进行了形式化分析。经验证,该方案能有效抵御上述安全威胁。

关键词: 网络访问控制, IEEE 802.1X标准, 可扩展认证协议, 状态机, 形式化分析, BAN逻辑