摘要： 安全协议的验证对确保网络通信安全极其重要，形式化分析方法使得安全协议的分析简单、规范和实用，成为信息安全领域的研究热点。针对802.1x/EAP-MD5认证协议，提出一种基于着色Petri网(CPN)的安全协议形式化验证方法，并给出具体的形式化分析过程。建立协议的CPN模型，分析协议执行过程中可能出现的不安全状态，利用CPN状态可达性判定这些不安全状态是否可达，从而验证协议的安全性。对于802.1x/EAP-MD5协议在中间人攻击下的安全漏洞问题，提出协议的改进方案，采用预共享密钥机制生成会话密钥加密交互信息，同时运用数字证书对服务器进行认证，以提升中间人攻击的难度及增强网络接入认证协议的安全性。

关键词: 着色Petri网, 安全协议, 形式化分析, EAP-MD5协议, 可达性分析, 中间人

Abstract: Safety verification of security protocol is extremely important to ensure the safety of the network communication. Formal analysis makes it simple, standard and practical, which becomes one of research hotspots in the field of information security. A Colored Petri Net(CPN)-based verification approach to the 802.1x/EAP-MD5 authentication protocol is proposed. The protocol is modeled by CPN, and then the potential insecure state is analyzed during the run of protocol. The reachability of insecure state is judged by the reachability analysis of CPN. After analyzing the protocol, it presents an improved protocol to eliminate the discovered vulnerabilities of 802.1x/ EAP-MD5, which generates the session key encryption communication information by using pre-shared key mechanism, and improves the difficulty of Man in the Middle(MITM) and strengthens security of the network access authentication protocol by using digital certificate to the server for authentication.

Key words: Colored Petri Net(CPN), security protocol, formal analysis, EAP-MD5 protocol, reachability analysis, Man in the Middle (MITM)

中图分类号: 

• TP393