随着信息技术的发展,互联网技术日益向无线网络迁移,无线应用日益普及,无线网络的安全越发重要。无线技术的技术基础、应用环境,与传统的有线网络有所区别,有线网络里成熟的安全技术不能直接适用于无线网络;同时,无线网络的特殊性,自身也衍生出新的攻击模式和安全漏洞。目前,普遍使用IEEE802.11n无线网络标准建立无线网络,该标准使用IEEE2004 802.1X协议对网络里的接入设备认证,同时使用CCMP算法进行加密,协议对不同的应用提出各自的密钥分发协议,保证密钥的新鲜性和秘密性。形式化方法是安全协议验证的一个强有力的工具,应用形式化方法来分析安全协议,是当今安全协议分析的重要技术。形式化方法分为:符号方法和计算方法。计算方法基于计算复杂性和概率理论,可以建立密码学可靠的证明。本文使用Blanchet演算为基础的CryptoVerif工具对IEEE802.11n标准进行验证,主要工作如下:1)详细介绍了802.11n标准使用的加密算法、身份认证协议、密钥协商协议,重点介绍了身份认证协议、直连密钥协商协议和组密钥协商协议。2)介绍了Blanchet演算和CryptoVerif工具,包括语法和形式化语义、类型系统、观察等价,Game转换。3)使用CryptoVerif工具对802.11n标准里身份认证协议和直连密钥协议进行验证,并提出基于公钥系统的直连密钥协商协议,对其使用CryptoVerif验证。