随着互联网的迅速发展,网络协议的安全性越来越成为人们关注的焦点。IEEE802.1X协议作为以太网上主要的接入认证协议,其安全性的重要性显而易见。形式化方法作为一种重要的软件及协议的安全性分析工具,以其准确性的特点已成为检验网络协议安全性的重要途径。常见的形式化方法有模型检测,逻辑推理以及定理证明。本文使用著名的模型检测工具SPIN(Simple Pro me la Interpreter)对IEEE802.1X协议进行形式化分析与验证,指出协议存在的安全漏洞,并提出改进方案。本文首先对IEEE802.1X协议使用Promela语言建模,并根据实际情况抽象出网络的攻击模型,对攻击者建模,然后用线性时态逻辑对协议的安全性属性进行了描述,给出了解决方案,并再次使用SPIN对修正过的协议模型进行验证。