本站原创
1007-0745（2012）12-0040-02
摘要：无线局域网技术把传统LAN技术、无线通信技术和移动通信技术相结合，通过网络连接使得WLAN用户可以访问有线LAN怎么写作器资源。在对我国自主研究的安全标准WAPI协议流程进行分析后，通过模型检测的方法，使用模型检查工具SPIN对WAPI协议
关键词：WLAN WAPI 模型检测协议测试
1 引言
无线局域网（WLAN）把传统LAN技术、无线通信技术和移动通信技术相结合，通过网络连接使得WLAN用户可以访问有线LAN怎么写作器资源。然而安全问题一直阻碍着WALN进入信息化应用领域的步伐。国际标准为此采用了WEP、WPA、802.1x、802.11i、VPN等方式来保证WLAN的安全，但都没有从根本上解决WLAN的安全问题。
我国在2003年5月份提出了无线局域网国际标准GB15629.11，引入一种全新的安全机制WAPI——无线局域网鉴别与保密基础结构，采用非对称（椭圆曲线）和对称（分组）体制分别用于WLAN设备的数字证书、密钥协商和传输数据的加解密，从而实现了设备的身份鉴别、链路验证、访问控制和用户信息在无线传输状态下的加密保护，很好的解决了WLAN的安全问题。
2WAPI协议的工作过程
WAPI协议由WAI（无线局域网鉴别基础结构）和WPI（无线局域网保密基础结构）两部分组成，其中：WAI包括安全策略的发现与协商、鉴别及密钥管理；WPI包括数据加密及完整性校验。
在一个采用了WAPI安全关联机制的WLAN中，当Client需要访问该WLAN时，通过被动AP的信标（Beacon）帧或主动发送探询帧（主动探询过程如图1所示）以识别AP所采用的安全策略：
若AP采用证书鉴别方式，AP将发送鉴别激活分组启动证书鉴别过程，当证书鉴别过程成功结束后，AP和Client再进行单播密钥协商和组播密钥通告；
若AP采用预共享密钥鉴别方式，AP将与Client直接进行单播密钥协商和组播密钥通告。
3协议的模型测试方法
由于一个协议的状态系统总是规模不大且是有界的，因此应用模型检测技术是可行的。把WAPI协议模拟为一个有限状态系统，从而通过彻底的研究来验证那些所有可获得的状态是否满足一些属性。
用于协议分析的模型检测技术可分为3个步骤进行：
系统建模：将协议描述（specification）转换为模型检测工具能够识别的形式化模型，如Kripke结构、有限状态机、Petri网等。
性质描述：在验证协议之前，需要描述协议必须满足的性质，通常采用时序逻辑公式来完成。时序逻辑引入时序和路径算子，并结合普通的逻辑运算，可以断言随时间变化的系统行为。
执行模型检测：验证的目的是检查协议模型是否满足协议规范，如果不满足，还应该分析其错误踪迹，即对错误进行追踪定位。
通过对协议模型的建立，可以最后建立出有效的状态模型并有利于使用模型检测工具SPIN的协议模型检测。Bell实验室开发的工具SPIN是目前应用最为广泛地模型检验工具之一。SPIN适合于并行系统，尤其是协议一致性的辅助分析验证工具。
4WAPI协议的模型测试
WAPI协议流程如下：
（1）工作站STA通过AP的信标帧（Beacon）或探寻响应帧（probe response）识别AP支持的WAI鉴别及密钥管理套件。在WAPI信息元素中，包含鉴别和密钥管理（M）套件、单播套件、组播套件、WAPI能力信息（目前只标识是否支持预鉴别）等。
（2）在识别出AP支持的WAI鉴别及密钥管理套件之后，STA和AP之间进行链路验证。链路验证分为：开始模式和预共享模式。由于预共享密钥模式之用与WEP加密的情况，所以对于WAPI来讲，链路验证都是开放模式的。
（3）链路验证完成之后，STA向AP发送关联请求帧（Association Request），在关联请求帧中包含WAPI信息元素确定选择的套件。AP随后会对关联请求帧进行处理。一旦关联请求获准，AP就会以代表成功的状态代码O及关联标识符（AID）来响应。如果关联请求失败，就只会返回状态码并中止整个过程。
（4）执行WAI鉴别过程。如果采用基于证书的认证方式，STA和AP先进行证书鉴别过程，协商出BK，然后进行单播密钥协商和组播密钥通告过程。
WAI利用证书对客户端STA和接入点AP进行双向认证，证书持有者的签名WAPI的椭圆曲线数字签名、公钥，证书包括证书颁发者ASU的公钥、签名等。WAI协议主要包括三个过程：证书鉴别过程、单播密钥协商过程、组播密钥协商过程（组播密钥相对于单播密钥具有优点，组播密钥只允许发生者对每个报文只能发送一次，可以最小化网络中报文的拷贝数）。WAI 协议主要包含3个过程：如图2所示
利用模型检测WAPI协议的基本方法是产生运行协议的一个小系统模型（如只有一个发起者和一个响应者），连同最一般的可以交互的协议的入侵者模型，并利用状态开发工具，去验证系统是否可以进入一个不安全的状态，就是说验证是否有一个入侵者者攻击协议。最后使用SPIN对WAPI协议进行形式化分析。
SPIN模拟和检验的基本过程是：使用Promela语言描述协议的性质，通过SPIN对建立的系统模型进行随意的或交互式仿真，或根据错误轨迹文件进行仿真，当检测到错误时，发出语法出错报告，使用pan.c模型检测代码进行模拟，经过编译器编译产生可执行的程序，检测器检测之后，如果不符合协议要求则产生错误的轨迹，并给出反例，系统会跳转到SPIN重新进行模拟和仿真，检测产生错误的原因。
4结束语
WAPI作为我国自主创新并拥有知识产权的安全接入技术标准，相比存在严重安全缺陷的802.11i标准，具有明显的安全和技术优势，迄今未发现安全技术漏洞。通过WAPI协议模型检测，建立一系列协议模型，最后经过成熟的模型检测工具SPIN进行了完整的验证，可看出WAPI在网络的安全性方面有很大的优势，WAPI安全机制在很大的程度上削弱了对接入点AP和AS可能实施的拒绝怎么写作攻击，使得整个WLAN认证与密钥协商过程简化并提高了效率，WAPI是一种高效的WLAN安全问题的解决方案。WAPI的鉴别过程能够保证数据的实现、身份验证、实现信息保密、接入控制的安全鉴别等安全目标，因此保证了无线网络通信的信息安全。
参考文献：
王兵，WAPI安全机制浅析[J]，计算机安全， 2011/6：75.
陈颖，陈淑春，吴小玉，浅谈WAPI及其认证技术[J]，2009/9，11（ 3）：50.
[3]李慧贤，蔡皖东，庞辽军，WAPI接入鉴别协议WAI的安全性分析和验证[J]，计算机工程，2008/2：34.
[4]陶晓明，孙树峰，薛梅，无线局域网安全认证协议研究[J]，菏泽师范专科学校学报，2004/5，26（2）：10.
摘要：无线局域网技术把传统LAN技术、无线通信技术和移动通信技术相结合，通过网络连接使得WLAN用户可以访问有线LAN怎么写作器资源。在对我国自主研究的安全标准WAPI协议流程进行分析后，通过模型检测的方法，使用模型检查工具SPIN对WAPI协议
源于：论文摘要范文www.udooo.com
进行分析和验证。关键词：WLAN WAPI 模型检测协议测试
1 引言
无线局域网（WLAN）把传统LAN技术、无线通信技术和移动通信技术相结合，通过网络连接使得WLAN用户可以访问有线LAN怎么写作器资源。然而安全问题一直阻碍着WALN进入信息化应用领域的步伐。国际标准为此采用了WEP、WPA、802.1x、802.11i、VPN等方式来保证WLAN的安全，但都没有从根本上解决WLAN的安全问题。
我国在2003年5月份提出了无线局域网国际标准GB15629.11，引入一种全新的安全机制WAPI——无线局域网鉴别与保密基础结构，采用非对称（椭圆曲线）和对称（分组）体制分别用于WLAN设备的数字证书、密钥协商和传输数据的加解密，从而实现了设备的身份鉴别、链路验证、访问控制和用户信息在无线传输状态下的加密保护，很好的解决了WLAN的安全问题。
2WAPI协议的工作过程
WAPI协议由WAI（无线局域网鉴别基础结构）和WPI（无线局域网保密基础结构）两部分组成，其中：WAI包括安全策略的发现与协商、鉴别及密钥管理；WPI包括数据加密及完整性校验。
在一个采用了WAPI安全关联机制的WLAN中，当Client需要访问该WLAN时，通过被动AP的信标（Beacon）帧或主动发送探询帧（主动探询过程如图1所示）以识别AP所采用的安全策略：
若AP采用证书鉴别方式，AP将发送鉴别激活分组启动证书鉴别过程，当证书鉴别过程成功结束后，AP和Client再进行单播密钥协商和组播密钥通告；
若AP采用预共享密钥鉴别方式，AP将与Client直接进行单播密钥协商和组播密钥通告。
3协议的模型测试方法
由于一个协议的状态系统总是规模不大且是有界的，因此应用模型检测技术是可行的。把WAPI协议模拟为一个有限状态系统，从而通过彻底的研究来验证那些所有可获得的状态是否满足一些属性。
用于协议分析的模型检测技术可分为3个步骤进行：
系统建模：将协议描述（specification）转换为模型检测工具能够识别的形式化模型，如Kripke结构、有限状态机、Petri网等。
性质描述：在验证协议之前，需要描述协议必须满足的性质，通常采用时序逻辑公式来完成。时序逻辑引入时序和路径算子，并结合普通的逻辑运算，可以断言随时间变化的系统行为。
执行模型检测：验证的目的是检查协议模型是否满足协议规范，如果不满足，还应该分析其错误踪迹，即对错误进行追踪定位。
通过对协议模型的建立，可以最后建立出有效的状态模型并有利于使用模型检测工具SPIN的协议模型检测。Bell实验室开发的工具SPIN是目前应用最为广泛地模型检验工具之一。SPIN适合于并行系统，尤其是协议一致性的辅助分析验证工具。
4WAPI协议的模型测试
WAPI协议流程如下：
（1）工作站STA通过AP的信标帧（Beacon）或探寻响应帧（probe response）识别AP支持的WAI鉴别及密钥管理套件。在WAPI信息元素中，包含鉴别和密钥管理（M）套件、单播套件、组播套件、WAPI能力信息（目前只标识是否支持预鉴别）等。
（2）在识别出AP支持的WAI鉴别及密钥管理套件之后，STA和AP之间进行链路验证。链路验证分为：开始模式和预共享模式。由于预共享密钥模式之用与WEP加密的情况，所以对于WAPI来讲，链路验证都是开放模式的。
（3）链路验证完成之后，STA向AP发送关联请求帧（Association Request），在关联请求帧中包含WAPI信息元素确定选择的套件。AP随后会对关联请求帧进行处理。一旦关联请求获准，AP就会以代表成功的状态代码O及关联标识符（AID）来响应。如果关联请求失败，就只会返回状态码并中止整个过程。
（4）执行WAI鉴别过程。如果采用基于证书的认证方式，STA和AP先进行证书鉴别过程，协商出BK，然后进行单播密钥协商和组播密钥通告过程。
WAI利用证书对客户端STA和接入点AP进行双向认证，证书持有者的签名WAPI的椭圆曲线数字签名、公钥，证书包括证书颁发者ASU的公钥、签名等。WAI协议主要包括三个过程：证书鉴别过程、单播密钥协商过程、组播密钥协商过程（组播密钥相对于单播密钥具有优点，组播密钥只允许发生者对每个报文只能发送一次，可以最小化网络中报文的拷贝数）。WAI 协议主要包含3个过程：如图2所示
利用模型检测WAPI协议的基本方法是产生运行协议的一个小系统模型（如只有一个发起者和一个响应者），连同最一般的可以交互的协议的入侵者模型，并利用状态开发工具，去验证系统是否可以进入一个不安全的状态，就是说验证是否有一个入侵者者攻击协议。最后使用SPIN对WAPI协议进行形式化分析。
SPIN模拟和检验的基本过程是：使用Promela语言描述协议的性质，通过SPIN对建立的系统模型进行随意的或交互式仿真，或根据错误轨迹文件进行仿真，当检测到错误时，发出语法出错报告，使用pan.c模型检测代码进行模拟，经过编译器编译产生可执行的程序，检测器检测之后，如果不符合协议要求则产生错误的轨迹，并给出反例，系统会跳转到SPIN重新进行模拟和仿真，检测产生错误的原因。
4结束语
WAPI作为我国自主创新并拥有知识产权的安全接入技术标准，相比存在严重安全缺陷的802.11i标准，具有明显的安全和技术优势，迄今未发现安全技术漏洞。通过WAPI协议模型检测，建立一系列协议模型，最后经过成熟的模型检测工具SPIN进行了完整的验证，可看出WAPI在网络的安全性方面有很大的优势，WAPI安全机制在很大的程度上削弱了对接入点AP和AS可能实施的拒绝怎么写作攻击，使得整个WLAN认证与密钥协商过程简化并提高了效率，WAPI是一种高效的WLAN安全问题的解决方案。WAPI的鉴别过程能够保证数据的实现、身份验证、实现信息保密、接入控制的安全鉴别等安全目标，因此保证了无线网络通信的信息安全。
参考文献：
王兵，WAPI安全机制浅析[J]，计算机安全， 2011/6：75.
陈颖，陈淑春，吴小玉，浅谈WAPI及其认证技术[J]，2009/9，11（ 3）：50.
[3]李慧贤，蔡皖东，庞辽军，WAPI接入鉴别协议WAI的安全性分析和验证[J]，计算机工程，2008/2：34.
[4]陶晓明，孙树峰，薛梅，无线局域网安全认证协议研究[J]，菏泽师范专科学校学报，2004/5，26（2）：10.