公共无线局域网（PWLAN）是目前无线网络技术发展的热点之一,旨在给用户提供随时随地高效率、高质量、低成本的移动接入,其安全性直接影响到公共无线局域网技术的推广应用。如何设计和实现公共无线局域网的安全体系,为其安全协议的设计与分析提供理论指导,从而确保公共无线局域网的安全是目前迫切需要解决的问题。本文采用形式化分析手段,对当前公共无线局域网安全协议的安全性进行证明,并比较不同协议的安全性能,从而为选择合适的安全协议提供依据。为此,本文开展了以下几个方面的研究:1.通过对公共无线局域网现有应用模式和体系结构的分析,将公共无线局域网归纳为:WISP-owned PWLAN、Operator PWLAN以及PWLAN for Enterprise三种类型。在此基础上,提出了一个可以基本满足各种类型公共无线局域网需求的基于接入控制器模式的通用公共无线局域网安全体系结构,给出了该体系设计的合理性分析。2.根据预言机模型,从协议的机密性和可靠性两方面,对WEP、TKIP以及CCMP密码协议进行了精确量化的可验安全性形式化分析;推导出WEP、TKIP和CCMP协议的安全量化函数,该函数采用攻击成功率的优势函数来衡量加密机制的安全性能。分析表明,当攻击RC4算法的成功率为O（n2） * 2^-128（密钥长度为128比特）时,WEP的攻击成功率约为O（n²） * 2^-24,TKIP的攻击成功率约为O（n³） * 2^-48,这两个加密协议都没有达到提供预期的安全强度。3.提出了TKIP算法的一种改进算法。在该算法中把TKIP序列计数器（TSC）值由原来的48比特扩大到128比特,使其安全强度比RC4算法提高了约3个数量级。4.证明了CCMP加密协议的安全性和可靠性。分析表明,当AES算法的攻击成功率为O（n²） * 2^-128时,CCMP的可靠性和机密性对应的攻击成功率分别为O（n） * 2^-64和O（n2） * 2^-128,达到了预期的设计目标,可以满足公共无线局域网的安全需求。5.利用Bellare-Rogoway模型,对密码交换协议进行了可验安全性分析。证明了公共无线局域网采用的四步握手密钥交换机制的保密性和认证正确性;6.提出了一种增强的Bellare-Rogoway模型。采用该模型对802.1X认证协议进行了可验安全性分析,发现了该协议存在安全缺陷,容易遭受中间人攻击。在此基础上提出了一种攻击方法及改进措施。7.设计和实现了符合公共无线局域网技术规范的无线接入点和接入控制器。