Formal Verification of the 802.11i Authentication Protocols by Model Checking
Dafang Zhang · Computer Engineering and Science · 2010
It is important to guarantee the correctness of security protocols to ensure the security-sensitive businesses on the Internet. The formal method is useful to analyze and verify security protocols. It can uncover bugs which are difficult to find by testing. As a formalized method,model checking has many advantages. It is fully automatic,and also can provide faulty traces. An approach to abstracting and modeling the EAP-TLS of 802.11i is presented by using model checker SPIN,and a formalized model of at a significant level of detail is extracted.The security properties of the protocol for verification are extracted using LTL to find if the security properties are true in the model. A way to model authentication protocols using PROMELA is presented.