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

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