研究目的
利用Casper/FDR研究异构网络垂直切换中EAP重认证协议(ERP)的安全特性。
研究成果
分析显示,EAP-ERP协议中代理间缺乏相互认证,但密钥材料的完整性得到了充分?;?。采用EAP-TLS作为底层家庭认证机制使安全性略有提升。
研究不足
使用Casper工具集的主要缺点在于处理大型协议时的问题,因为执行精化检查算法需要大量内存。为在建模EAP-ERP(特别是将EAP-TLS作为家庭认证机制且系统中存在四个代理)期间克服此问题,我们不得不优化Casper输入文件以缩短编译时间。