IKE2协议的形式化分析  

Formal Analysis of IKE2

作　　者：解云峰[1] 李之棠[1] 李伟明[1] 

机构地区：[1]华中科技大学计算机科学与技术学院,武汉,430074 华中科技大学网络中心,武汉,430074 华中科技大学计算机科学与技术学院,武汉,430074

出　　处：《计算机研究与发展》2006年第z2期275-279,共5页Journal of Computer Research and Development

基　　金：国家自然科学基金项目(60573120);武汉市科技攻关计划基金项目(20043001032)

摘　　要：现有的IPSec密钥交换标准存在着若干安全漏洞,为了解决相关的安全及应用问题,IETF提出了IKE2协议.应用SVO逻辑对IKE2协议进行了形式化分析,证明了IKE2协议的密钥交换和认证安全性.对IKE2协议的分析也证明了SVO逻辑可用于分析基于Diffie-Hellman交换的复杂安全协议.

关 键 词：安全协议 SVO逻辑 IKE2 

分 类 号：TP391[自动化与计算机技术—计算机应用技术]