Public Wireless Lan Security System And Its Experience In Security Formal Analysis

The public wireless local area network (PWLAN), which can provide convenient high-speed wireless access to the Internet in'hot spots'such as airport, park and business quarter,is becoming one of the most interesting techniques in wireless network area. It would helppeople to enjoy high efficiency, high quality and low business cost mobile network services atanytime and anywhere. The security of PWLAN is the mainly concerned aspect in PWLANresearch. The problems which should be solved urgently include how to design and realizethe PWLAN security system, how to provide theoretic instruction in security protocols de-sign, and how to guarantee the PWLAN security. The proofs of security protocols validitybased on formal analysis methods are discussed in this dissertation. Especially, the securityperformances of security protocols adopted in PWLAN architecture are concretely comparedwith each other based on the conclusions of these proofs. The research in this dissertationincludes following aspects:1. The research on the PWLAN architecture: With a wide survey on the existing PWLANapplication pattern and system structure, we generalize the PWLAN into ISP-ownedPWLAN, Operator PWLAN and PWLAN for Enterprise. A PWLAN security systemarchitecture based on controller mode is proposed to meet the need of all PWLANtypes. Furthermore, the rational analysis of this system design is discussed after study-ing the component of the system structure and corresponding security mechanisms.2. The research on the correctness analysis and validity analysis of WEP and TKIP proto-cols: Concrete security analyses of WEP, TKIP and CCMP protocols are provided here.There are two aspects of security in our analysis: privacy and authenticity. We quantifythe security provided by these protocols as the advantage of attack successful probabil-ity and a function of the security of the underlying cipher. It is showed that while theadvantage of attack successful probability to RC4 algorithm is O(n²) * 2^-128, the ad-vantage of attack successful probability to WEP algorithm is approximate O(n²)*2^-24and the advantage of attack successful probability to TKIP is approximate O(n³)*2^-48.The conclusion is that both WEP and TKIP protocols do not provide a level of privacythat satisfies the PWLAN environment.3. The research on the enhancement of TKIP protocol: We enhance the TKIP algorithmby increasing the space of the TKIP sequence counter (TSC) from 48bits to 128bits. Itis showed that the security strength of this enhanced algorithm is 3 magnitudes higherthan RC4 algorithm.4. The research on the security analysis on privacy and authenticity of CCMP protocol:The concrete bounds for the security of CCMP are presented in terms of the security ofthe AES algorithm. The result is that while the advantage of attack successful probabil-ity to AES algorithm is O(n²) * 2^-128, the advantages of attack successful probabilityon authenticity and privacy are approximate O(n)*2^-64 and O(n²)*2^-128. It achievesthe anticipated design goals and satisfies the security requirements of the PWLAN.5. The research on the security analysis of key exchange protocol. We make a provablesecurity analysis of key exchange protocol with the Bellare-Rogoway model. It isshowed that the 4-way handshake protocol adopted in PWLAN does indeed bringingsignificant, provable security gains in practical situations.6. The research on the security analysis of authentication protocol. We proposed an ex-pansion Bellare-Rogoway model to analyze the provable security of 802.1X authentica-tion protocol. A security problem was found and the corresponding man-in-the-middleattack is given here. Furthermore, some proposed solutions are presented to preventthe discussed attack.7. The research on the design and realization of access point and controller: The designsand realizations of wireless access point and controller are discussed at the end of thisdissertation. The designs of these devices are confirmed with the PWLAN technologycriterion.