The Formal Verification And Improvement Of 802.1X Protocol Based On SPIN

With the rapid development of Internet, the security of network protocol become the focus of attention. As the main access authentication protocol, the importance of IEEE802.1X protocol's security is obvious. Formal method is an important software and protocol analysis and verification tools. Formal method includes model checking, logic inference and theorem-proving. This paper uses the famous model checking tool SPIN (Simple Promela Interpreter) to check and verify IEEE 802.1X network protocol in order to find out the flaws of this protocol and give an improved solution to prevent these flaws.Firstly, IEEE802.1X network protocol with attacker is modeled by Promela formal language based on the reality. Secondly, LTL (Linear Temporal Logic) formula is used to describe the properties of IEEE802.1X. Finally, SPIN is used to verify this model and give an improved solution.