| 用分布式时序逻辑形式化分析IEEE802.11i协议 |
| |
| 引用本文： | 杨琳琳,周勇.用分布式时序逻辑形式化分析IEEE802.11i协议[J].南通大学学报(自然科学版),2010,9(3). |
| |
| 作者姓名： | 杨琳琳 周勇 |
| |
| 作者单位： | 南京航空航天大学,信息科学与技术学院,江苏,南京,210016 |
| |
| 基金项目： | 江苏省自然科学基金项目 |
| |
| 摘 要： | 基于Caleiro提出的分布式时序逻辑,在其模型中增加了挑战问题集合和挑战应答集合,将IEEE802.11i协议转化为分布式时序逻辑的事件结构语义模型.形式化分析并证明了该协议的保密性以及协议中申请者、认证者、认证服务器之间的相互认证性.结果表明,IEEE802.11i协议是安全的.
|
| 关 键 词： | 分布式时序逻辑 形式化分析 IEEE802.11i协议 网络模型 |
Formal Verification of IEEE802.11i Protocol Using Distributed Temporal Logic Formalization |
| |
| Authors: | YANG Lin-lin ZHOU Yong |
| |
| Abstract: | |
| |
| Keywords: | |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
