协议抗拒绝服务攻击性自动化证明

• 来源期刊: 通信学报
• 学科: 工学
• 关键词: 拒绝服务攻击 形式化 自动化证明 协议状态
• 年，卷（期）: 2012,（3）
• 页码范围: 112-121
• 页数: 10页
• 分类号: TP393.08
• 语种: 中文

摘要

首先从攻击者上下文与进程表达式2个方面对标准应用PI演算进行扩展,然后从协议状态的角度,应用扩展后的应用PI演算对协议抗拒绝服务攻击性进行建模,提出一个基于定理证明支持一阶定理证明器ProVerif的抗拒绝服务攻击性自动化证明方法,最后应用ProVerif分析与验证了JFK协议与IEEE 802.11四步握手协议抗拒绝服务攻击性,发现IEEE 802.11四步握手协议存在一个新的拒绝服务攻击,并且针对IEEE 802.11四步握手协议存在的拒绝服务攻击提出了改进方法.