802.11i standard is proposed by IEEE 802.11 Standard Group to improve the security of the WLAN. In 802.11i, 802.1x standard is used for the authentication and access controll. How to analyze the security of the new protocol to prove its validity is the most interesting problem we are concerned. In order to solve this problem, an expanded Bellare-Rogaway model is established to give a provable security formal analysis on this protocol. By utilizing the expanded Bellare-Rogaway model, a flaw has been found in 802.1X authentication protocols and the corresponding man-in-the-middle attack is given here.